Item

Abstract

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.