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 Library locked




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



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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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 09:52:53 PM
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
JohannsenRazgonWahlstroem_2008_SolvingSATForCNFFormulasWithAOnesidedRestrictionOnVariableOccurrences.pdf