Proceedings Article, Paper @InProceedings Beitrag in Tagungsband, Workshop

 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Library locked Goto entry point

 Author, Editor
 Author(s): Johannsen, Daniel Razgon, Igor Wahlström, Magnus dblp dblp dblp Not MPG Author(s): Razgon, Igor
 Editor(s): Kullmann, Oliver dblp 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
 URL of the conference: http://www.cs.swan.ac.uk/~csoliver/SAT2009/index.html URL for downloading the paper: 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

 (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},
}