Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)

Details Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II) Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)

2011-04-21

arxiv.org/abs/1104.4279v1

Proc. SAT 2011, Lecture Notes in Computer Science, vol. 6695, pp. 47-60, 2011

Computer Science

Data Structures and Algorithms

Scientific paper

10.1007/978-3-642-21581-0_6

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.

Affiliated with

Also associated with

No associations

Rating

Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II) does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II), we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II) will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-178626