Abstract
We show a new connection between the clause space measure in tree-like resolution and the reversible pebble game on graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the clause space complexity measure in tree-like and general resolution. We also provide upper bounds for tree-like resolution clause space in terms of general resolution clause and variable space. In particular, we show that for any formula F, its tree-like resolution clause space is upper bounded by space\((\pi)\)\((\log({\rm time}(\pi))\), where \(\pi\) is any general resolution refutation of F. This holds considering as space\((\pi)\) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space\((\pi)\log n\), where n is the number of vertices of the corresponding graph
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Change history
25 May 2021
Corrections to references in page 2 and 4 updated and errors to Theorem 4.2 corrected.
References
Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov & Avi Wigderson (2002). Space Complexity in Propositional Calculus. SIAM Journal on Computing 31(4), 1184–1211. Preliminary version in STOC '00
Carlos Ansótegui, María Luisa Bonet, Jordi Levy & Felip Manyà (2008). Measuring the Hardness of SAT Instances. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI '08), 222–228
Ben-Sasson, Eli, Impagliazzo, Russell, Wigderson, Avi: Near Optimal Separation of Tree-Like and General Resolution. Combinatorica 24(4), 585–603 (2004)
Eli Ben-Sasson & Jakob Nordström (2008). Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS '08), 709–718
Eli Ben-Sasson & Jakob Nordström (2011). Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), 401–416. Full-length version available at http://eccc.hpi-web.de/report/2010/125/
Eli Ben-Sasson & Avi Wigderson (2001). Short Proofs are Narrow—Resolution Made Simple. Journal of the ACM 48(2), 149–169. Preliminary version in STOC '99
Bennett, Charles H.: Time/Space Trade-offs for Reversible Computation. SIAM Journal on Computing 18(4), 766–776 (1989)
María Luisa Bonet, Juan Luis Esteban, Nicola Galesi & Jan Johannsen (1998). Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science (FOCS '98), 638–647
Carlson, David A., Savage, John E.: Extreme Time-Space Tradeoffs for Graphs with Small Space Requirements. Information Processing Letters 14(5), 223–227 (1982)
Siu Man Chan (2013). Just a Pebble game. In Proceedings of the 28th Annual IEEE Conference on Computational Complexity (CCC '13), 133–143
Siu Man Chan, Massimo Lauria, Jakob Nordström & Marc Vinyals (2015). Hardness of Approximation in PSPACE and Separation Results for Pebble Games (Extended Abstract). In Proceedings of the 56th Annual IEEE Symposium on Foundations of Computer Science (FOCS '15), 466–485
Davis, Martin, Logemann, George, Loveland, Donald: A Machine Program for Theorem Proving. Communications of the ACM 5(7), 394–397 (1962)
Martin Davis & Hilary Putnam: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3), 201–215 (1960)
Susanna F. de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere & Marc Vinyals (2020). Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. In Proceedings of the 61st IEEE Annual Symposium on Foundations of Computer Science (FOCS '20), 24–30. Full-length version available as arXiv:2001.02144
Susanna F. de Rezende, Or Meir, Jakob Nordström & Robert Robere (2021). Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. Computational Complexity 30(4), 1–45. Preliminary version in CCC '19
Juan Luis Esteban & Jacobo Torán (2001). Space Bounds for Resolution. Information and Computation 171(1), 84–97. Preliminary versions of these results appeared in STACS '99 and CSL '99
Juan Luis Esteban & Jacobo Torán: A combinatorial characterization of treelike resolution space. Information Processing Letters 87(6), 295–300 (2003)
Philippe Flajolet, Jean-Claude Raoult & Jean Vuillemin (1979). The Number of Registers Required for Evaluating Arithmetic Expressions. Theoretical Computer Science 9, 99–125. Preliminary version in FOCS '77
Nicola Galesi, Navid Talebanfard & Jacobo Torán (2020). Cops-Robber Games and the Resolution of Tseitin Formulas. ACM Transactions on Computation Theory 12(2), 9:1–9:22. Preliminary version in SAT '18
Matti Järvisalo, Arie Matsliah, Jakob Nordström & Stanislav Živný (2012). Relating Proof Complexity Measures and Practical Hardness of SAT. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP '12), volume 7514 of Lecture Notes in Computer Science, 316–331. Springer
Richard Královič (2004). Time and Space Complexity of Reversible Pebbling. RAIRO – Theoretical Informatics and Applications 38(02), 137–161. Preliminary version in SOFSEM '01
Friedhelm Meyer auf der Heide (1981). A Comparison of Two Variations of a Pebble Game on Graphs. Theoretical Computer Science 13(3), 315–322. Preliminary version in ICALP '79
Jakob Nordström (2012). On the Relative Strength of Pebbling and Resolution. ACM Transactions on Computational Logic 13(2), 16:1–16:43. Preliminary version in CCC '10
Jakob Nordström (2015). New Wine into Old Wineskins: A Survey of Some Pebbling Classics with Supplemental Results. Manuscript in preparation. Current draft version available at http://www.csc.kth.se/~jakobn/research/PebblingSurveyTMP.pdf
Michael S. Paterson & Carl E. Hewitt (1970). Comparative Schematology. In Record of the Project MAC Conference on Concurrent Systems and Parallel Computation, 119–127
Pavel Pudlák & Russell Impagliazzo (2000). A Lower Bound for DLL Algorithms for \(k\)-SAT (preliminary version). In Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA '00), 128–136
Ran Raz & Pierre McKenzie (1999). Separation of the Monotone NC Hierarchy. Combinatorica 19(3), 403–435. Preliminary version in FOCS '97
Razborov, Alexander A.: On Space and Depth in Resolution. Computational Complexity 27(3), 511–559 (2018)
Jacobo Torán (1999). Lower Bounds for Space in Resolution. In Proceedings of the 13th International Workshop on Computer Science Logic (CSL '99), volume 1683 of Lecture Notes in Computer Science, 362–373. Springer
Jacobo Torán & Florian Wörz (2019). Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Technical Report TR19-097, Electronic Colloquium on Computational Complexity (ECCC). https://eccc.weizmann.ac.il/report/2019/097
Jacobo Torán & Florian Wörz (2020). Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. In Proceedings of the 37th International Symposium on Theoretical Aspects of Computer Science (STACS '20), volume 154 of Leibniz International Proceedings in Informatics (LIPIcs), 60:1–60:18. https://doi.org/10.4230/LIPIcs.STACS.2020.60
Grigori Tseitin (1968). The Complexity of a Deduction in the Propositional Predicate calculus. Zapiski Nauchnyh Seminarov Leningradskogo Otdelenija matematicheskogo Instituta im. V. A. Steklova akademii Nauk SSSR (LOMI) 8, 234–259. In Russian
Urquhart, Alasdair: Hard Examples for Resolution. Journal of the ACM 34(1), 209–219 (1987)
Urquhart, Alasdair: The Depth of Resolution Proofs. Studia Logica 99(1–3), 349–364 (2011)
Acknowledgements
This research was supported by the Deutsche Forschungsgemeinschaft (DFG) under project number 430150230, “Complexity measures for solving propositional formulas”.
An extended abstract of this paper has appeared as Torán & Wörz (2020). The authors would like to thank all reviewers for many insightful comments.
Funding
Open Access funding enabled and organized by Projekt DEAL.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Torán, J., Wörz, F. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. comput. complex. 30, 7 (2021). https://doi.org/10.1007/s00037-021-00206-1
Received:
Published:
DOI: https://doi.org/10.1007/s00037-021-00206-1
Keywords
- Proof complexity
- Resolution
- Tree-like resolution
- Pebble game
- Reversible pebbling
- Prover–Delayer game
- Raz–McKenzie game
- Clause space
- Variable space