# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

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

##### 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<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.