In the first part of this work (FSTTCS'10) we have shown that the satisfiability of CNF formulas with β-acyclic hypergraphs can be decided in polynomial time. In this paper we continue and extend this work. The decision algorithm for β-acyclic formulas is based on a special type of Davis-Putnam resolution where each resolvent is a subset of a parent clause. We generalize the class of β-acyclic formulas to more general CNF formulas for which this type of Davis-Putnam resolution still applies. We then compare the class of β-acyclic formulas and this superclass with a number of known polynomial formula classes. © 2011 Springer-Verlag.
CITATION STYLE
Ordyniak, S., Paulusma, D., & Szeider, S. (2011). Satisfiability of acyclic and almost acyclic CNF formulas (II). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6695 LNCS, pp. 47–60). https://doi.org/10.1007/978-3-642-21581-0_6
Mendeley helps you to discover research relevant for your work.