Satisfiability of Acyclic and Almost Acyclic CNF FormulasSebastian Ordyniak, Daniel Paulusma, and .
Proceedings of FSTTCS 2010, 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, December 15-18, 2010, IMSc, Chennai, India. Kamal Lodaya and Meena Mahajan (eds.), Leibniz International Proceedings in Informatics (LIPIcs), pp. 84-95, 2010.
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 "β-acyclic hypergraphs" can be decided in polynomial time. We also 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 smallest strong backdoor sets and the β-hypertree width. As a by-product we obtain the W-hardness of SAT parameterized by the (undirected) clique-width of the incidence graph, which disproves a conjecture by Fischer, Makowsky, and Ravve (Discrete Applied Mathematics 156, 2008).
Link to paper: [paper pdf]