Width Versus Size in Resolution Proofs
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 , 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.
Unable to display preview. Download preview PDF.
- 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
- Buss, S.R., Turán, G.: Resolution proofs of generalized pigeonhole principles. Theoretical Computer Science, 311–317 (1988)Google Scholar
- 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.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
- Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, New York (1983)Google Scholar
- 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 , vol. 2, pp. 466–483Google Scholar