Solving SAT for CNF formulas with a One-sided Variable Occurrence Restriction
Daniel Johannsen, Igor Razgon, Magnus Wahlström · 2009
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~[Wahlstr{\\"o}m,~2005]. Applying complement search~[Purdom,~1984], we show that for every~$d$ there exists a constant~$\\gamma_d<2-\\frac{1}{2d+1}$ such that satisfiability of a~CNF formula on~$n$ variables can be checked in runtime~$\\Oh(\\gamma_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~$\\gamma_d$ more precisely. Finally, we show that the trivial~$\\Oh(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~\\emph{$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.