English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

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