Abstract
The complexity of resolution refutations of contradictory sets of clauses in propositional logic has been investigated deeply over the last forty years, beginning with the groundbreaking paper of Tseitin [16], based on a talk given in a Leningrad seminar of 1966.
A general theme that emerged gradually in the course of the intensive investigations of the last few decades has been that of basing size lower bounds on lower bounds on the width of refutations. Roughly speaking, it turns out that in many cases, the minimum size of a refutation is exponential in the minimum width.
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
Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proceedings of the 37th Annual IEEE Symposium on the Foundations of Computer Science, pp. 274–282 (1996)
Ben-Sasson, E., Wigdersonq, A.: Short proofs are narrow – resolution made simple. Journal of the Association for Computing Machinery 48, 149–169 (2001); Preliminary version: Proceedings of the 31st Annual ACM Symposium on Theory of Computing, pp. 517–526 (1999)
Bollobás, B.: Random Graphs. Academic Press, London (1985)
Buss, S.R., Pitassi, T.: Resolution and the weak pigeonhole principle. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 149–156. Springer, Heidelberg (1998)
Buss, S.R., Turán, G.: Resolution proofs of generalized pigeonhole principles. Theoretical Computer Science, 311–317 (1988)
Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery 35, 759–768 (1988)
Galil, Z.: On the complexity of regular resolution and the Davis-Putnam procedure. Theoretical Computer Science 4, 23–46 (1977)
Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)
Pitassi, T., Raz, R.: Regular resolution lower bounds for the weak pigeonhole principle. Combinatorica 24, 513–524 (2004); Preliminary version: Proceedings of the Thirty-third Annual ACM Symposium on Theory of Computing, pp. 347–355 (2001)
Raz, R.: Resolution lower bounds for the weak pigeonhole principle. Journal of the Association for Computing Machinery 51, 115–138 (2004); Preliminary version: Proceedings of the 34th Symposium on the Theory of Computing, pp. 553–562 (2002)
Razborov, A.: Improved resolution lower bounds for the weak pigeonhole principle. Technical report, Electronic Colloquium on Computational Complexity (2001), TR01-055: available at http://www.eccc.uni-trier.de/pub/reports/2001
Razborov, A.: Resolution lower bounds for the weak functional pigeonhole principle. Theoretical Computer Science 303, 233–243 (2001)
Razborov, A.: Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences 69, 3–27 (2004)
Razborov, A.A., Wigderson, A., Yao, A.: Read-once branching programs, rectangular proofs of pigeonhole principle and the transversal calculus. In: Proceedings of the 29th Annual ACM Symposium on Theory of Computing, pp. 739–748 (1997)
Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, New York (1983)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, Consultants Bureau, New York, pp. 115–125 (1970); Reprinted in [15], vol. 2, pp. 466–483
Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery 34, 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urquhart, A. (2006). Width Versus Size in Resolution Proofs. In: Cai, JY., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2006. Lecture Notes in Computer Science, vol 3959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750321_6
Download citation
DOI: https://doi.org/10.1007/11750321_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34021-8
Online ISBN: 978-3-540-34022-5
eBook Packages: Computer ScienceComputer Science (R0)