English

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Solving SAT for CNF formulas with a One-sided Variable Occurrence Restriction

##### MPS-Authors
/persons/resource/persons44705

Johannsen,  Daniel
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

/persons/resource/persons45687

Wahlström,  Magnus
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

##### External Ressource
No external resources are shared
##### Fulltext (public)
There are no public fulltexts stored in PuRe
##### Supplementary Material (public)
There is no public supplementary material available
##### Citation

Johannsen, D., Razgon, I., & Wahlström, M. (2009). Solving SAT for CNF formulas with a One-sided Variable Occurrence Restriction. In Theory and Applications of Satisfiability Testing - SAT 2009 (pp. 80-85). Berlin: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-18D0-6
##### 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&lt;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.