Document Open Access Logo

Pebble Games and Algebraic Proof Systems

Authors Lisa-Marie Jaser, Jacobo Torán

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2024.64.pdf
  • Filesize: 0.69 MB
  • 14 pages

Document Identifiers

Author Details

Lisa-Marie Jaser
  • Institut für Theoretische Informatik, Universität Ulm, Germany
Jacobo Torán
  • Institut für Theoretische Informatik, Universität Ulm, Germany

Cite AsGet BibTex

Lisa-Marie Jaser and Jacobo Torán. Pebble Games and Algebraic Proof Systems. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.MFCS.2024.64

Abstract

Analyzing refutations of the well known pebbling formulas Peb(G) we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG G with a single sink, if there is a Monomial Calculus refutation for Peb(G) having simultaneously degree s and size t then there is a black pebbling strategy on G with space s and time t+s. Also if there is a black pebbling strategy for G with space s and time t it is possible to extract from it a MC refutation for Peb(G) having simultaneously degree s and size ts. These results are analogous to those proven in [Susanna F. de Rezende et al., 2021] for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC. We also notice that for any directed acyclic graph G the space needed in a pebbling strategy on G, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb(G) in each of the algebraic proof systems NS,MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
  • Mathematics of computing → Graph theory
Keywords
  • Proof Complexity
  • Algebraic Proof Systems
  • Pebble Games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Albert Atserias and Joanna Fijalkow. Definable ellipsoid method, sums-of-squares proofs, and the graph isomorphism problem. SIAM J. Comput., 52(5):1193-1229, 2023. URL: https://doi.org/10.1137/20m1338435.
  2. Albert Atserias and Elitza N. Maneva. Sherali-Adams relaxations and indistinguishability in counting logics. SIAM Journal on Computing, 42(1):112-137, January 2013. Preliminary version in ITCS '12. URL: https://doi.org/10.1137/120867834.
  3. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. In Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science (FOCS '94), pages 794-806, 1994. URL: https://doi.org/10.1109/SFCS.1994.365714.
  4. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13), pages 813-822, May 2013. URL: https://doi.org/10.1145/2488608.2488711.
  5. Eli Ben-Sasson. Size space tradeoffs for resolution. In Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC '02), pages 457-464, May 2002. URL: https://doi.org/10.1145/509907.509975.
  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. URL: https://doi.org/10.1145/375827.375835.
  7. Charles H. Bennett. Time/space trade-offs for reversible computation. SIAM Journal on Computing, 18(4):766-776, 1989. URL: https://doi.org/10.1137/0218053.
  8. Christoph Berkholz and Martin Grohe. Limitations of algebraic approaches to graph isomorphism testing. In ICALP 2015, volume 9134 of Lecture Notes in Computer Science, pages 155-166. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47672-7_13.
  9. Joshua Buresh-Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann Pitassi. Homogenization and the polynomial calculus. Computational Complexity, 11(3-4):91-108, 2002. Preliminary version in ICALP '00. URL: https://doi.org/10.1007/s00037-002-0171-6.
  10. 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, 2015. URL: https://doi.org/10.1109/FOCS.2015.36.
  11. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC '96), pages 174-183, May 1996. URL: https://doi.org/10.1145/237814.237860.
  12. Stephen A. Cook and Ravi Sethi. Storage requirements for deterministic polynomial time recognizable languages. Journal of Computer and System Sciences, 13(1):25-37, 1976. Preliminary version in STOC '74. URL: https://doi.org/10.1016/S0022-0000(76)80048-7.
  13. Susanna F. de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. CoRR, abs/2001.02144, 2020. URL: https://doi.org/10.48550/arXiv.2001.02144.
  14. Susanna F. de Rezende, Or Meir, Jakob Nordström, and Robert Robere. Nullstellensatz size-degree trade-offs from reversible pebbling. Comput. Complex., 30(1):4, 2021. URL: https://doi.org/10.1007/s00037-020-00201-y.
  15. Erich Grädel, Martin Grohe, Benedikt Pago, and Wied Pakusa. A finite-model-theoretic view on propositional proof complexity. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:4)2019.
  16. Martin Grohe and Wied Pakusa. Descriptive complexity of linear equation systems and applications to propositional proof complexity. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005081.
  17. Alexander Hertel. Applications of Games to Propositional Proof Complexity. PhD thesis, University of Toronto, May 2008. Available at http://www.cs.utoronto.ca/~ahertel/. URL: http://hdl.handle.net/1807/16735.
  18. Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384-406, 1981. URL: https://doi.org/10.1016/0022-0000(81)90039-8.
  19. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  20. Balasubramanian Kalyanasundaram and George Schnitger. On the power of white pebbles. Combinatorica, 11(2):157-171, June 1991. Preliminary version in STOC '88. URL: https://doi.org/10.1007/BF01206359.
  21. Friedhelm Meyer auf der Heide. A comparison of two variations of a pebble game on graphs. Theoretical Computer Science, 13(3):315-322, 1981. URL: https://doi.org/10.1016/S0304-3975(81)80004-7.
  22. Jakob Nordström. Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science, 9:15:1-15:63, September 2013. URL: https://doi.org/10.2168/LMCS-9(3:15)2013.
  23. 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.
  24. 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. URL: https://doi.org/10.1145/1344551.1344563.
  25. Wolfgang J. Paul, Robert Endre Tarjan, and James R. Celoni. Space bounds for a game on graphs. Mathematical Systems Theory, 10:239-251, 1977. URL: https://doi.org/10.1007/BF01683275.
  26. Nicholas Pippenger. Pebbling. Technical Report RC8258, IBM Watson Research Center, 1980. Google Scholar
  27. Alexander A. Razborov. On space and depth in resolution. Computational Complexity, 27(3):511-559, 2018. URL: https://doi.org/10.1007/s00037-017-0163-1.
  28. John E. Savage. Models of computation - exploring the power of computing. Addison-Wesley, 1998. Google Scholar
  29. 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
  30. Jacobo Torán and Florian Wörz. Reversible pebble games and the relation between tree-like and general resolution space. Comput. Complex., 30(1):7, 2021. URL: https://doi.org/10.1007/s00037-021-00206-1.
  31. Robert E. Wilber. White pebbles help. Journal of Computer and System Sciences, 36(2):108-124, 1988. Preliminary version in STOC '85. URL: https://doi.org/10.1016/0022-0000(88)90023-2.
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 Imprint Privacy Contact