Skip to main content

Research Repository

Advanced Search

Satisfiability of acyclic and almost acyclic CNF formulas

Ordyniak, S.; Paulusma, D.; Szeider, S.

Satisfiability of acyclic and almost acyclic CNF formulas Thumbnail


Authors

S. Ordyniak

S. Szeider



Abstract

We show that the Satisfiability (SAT) problem for CNF formulas with ββ-acyclic hypergraphs can be solved in polynomial time by using a special type of Davis–Putnam resolution in which each resolvent is a subset of a parent clause. We extend this class to CNF formulas for which this type of Davis–Putnam resolution still applies and show that testing membership in this class is NP-complete. We compare the class of ββ-acyclic formulas and this superclass with a number of known polynomial formula classes. We then study the parameterized complexity of SAT for “almost” ββ-acyclic instances, using as parameter the formula’s distance from being ββ-acyclic. As distance we use the size of a smallest strong backdoor set and the ββ-hypertree width. As a by-product we obtain the W[1]W[1]-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve.

Citation

Ordyniak, S., Paulusma, D., & Szeider, S. (2013). Satisfiability of acyclic and almost acyclic CNF formulas. Theoretical Computer Science, 481, 85-99. https://doi.org/10.1016/j.tcs.2012.12.039

Journal Article Type Article
Publication Date Apr 1, 2013
Deposit Date Mar 11, 2013
Publicly Available Date Apr 17, 2013
Journal Theoretical Computer Science
Print ISSN 0304-3975
Publisher Elsevier
Peer Reviewed Peer Reviewed
Volume 481
Pages 85-99
DOI https://doi.org/10.1016/j.tcs.2012.12.039
Public URL https://durham-repository.worktribe.com/output/1465433

Files

Accepted Journal Article (263 Kb)
PDF

Copyright Statement
NOTICE: this is the author’s version of a work that was accepted for publication in Theoretical computer science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Theoretical computer science, 481, 2013, 10.1016/j.tcs.2012.12.039





You might also like



Downloadable Citations