Satisfiability of acyclic and almost acyclic CNF formulas (II)

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

Abstract

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.

Citation

Ordyniak, S., Paulusma, D., & Szeider, S. (2011, December). Satisfiability of acyclic and almost acyclic CNF formulas (II). Presented at 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011, Ann Arbor, MI

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011
• Publication Date: Jan 1, 2011
• Deposit Date: Dec 6, 2011
• Print ISSN: 0302-9743
• Pages: 47-60
• Series Title: Lecture notes in computer science
• Series Number: 6695
• Series ISSN: 0302-9743,1611-3349
• Book Title: Theory and Applications of Satisfiability Testing - SAT 2011, 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011 ; proceedings.
• ISBN: 9783642215803
• DOI: https://doi.org/10.1007/978-3-642-21581-0_6
• Public URL: https://durham-repository.worktribe.com/output/1157532