A Hierarchy of Tractable Subclasses for SAT and Counting SAT Problems

Finding subclasses of formulae for which the SAT problem can be solved in polynomial time has been an important problem in computer science. We present a new hierarchy of propositional formulæ subclasses for which the SAT and counting SAT problems can be solved in polynomial time. Our tractable subclasses are those propositional formulae in conjunctive normal form where any set of k + 1 clauses are related, i.e., there exists at least one literal in one clause that appears negated in another clause of the considered set of k + 1 clauses. We say this subclass of formulæ is of rank k and it is different from previously known subclasses that are solvable in polynomial time. This is an improvement over the SAT Dichotomy Theorem and the counting SAT Dichotomy Theorem, since our subclass can be moved out from the NP-complete class to the P class. The membership problem for this new subclass can be solved in O(n*l^{k+1}), where n, l and k are the number of variables, clauses and the rank (1 ≤ k ≤ l − 1), respectively. We give an efficient algorithm to approximate the number of assignments for any arbitrary conjunctive normal form propositional formula by an upper bound.