Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)Sebastian Ordyniak, Daniel Paulusma, and .
Proceedings of SAT 2011, Fourteenth International Conference on Theory and Applications of Satisfiability Testing June 19-22, 2011, Ann Arbor, USA. Lecture Notes in Computer Science vol. 6695, pp. 47-60, Springer, 2011.
Abstract:In the first part of this work (FSTTCS'10) we have shown that the satisfiability of CNF formulas with beta-acyclic hypergraphs can be decided in polynomial time. In this paper we continue and extend this work. The decision algorithm for beta-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 beta-acyclic formulas to more general CNF formulas for which this type of Davis-Putnam resolution still applies. We then compare the class of beta-acyclic formulas and this superclass with a number of known polynomial formula classes.
Preprint available from [arXiv.1104.4279v1]