Advertisement

Width Versus Size in Resolution Proofs

  • Alasdair Urquhart
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3959)

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)Google Scholar
  2. 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)zbMATHGoogle Scholar
  3. Bollobás, B.: Random Graphs. Academic Press, London (1985)zbMATHGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. Buss, S.R., Turán, G.: Resolution proofs of generalized pigeonhole principles. Theoretical Computer Science, 311–317 (1988)Google Scholar
  6. Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery 35, 759–768 (1988)zbMATHMathSciNetGoogle Scholar
  7. Galil, Z.: On the complexity of regular resolution and the Davis-Putnam procedure. Theoretical Computer Science 4, 23–46 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  8. Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 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)MathSciNetGoogle Scholar
  10. 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)MathSciNetGoogle Scholar
  11. 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
  12. Razborov, A.: Resolution lower bounds for the weak functional pigeonhole principle. Theoretical Computer Science 303, 233–243 (2001)CrossRefMathSciNetGoogle Scholar
  13. Razborov, A.: Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences 69, 3–27 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 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)Google Scholar
  15. Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, New York (1983)Google Scholar
  16. 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–483Google Scholar
  17. Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery 34, 209–219 (1987)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Alasdair Urquhart
    • 1
  1. 1.Departments of Philosophy and Computer ScienceUniversity of TorontoToronto, OntarioCanada

Personalised recommendations