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.
Ordyniak and Szeider’s research was funded by the ERC (COMPLEX REASON, 239962). Paulusma’s research was funded by EPSRC (EP/G043434/1).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bodlaender, H.L.: A partial k-arboretum of graphs with bounded treewidth. Theoret. Comput. Sci. 209(1-2), 1–45 (1998)
Brandstädt, A., Le, V.B., Spinrad, J.P.: Graph classes: a survey. SIAM Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (1999)
Brandstädt, A., Lozin, V.V.: On the linear structure and clique-width of bipartite permutation graphs. Ars Combinatoria 67, 273–281 (2003)
Courcelle, B., Olariu, S.: Upper bounds to the clique-width of graphs. Discr. Appl. Math. 101(1-3), 77–114 (2000)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Fagin, R.: Degrees of acyclicity for hypergraphs and relational database schemes. J. ACM 30(3), 514–550 (1983)
Fischer, E., Makowsky, J.A., Ravve, E.R.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discr. Appl. Math. 156(4), 511–529 (2008)
Ganian, R., Hlinený, P., Obdrzálek, J.: Better algorithms for satisfiability problems for formulas of bounded rank-width. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, Chennai, India, December 15-18. LIPIcs, vol. 8, pp. 73–83. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)
Gottlob, G., Szeider, S.: Fixed-parameter algorithms for artificial intelligence, constraint satisfaction, and database problems. The Computer Journal 51(3), 303–325 (2006), Survey paper
Kloks, T., Bodlaender, H.: Approximating treewidth and pathwidth of some classes of perfect graphs. In: Ibaraki, T., Iwama, K., Yamashita, M., Inagaki, Y., Nishizeki, T. (eds.) ISAAC 1992. LNCS, vol. 650, pp. 116–125. Springer, Heidelberg (1992)
Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures (1999) (manuscript)
Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, Chennai, India, December 15-18. LIPIcs, vol. 8, pp. 84–95. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)
Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50–64 (2010)
Schlipf, J.S., Annexstein, F.S., Franco, J.V., Swaminathan, R.P.: On finding solutions for extended Horn formulas. Information Processing Letters 54(3), 133–137 (1995)
Speckenmeyer, E.: Classes of easy expressions. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 13, Section 1.19, pp. 27–31. IOS Press, Amsterdam (2009)
Spinrad, J.P.: Efficient Graph Representations. Fields Institute Monographs. AMS, Providence (2003)
Tarjan, R.E., Yannakakis, M.: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. Comput. 13(3), 566–579 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ordyniak, S., Paulusma, D., Szeider, S. (2011). Satisfiability of Acyclic and almost Acyclic CNF Formulas (II). In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)