Abstract
We consider unsatisfiable Boolean formulas in conjunctive normal form. It is known that unsatisfiability can be shown by a regular resolution proof in time polynomial in the number of variables n, and exponential in the tree-width w. It is also known that satisfiability for bounded tree-width can actually be decided in time linear in the length of the formula and exponential in the tree-width w.
We investigate the complexities of resolution proofs and arbitrary proofs in more detail depending on the number of variables n and the tree-width w. We present two very traditional algorithms, one based on resolution and the other based on truth tables. Maybe surprisingly, we point out that the two algorithms turn out to be basically the same algorithm with different interpretations.
Similar results holds for a bound w′ on the tree-width of the incidence graph for a somewhat extended notion of a resolution proof. The length of any proper resolution proof might be quadratic in n, but if we allow to introduce abbreviations for frequently occurring subclauses, then the proof length and running time are again linear in n.
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
Alekhnovich, M., Razborov, A.A.: Satisfiability, branch-width and Tseitin tautologies. In: Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS 2002), pp. 593–603 (2002)
Björklund, A., Husfeldt, T., Kaski, P., Koivisto, M.: Fourier meets Möbius: Fast subset convolution. In: Proceedings of the 39th Annual ACM Symposium on Theory of Computing, STOC 2007, pp. 67–74. ACM (2007)
Björklund, A., Husfeldt, T., Kaski, P., Koivisto, M.: Trimmed Moebius inversion and graphs of bounded degree. Theor. Comp. Sys. 47, 637–654 (2010)
Bodlaender, H.L., Koster, A.M.C.A.: Combinatorial optimization on graphs of bounded treewidth. Comput. J. 51(3), 255–269 (2008)
Bodlaender, H.L.: A linear time algorithm for finding tree-decompositions of small treewidth. SIAM Journal on Computing 25, 1305–1317 (1996)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Fischer, E., Makowsky, J.A., Ravve, E.V.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Applied Mathematics 156(4), 511–529 (2008)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Robertson, N., Seymour, P.D.: Graph minors. X. Obstructions to tree-decomposition. Comb. Theory, Ser. B 52(2), 153–190 (1991)
Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50–64 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fürer, M. (2012). Efficient Arbitrary and Resolution Proofs of Unsatisfiability for Restricted Tree-Width. In: Fernández-Baca, D. (eds) LATIN 2012: Theoretical Informatics. LATIN 2012. Lecture Notes in Computer Science, vol 7256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29344-3_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-29344-3_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29343-6
Online ISBN: 978-3-642-29344-3
eBook Packages: Computer ScienceComputer Science (R0)