Document Open Access Logo

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

Authors Jacobo Torán , Florian Wörz

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Jacobo Torán
  • Universität Ulm, Ulm, Germany
Florian Wörz
  • Universität Ulm, Ulm, Germany

Funding

This research was supported by the Deutsche Forschungsgemeinschaft (DFG) under project number 430150230, "Complexity measures for solving propositional formulas".

Acknowledgements

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

Cite As Get BibTex

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
    PDF Downloads
    0
    Metadata Views

Related Versions

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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  7. Charles H. Bennett. Time/space trade-offs for reversible computation. SIAM Journal on Computing, 18(4):766-776, August 1989. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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]. Google Scholar
  12. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, July 1962. Google Scholar
  13. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. Google Scholar
  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. Google Scholar
  16. Juan Luis Esteban and Jacobo Torán. A combinatorial characterization of treelike resolution space. Information Processing Letters, 87(6):295-300, 2003. Google Scholar
  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. Google Scholar
  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. Google Scholar
  19. Richard Královič. Time and space complexity of reversible pebbling. RAIRO - Theoretical Informatics and Applications, 38(02):137-161, April 2004. Google Scholar
  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. Google Scholar
  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. Google Scholar
  23. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Combinatorica, 19(3):403-435, March 1999. Preliminary version in FOCS '97. Google Scholar
  24. Alexander A. Razborov. On space and depth in resolution. Computational Complexity, 27(3):511-559, 2018. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  29. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987. Google Scholar
  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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact