Document

# Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

## File

LIPIcs.STACS.2020.60.pdf
• Filesize: 0.55 MB
• 18 pages

## Acknowledgements

The authors would like to thank the reviewers for many insightful comments.

## Cite As

Jacobo Torán and Florian Wörz. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.STACS.2020.60

## Abstract

We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are not far from optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular we show that for any formula F, its tree-like resolution space is upper bounded by space(π)log(time(π)), where π is any general resolution refutation of F. This holds considering as space(π) 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(π)log n, where n is the number of vertices of the corresponding graph.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Proof complexity
##### Keywords
• Proof Complexity
• Resolution
• Tree-like Resolution
• Pebble Game
• Reversible Pebbling
• Prover-Delayer Game
• Raz - McKenzie Game
• Clause Space
• Variable Space

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM Journal on Computing, 31(4):1184-1211, 2002. Preliminary version in STOC '00.
2. Carlos Ansótegui, María Luisa Bonet, Jordi Levy, and Felip Manyà. Measuring the hardness of SAT instances. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI '08), pages 222-228, July 2008.
3. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, September 2004.
4. Eli Ben-Sasson and Jakob Nordström. 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), pages 709-718, October 2008.
5. Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), pages 401-416, January 2011. Full-length version available at URL: http://eccc.hpi-web.de/report/2010/125/.
6. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, March 2001. Preliminary version in STOC '99.
7. Charles H. Bennett. Time/space trade-offs for reversible computation. SIAM Journal on Computing, 18(4):766-776, August 1989.
8. María Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. 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), pages 638-647, November 1998.
9. David A. Carlson and John E. Savage. Extreme time-space tradeoffs for graphs with small space requirements. Information Processing Letters, 14(5):223-227, 1982.
10. Siu Man Chan. Just a pebble game. In Proceedings of the 28th Annual IEEE Conference on Computational Complexity (CCC '13), pages 133-143, June 2013.
11. Siu Man Chan, Massimo Lauria, Jakob Nordström, and Marc Vinyals. 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), pages 466-485, October 2015. Full-length version in [30].
12. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, July 1962.
13. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960.
14. Susanna F. de Rezende. Lower Bounds and Trade-offs in Proof Complexity. PhD thesis, KTH Royal Institute of Technology, June 2019. Available at URL: http://kth.diva-portal.org/smash/record.jsf?pid=diva2%3A1318061&dswid=-4968.
15. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171(1):84-97, 2001. Preliminary versions of these results appeared in STACS '99 and CSL '99.
16. Juan Luis Esteban and Jacobo Torán. A combinatorial characterization of treelike resolution space. Information Processing Letters, 87(6):295-300, 2003.
17. Nicola Galesi, Navid Talebanfard, and Jacobo Torán. Cops-robber games and the resolution of Tseitin formulas. In Proceedings of the 21th International Conference on Theory and Applications of Satisfiability Testing (SAT '18), volume 10929 of Lecture Notes in Computer Science, pages 311-326. Springer, 2018.
18. Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný. 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, pages 316-331. Springer, October 2012.
19. Richard Královič. Time and space complexity of reversible pebbling. RAIRO - Theoretical Informatics and Applications, 38(02):137-161, April 2004.
20. Jakob Nordström. 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, 2015. URL: http://www.csc.kth.se/~jakobn/research/PebblingSurveyTMP.pdf.
21. Michael S. Paterson and Carl E. Hewitt. Comparative schematology. In Record of the Project MAC Conference on Concurrent Systems and Parallel Computation, pages 119-127, 1970.
22. Pavel Pudlák and Russell Impagliazzo. 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), pages 128-136, January 2000.
23. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Combinatorica, 19(3):403-435, March 1999. Preliminary version in FOCS '97.
24. Alexander A. Razborov. On space and depth in resolution. Computational Complexity, 27(3):511-559, 2018.
25. Uwe Schöning and Jacobo Torán. The Satisfiability Problem: Algorithms and Analyses, volume 3 of Mathematics for Applications (Mathematik für Anwendungen). Lehmanns Media, 2013.
26. Jacobo Torán and Florian Wörz. Reversible pebble games and the relation between tree-like and general resolution space. Technical Report TR19-097, Electronic Colloquium on Computational Complexity (ECCC), 2019. URL: https://eccc.weizmann.ac.il/report/2019/097.
27. Jacobo Torán. 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, pages 362-373. Springer, 1999.
28. Grigori Tseitin. 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, 1968. In Russian.
29. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987.
30. Marc Vinyals. Space in Proof Complexity. PhD thesis, KTH Royal Institute of Technology, May 2017. Available at URL: http://www.csc.kth.se/~jakobn/project-proofcplx/docs/MV_PhDthesis.pdf.
X

Feedback for Dagstuhl Publishing