In this paper we consider the class of Boolean formulas in Conjunctive Normal Form (CNF) where for each variable all but at most d occurrences are either positive or negative. This class is a generalization of the class of CNF formulas with at most d occurrences (positive and negative) of each variable which was studied in [Wahlstrom, 2005]. Applying complement search [Purdom, 1984], we show that for every d there exists a constant γ_d < 2 - 1/(2d+1) such that satisfiability of a CNF formula on n variables can be checked in runtime O(γ_d~n) if all but at most d occurrences of each variable are either positive or negative. We thoroughly analyze the proposed branching strategy and determine the asymptotic growth constant γ_d more precisely. Finally, we show that the trivial O(2~n) barrier of satisfiability checking can be broken even for a more general class of formulas, namely formulas where the positive or negative literals of every variable have what we will call a d-covering. To the best of our knowledge, for the considered classes of formulas there are no previous non-trivial upper bounds on the complexity of satisfiability checking.
展开▼
