Abstract
We analyse the possibility that a system that simulates Resolution is automatizable. We call this notion ”weak automatizability”. We prove that Resolution is weakly automatizable if and only if Res(2) has feasible interpolation. In order to prove this theorem, we show that Res(2) has polynomial-size proofs of the reflection principle of Resolution (and of any Res(k)), which is a version of consistency. We also show that Resolution proofs of its own reflection principle require slightly subexponential size. This gives a better lower bound for the monotone interpolation of Res(2) and a better separation from Resolution as a byproduct. Finally, the techniques for proving these results give us a new complexity measure for Resolution that refines the width of Ben-Sasson and Wigderson. The new measure and techniques suggest a new algorithm to find Resolution refutations, and a way to obtain a large class of examples that have small Resolution refutations but require relatively large width. This answers a question of Alekhnovich and Razborov related to whether Resolution is automatizable in quasipolynomial-time.
Partially supported by CICYT TIC2001-1577-C03-02, ALCOM-FT IST-99-14186 and HA2000-41.
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.
Similar content being viewed by others
References
M. Alekhnovich and A. A. Razborov. Resolution is not automatizable unless W[P] is tractable. In 42nd Annual IEEE Symposium on Foundations of Computer Science, 2001.
N. Alon and R. B. Boppana. The monotone circuit complexity of boolean functions. Combinatorica, 7:1–22, 1987.
A. Atserias and M. L. Bonet. On the automatizability of resolution and related propositional proof systems. ECCC TR02-010, 2002.
A. Atserias, M. L. Bonet, and J.L. Esteban. Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Accepted for publication in Information and Computation. A preliminary version appeared in ICALP’01, Lecture Notes in Computer Science 2076, Springer, pages 1005–1016., 2001.
P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In 37th Annual IEEE Symposium on Foundations of Computer Science, pages 274–282, 1996.
E. Ben-Sasson, R. Impagliazzo, and A. Wigderson. Near-optimal separation of general and tree-like resolution. To appear, 2002.
E. Ben-Sasson and A. Wigderson. Short proofs are narrow-resolution made simple. J. ACM, 48(2):149–169, 2001.
M. Blum, R. M. Karp, O. Vornberger, C. H. Papadimitriou, and M. Yannakakis. The complexity of testing whether a graph is a superconcentrator. Information Processing Letter, 13:164–167, 1981.
M. L. Bonet, C. Domingo, R. Gavaldà, A. Maciel, and T. Pitassi. Non-automatizability of bounded-depth Frege proofs. In 14th IEEE Conference on Computational Complexity, pages 15–23, 1999. Accepted for publication in the Journal of Computational Complexity.
M. L. Bonet, J. L. Esteban, N. Galesi, and J. Johansen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal of Computing, 30(5):1462–1484, 2000. A preliminary version appeared in FOCS’98.
M. L. Bonet and N. Galesi. Optimality of size-width trade-offs for resolution. Journal of Computational Complexity, 2001. To appear. A preliminary version appeared in FOCS’99.
M. L. Bonet, T. Pitassi, and R. Raz. Lower bounds for cutting planes proofs with small coefficients. Journal of Symbolic Logic, 62(3):708–728, 1997. A preliminary version appeared in STOC’95.
M. L. Bonet, T. Pitassi, and R. Raz. On interpolation and automatization for Frege systems. SIAM Journal of Computing, 29(6):1939–1967, 2000. A preliminary version appeared in FOCS’97.
S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36–50, 1979.
S.A. Cook and A. Haken. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences, 58:326–335, 1999.
S. Dantchev and S. Riis. Tree resolution proofs of the weak pigeon-hole principle. In 16th IEEE Conference on Computational Complexity, pages 69–75, 2001.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394–397, 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7:201–215, 1960.
J. L. Esteban, N. Galesi, and J. Messner. Personal communication. Manuscript, 2001.
R. Impagliazzo, T. Pitassi, and A. Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In 9th IEEE Symposium on Logic in Computer Science, pages 220–228, 1994.
J. Krajícek. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 39(1):73–86, 1994.
J. Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, 62:457–486, 1997.
J. Krajícek. On the weak pigeonhole principle. To appear in Fundamenta Mathematicæ, 2000.
J. Krajícek and P. Pudlák. Some consequences of cryptographical conjectures for S 2 1 and EF. Information and Computation, 140(1):82–94, 1998.
A. Maciel, T. Pitassi, and A.R. Woods. A new proof of the weak pigeonhole principle. In 32nd Annual ACM Symposium on the Theory of Computing, 2000.
P. Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3):981–998, 1997.
P. Pudlák. On the complexity of the propositional calculus. In Sets and Proofs, Invited Papers from Logic Colloquium’ 97, pages 197–218. Cambridge University Press, 1999.
P. Pudlák. On reducibility and symmetry of disjoint NP-pairs. In 26th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, pages 621–632. Springer-Verlag, 2001.
P. Pudlák and J. Sgall. Algebraic models of computation and interpolation for algebraic proof systems. In P. W. Beame and S.R. Buss, editors, Proof Complexity and Feasible Arithmetic, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279–296. American Mathematical Society, 1998.
A. A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya of the RAN, 59(1):205–227, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Atserias, A., Bonet, M.L. (2002). On the Automatizability of Resolution and Related Propositional Proof Systems. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_38
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive