Looking for subclasses of formulas for which the SAT problem can be solved
in polynomial time is one of important challenges in computer science.
We present a new subclass of formulas for which the SAT and counting SAT
problem can be solved in polynomial time. Specifically, our novel algorithm
operates on conjunctive normal form propositional formulas in which all pairs
of clauses are coupled, i.e., there exists at least one literal in
one clause that appears negated in the other. This subclass of formulas is
different than previously known subclasses that are
solvable in polynomial time. This is an improvement over the SAT Dichotomy
Theorem [Sch78] and the counting SAT Dichotomy Theorem [CrH96], since
our subclass can be moved out from the NP-complete class to
P. The membership problem for this new subclass can be done in
O(n x l^2), where n and l are the number of variables
and clauses, respectively. Moreover, the algorithm can also be used
to approximate the counting SAT problem for arbitrary conjunctive
normal form propositional formulas in that it generates an upper bound
for the number of assignments that satisfy the formula.
|