Satisfiability of Acyclic and Almost Acyclic CNF Formulas

Ordyniak, Sebastian; Paulusma, Daniel; Szeider, Stefan

doi:10.4230/LIPIcs.FSTTCS.2010.84

Document

Satisfiability of Acyclic and Almost Acyclic CNF Formulas

Authors Sebastian Ordyniak, Daniel Paulusma, Stefan Szeider

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2010.84.pdf

Filesize: 468 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2010.84
URN: urn:nbn:de:0030-drops-28556

Subject Classification

Keywords

Satisfiability
chordal bipartite graphs
beta-acyclic hypergraphs
backdoor sets
parameterized complexity

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

We study the propositional satisfiability problem (SAT) on classes of CNF formulas (formulas in Conjunctive Normal Form) that obey certain structural restrictions in terms of their hypergraph structure, by associating to a CNF formula the hypergraph obtained by ignoring negations and considering clauses as hyperedges on variables. We show that satisfiability of CNF formulas with so-called ``beta-acyclic hypergraphs'' can be decided in polynomial time.

We also study the parameterized complexity of SAT for ``almost''  beta-acyclic instances, using as parameter the formula's distance   from being beta-acyclic. As distance we use the size of smallest strong backdoor sets and the beta-hypertree width. As a by-product we obtain the W[1]-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve (Discr. Appl. Math. 156, 2008).

Cite As Get BibTex

Sebastian Ordyniak, Daniel Paulusma, and Stefan Szeider. Satisfiability of Acyclic and Almost Acyclic CNF Formulas. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 84-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.FSTTCS.2010.84

Author Details

Sebastian Ordyniak

Daniel Paulusma

Stefan Szeider

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail