Ordyniak, S. and Paulusma, Daniel and Szeider, S. (2011) 'Satisfiability of acyclic and almost acyclic CNF formulas (II).', in Theory and Applications of Satisfiability Testing - SAT 2011, 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011 ; proceedings. Berlin: Springer, pp. 47-60. Lecture notes in computer science. (6695).
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.
| Item Type: | Book chapter |
|---|---|
| Full text: | Full text not available from this repository. |
| Publisher Web site: | http://dx.doi.org/10.1007/978-3-642-21581-0_6 |
| Date accepted: | No date available |
| Date deposited: | No date available |
| Date of first online publication: | 2011 |
| Date first made open access: | No date available |
Save or Share this output
| Export: | |
| Look up in GoogleScholar |
