MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Johannsen, Daniel
Razgon, Igor
Wahlström, Magnus		dblp
dblp
dblp
Not MPG Author(s):
Razgon, Igor
Editor(s):
Kullmann, Oliverdblp
Not MPII Editor(s):
Kullmann, Oliver
BibTeX cite key*:
JohannsenRazgonWahlstroem2008
Title, Booktitle
Title*:
Solving SAT for CNF formulas with a one-sided variable occurrence restriction
JohannsenRazgonWahlstroem_2008_SolvingSATForCNFFormulasWithAOnesidedRestrictionOnVariableOccurrences.pdf (167.5 KB)
Booktitle*:
Theory and Applications of Satisfiability Testing, SAT 2009 : 12th International Conference, SAT 2009
Event, URLs
Conference URL::
http://www.cs.swan.ac.uk/~csoliver/SAT2009/index.html
Downloading URL:
http://www.springerlink.com/content/08lk850607575768/fulltext.pdf
Event Address*:
Swansea, Wales, United Kingdom
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
30 June 2009
Event End Date:
3 July 2009
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
5584
Number:
Month:
Pages:
80-85
Year*:
2009
VG Wort Pages:
ISBN/ISSN:
978-3-642-02776-5
Sequence Number:
DOI:
10.1007/978-3-642-02777-2_10
Note, Abstract, ©
(LaTeX) 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.
Keywords:
Satisfiability
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Algorithms and Complexity Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{JohannsenRazgonWahlstroem2008,
AUTHOR = {Johannsen, Daniel and Razgon, Igor and Wahlstr{\"o}m, Magnus},
 EDITOR = {Kullmann, Oliver},
 TITLE = {Solving {SAT} for {CNF} formulas with a one-sided variable occurrence restriction},
 BOOKTITLE = {Theory and Applications of Satisfiability Testing, SAT 2009 : 12th International Conference, SAT 2009},
 PUBLISHER = {Springer},
 YEAR = {2009},
 VOLUME = {5584},
 PAGES = {80--85},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Swansea, Wales, United Kingdom},
 ISBN = {978-3-642-02776-5},
 DOI = {10.1007/978-3-642-02777-2_10},
}

Entry last modified by Manuel Lamotte-Schubert, 02/25/2011
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]		Created
06/03/2009 21:52:53
Revisions
4.
3.
2.
1.
0.		Editor(s)
Manuel Lamotte-Schubert
Anja Becker
Daniel Johannsen
Daniel Johannsen
Daniel Johannsen		Edit Dates
25.02.2011 08:11:32
08.03.2010 13:30:18
11/17/2009 03:18:30 PM
03.06.2009 22:05:21
03.06.2009 21:52:53

File Attachment Icon
JohannsenRazgonWahlstroem_2008_SolvingSATForCNFFormulasWithAOnesidedRestrictionOnVariableOccurrences.pdf