The #SAT problem is a classical #P-complete problem even for monotone, Horn and two conjunctive formulas (the last known as #2SAT). We present a novel branch and bound algorithm to solve the #2SAT problem exactly. Our procedure establishes a new threshold where #2SAT can be computed in polynomial time. We show that for any 2-CF formula F with n variables where #2SAT(F) . p(n), for some polynomial p, #2SAT(F) is computed in polynomial time. This is a new way to measure the degree of difficulty for solving #2SAT and, according to such measure our algorithm allows to determine a boundary between ‘hard’ and easy’ instances of the #2SAT problem.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.