Skip to main content

Research Repository

Advanced Search

Satisfiability of acyclic and almost acyclic CNF formulas (II)

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

Authors

S. Ordyniak

S. Szeider



Contributors

K. A. Sakallah
Editor

L. Simons
Editor

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). Satisfiability of acyclic and almost acyclic CNF formulas (II). In K. A. Sakallah, & L. Simons (Eds.), Theory and Applications of Satisfiability Testing - SAT 2011, 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011 ; proceedings (47-60). https://doi.org/10.1007/978-3-642-21581-0_6

Conference Name 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011
Conference Location Ann Arbor, MI
Publication Date Jan 1, 2011
Deposit Date Dec 6, 2011
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


You might also like



Downloadable Citations