Abstract
We analyze size and space complexity of Res(k), a family of proof systems introduced by Krajíček in [16] which extend Resolution by allowing disjunctions of conjunctions of up to k ≥ 1 literals. We prove the following results: (1) The treelike Res(k) proof systems form a strict hierarchy with respect to proof size and also with respect to space. (2) Resolution polynomially simulates treelike Res(k), and is almost exponentially separated from treelike Res(k). (3) The space lower bounds known for Resolution also carry over to Res(k). We obtain almost optimal space lower bounds for PHPn, GTn, Random Formulas, CTn, and Tseitin Tautologies.
The authors were partly supported by the DAAD project Acciones integradas Hispano-Alemanas no. 70116. J.L. Esteban was also partly supported by MEC through grant PB 98-0937-C04 (FRESCO Project). N. Galesi was also partly supported by Spanish grant TIC2001-1577-C03-02 and by CSERC Canadian funds.
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, E. Ben-Sasson, A. Razborov, A. Wigderson. Space complexity in propositional calculus. STOC 2000 pp. 358–367. To appear in SIAM J. Comput.
M. Alekhnovich, A. Razborov. Resolution is not automatizable unless W[P] is not tractable. FOCS 2001. pp. 190–199.
A. Atserias, M. L. Bonet. On the automatizability of Resolution and related propositional proof systems. TR02-010, ECCC, 2002.
A. Atserias, M.L. Bonet, J.L. Esteban. Lower Bounds for the Weak Pigeonhole Principle Beyond Resolution. ICALP 2001, pp. 1005–1016.
P. Beame, T. Pitassi. Simplified and Improved Resolution Lower Bounds. FOCS 1996, pp. 274–282.
E. Ben-Sasson. Size-Space tradeoffs for Resolution. To appear in,STOC 2002.
E. Ben-Sasson, N. Galesi. Space Complexity of Random Formulae in Resolution. CCC 2001, pp. 42–51.
E. Ben-Sasson, R. Impagliazzo, A. Wigderson. Near optimal separation of treelike and general Resolution. TR00-005, ECCC, 2000.
E. Ben-Sasson, A. Wigderson. Short Proofs Are Narrow—Resolution Made Simple. J. A CM 48(2) pp. 149–168, 2001.
M.L. Bonet, J.L. Esteban, N. Galesi, J. Johannsen. On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems. SIAM J. Comput. 30(5) pp. 1462–1484, 2000.
P. Beame, R.M. Karp, T. Pitassi, M.E. Saks. On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas. STOC 1998, pp. 561–571.
M.L. Bonet, T. Pitassi, R. Raz On Interpolation and Automatization for Frege Systems. SIAM J. Comput. 29(6) pp. 1939–1967, 2000.
S. Cook, R. Reckhow. The relative efficiency of propositional proof systems. J. Symbolic Logic 44 pp. 36–50, 1979.
J.L. Esteban, J. Torán. Space bounds for resolution. Inform. and Comput. 171(1) pp. 84–97, 2001.
A. Haken. The Intractability of Resolution. Theoret. Comp. Sci. 39, 297–308, 1985.
J. Krajíček. On the weak pigeonhole principle. Fund. Math. 170(1–3) pp. 123–140, 2001.
J. Krajíček. Lower Bounds to the Size of Constant-Depth Propositional Proofs. J. Symbolic Logic 59(1) pp. 73–86, 1994.
J. Krajíček, P. Pudlák. Some Consequences of Cryptographical Conjectures for S 21 and EF. Inform. and Comput. 140(1) pp. 82–94, 1998.
A. Maciel, T. Pitassi, A.R. Woods. A new proof of the weak pigeonhole principle. STOC 2000 pp. 368–377.
W.J. Paul, R.E. Tarjan, J.R. Celoni. Space bounds for a game on graphs. Math. Systems Theory, 10 pp. 239–251, 1977.
P. Pudlák, R. Impagliazzo. Lower bounds for DLL algorithms. SODA 2000 pp. 128–136.
R. Raz. Resolution Lower Bounds for the Weak Pigeonhole Principle. TR01-21. ECCC, 2001.
A. Razborov. Resolution Lower Bounds for Perfect Matching Principles.MS, 2001.
G.S. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part 2. pp. 115–125. Consultants Bureau, New York-London, 1968.
A. Urquhart. Hard examples for resolution. J. A CM 34(1) pp. 209–219, 1987.
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
Esteban, J.L., Galesi, N., Messner, J. (2002). On the Complexity of Resolution with Bounded Conjunctions. In: Widmayer, P., Eidenbenz, S., Triguero, F., Morales, R., Conejo, R., Hennessy, M. (eds) Automata, Languages and Programming. ICALP 2002. Lecture Notes in Computer Science, vol 2380. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45465-9_20
Download citation
DOI: https://doi.org/10.1007/3-540-45465-9_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43864-9
Online ISBN: 978-3-540-45465-6
eBook Packages: Springer Book Archive