Affiliations: Computer Sciences Department, Benemérita Universidad Autónoma de Puebla, México. deita@cs.buap.mx | Facultad de Ingeniería, Universidad Autónoma del Estado de México. rmarcial@fi.uaemex.mx | Facultad de Ingeniería, Universidad Autónoma del Estado de México. xoseahernandez@gmail.com
Note: [] Address for correspondence: Computer Sciences Department, Benemérita Universidad Autónoma de Puebla, México
Abstract: 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.
