Satisfiability of acyclic and almost acyclic CNF formulas

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

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