Solving SAT for CNF formulas with a one-sided restriction on variable occurrences
- Johannsen, D.
- Razgon, Igor
- Wahlström, M.
DOIAbstract
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öm, 2005]. Applying complement search [Purdom, 1984], we show that for every d there exists a constant γd<2−12d+1 such that satisfiability of a CNF formula on n variables can be checked in runtime \ensuremathO(γnd) 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 precisel...
Add to ORKG