Document Open Access Logo

Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling

Authors Susanna F. de Rezende, Jakob Nordström, Or Meir, Robert Robere

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2019.18.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • Nullstellensatz
  • pebble games
  • trade-offs
  • size
  • degree

Metrics

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

Abstract

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz refutation of the pebbling formula over G in size t+1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

Cite As Get BibTex

Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CCC.2019.18

Author Details

Susanna F. de Rezende
  • KTH Royal Institute of Technology, Stockholm, Sweden
Jakob Nordström
  • University of Copenhagen, Denmark
  • KTH Royal Institute of Technology, Stockholm, Sweden
Or Meir
  • University of Haifa, Israel
Robert Robere
  • DIMACS, New Brunswick, U.S.A.

Funding

This work was mostly carried out while the authors were visiting the Simons Institute for the Theory of Computing in association with the DIMACS/Simons Collaboration on Lower Bounds in Computational Complexity, which is conducted with support from the National Science Foundation.
  • de Rezende, Susanna F.: was supported by the Knut and Alice Wallenberg grant KAW 2016.0066 Approximation and Proof Complexity.
  • Nordström, Jakob: was supported by the Knut and Alice Wallenberg grant KAW 2016.0066 Approximation and Proof Complexity and by the Swedish Research Council grants 621-2012-5645 and 2016-00782.
  • Meir, Or: was supported by the Israel Science Foundation (grant No. 1445/16).
  • Robere, Robert: was supported by NSERC, and also conducted part of this work at DIMACS with support from the National Science Foundation under grant number CCF-1445755.

Acknowledgements

We are grateful for many interesting discussions about matters pebbling-related (and not-so-pebbling-related) with Arkadev Chattopadhyay, Toniann Pitassi, and Marc Vinyals.

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. Joël Alwen and Vladimir Serbinenko. High Parallel Complexity Graphs and Memory-Hard Functions. In Proceedings of the 47th Annual ACM Symposium on Theory of Computing (STOC '15), pages 595-603, June 2015. Google Scholar
  3. Albert Atserias and Tuomas Hakoniemi. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. Technical report, arXiv.org, November 2018. URL: http://arxiv.org/abs/1811.01351.
  4. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow Proofs May Be Maximally Long. ACM Transactions on Computational Logic, 17(3):19:1-19:30, May 2016. Preliminary version in CCC '14. Google Scholar
  5. Albert Atserias and Joanna Ochremiak. Proof Complexity Meets Algebra. ACM Transactions on Computational Logic, 20:1:1-1:46, February 2019. Preliminary version in ICALP '17. Google Scholar
  6. Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The Relative Complexity of NP Search Problems. Journal of Computer and System Sciences, 57(1):3-19, August 1998. Preliminary version in STOC '95. Google Scholar
  7. 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, November 1994. Google Scholar
  8. 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. Google Scholar
  9. Eli Ben-Sasson. Size-Space Tradeoffs for Resolution. SIAM Journal on Computing, 38(6):2511-2525, May 2009. Preliminary version in STOC '02. Google Scholar
  10. 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. Google Scholar
  11. 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
  12. Charles H. Bennett. Logical Reversibility of Computation. IBM Journal of Research and Development, 17(6):525-532, November 1973. Google Scholar
  13. Charles H. Bennett. Time/Space Trade-offs for Reversible Computation. SIAM Journal on Computing, 18(4):766-776, August 1989. Google Scholar
  14. Christoph Berkholz. The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs. In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS '18), volume 96 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:14, February 2018. Google Scholar
  15. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  16. Harry Buhrman, John Tromp, and Paul Vitányi. Time and Space Bounds for Reversible Simulation. Journal of physics A: Mathematical and general, 34:6821-6830, 2001. Preliminary version in ICALP '01. Google Scholar
  17. 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. Google Scholar
  18. Samuel R. Buss. Lower Bounds on Nullstellensatz Proofs via Designs. In Proof Complexity and Feasible Arithmetics, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 59-71. American Mathematical Society, 1998. Available at URL: http://www.math.ucsd.edu/~sbuss/ResearchWeb/designs/.
  19. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiri Sgall. Proof Complexity in Algebraic Systems and Bounded Depth Frege Systems with Modular Counting. Computational Complexity, 6(3):256-298, 1997. Google Scholar
  20. Samuel R. Buss and Toniann Pitassi. Good Degree Bounds on Nullstellensatz Refutations of the Induction Principle. Journal of Computer and System Sciences, 2(57):162-171, October 1998. Preliminary version in CCC '96. Google Scholar
  21. David A. Carlson and John E. Savage. Graph Pebbling with Many Free Pebbles Can Be Difficult. In Proceedings of the 12th Annual ACM Symposium on Theory of Computing (STOC '80), pages 326-332, 1980. Google Scholar
  22. 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
  23. 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. Google Scholar
  24. Siu Man Chan and Aaron Potechin. Tight Bounds for Monotone Switching Networks via Fourier Analysis. Theory of Computing, 10:389-419, October 2014. Preliminary version in STOC '12. Google Scholar
  25. Ashok K. Chandra. Efficient Compilation of Linear Recursive Programs. In Proceedings of the 14th Annual Symposium on Switching and Automata Theory (SWAT '73), pages 16-25, 1973. Google Scholar
  26. 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. Google Scholar
  27. Stephen A. Cook. An Observation on Time-Storage Trade Off. Journal of Computer and System Sciences, 9(3):308-316, 1974. Preliminary version in STOC '73. Google Scholar
  28. Stefan S. Dantchev, Barnaby Martin, and Martin Rhodes. Tight Rank Lower Bounds for the Sherali-Adams Proof System. Theoretical Computer Science, 410(21-23):2054-2063, May 2009. Google Scholar
  29. 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. Manuscript in preparation, 2019. Google Scholar
  30. Cynthia Dwork, Moni Naor, and Hoeteck Wee. Pebbling and Proofs of Work. In Proceedings of the 25th Annual International Cryptology Conference (CRYPTO '05), volume 3621 of Lecture Notes in Computer Science, pages 37-54. Springer, August 2005. Google Scholar
  31. Yuval Filmus, Toniann Pitassi, Robert Robere, and Stephen A Cook. Average Case Lower Bounds for Monotone Switching Networks. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS '13), pages 598-607, November 2013. Google Scholar
  32. John R. Gilbert, Thomas Lengauer, and Robert Endre Tarjan. The Pebbling Problem is Complete in Polynomial Space. SIAM Journal on Computing, 9(3):513-524, August 1980. Preliminary version in STOC '79. Google Scholar
  33. Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. Exponential Lower Bound for Static Semi-algebraic Proofs. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP '02), volume 2380 of Lecture Notes in Computer Science, pages 257-268. Springer, July 2002. Google Scholar
  34. Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in Monotone Complexity and TFNP. Technical Report TR18-163, Electronic Colloquium on Computational Complexity (ECCC), September 2018. Google Scholar
  35. John Hopcroft, Wolfgang Paul, and Leslie Valiant. On Time Versus Space. Journal of the ACM, 24(2):332-337, April 1977. Preliminary version in FOCS '75. Google Scholar
  36. 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. Google Scholar
  37. Arist Kojevnikov and Dmitry Itsykson. Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP '06), volume 4051 of Lecture Notes in Computer Science, pages 323-334. Springer, July 2006. Google Scholar
  38. Balagopal Komarath, Jayalal Sarma, and Saurabh Sawlani. Pebbling meets coloring: Reversible pebble game on trees. Journal of Computer and System Sciences, 91:33-41, 2018. URL: http://dx.doi.org/10.1016/j.jcss.2017.07.009.
  39. Richard Královič. Time and Space Complexity of Reversible Pebbling. RAIRO - Theoretical Informatics and Applications, 38(02):137-161, April 2004. Google Scholar
  40. Klaus-Jörn Lange, Pierre McKenzie, and Alain Tapp. Reversible Space Equals Deterministic Space. Journal of Computer and System Sciences, 60(2):354-367, April 2000. Google Scholar
  41. Thomas Lengauer and Robert Endre Tarjan. Asymptotically Tight Bounds on Time-Space Trade-offs in a Pebble Game. Journal of the ACM, 29(4):1087-1130, October 1982. Preliminary version in STOC '79. Google Scholar
  42. Ming Li, John Tromp, and Paul Vitányi. Reversible Simulation of Irreversible Computation. Physica D: Nonlinear Phenomena, 120(1-2):168-176, September 1998. Google Scholar
  43. Ming Li and Paul Vitányi. Reversibility and Adiabatic Computation: Trading Time and Space for Energy. Proceedings of the Royal Society of London, Series A, 452(1947):769-789, April 1996. Google Scholar
  44. Jesús A. De Loera, Jon Lee, Susan Margulies, and Shmuel Onn. Expressing Combinatorial Problems by Systems of Polynomial Equations and Hilbert’s Nullstellensatz. Combinatorics, Probability and Computing, 18(4):551-582, July 2009. Google Scholar
  45. Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj Bjørner, and Giovanni De Micheli. Reversible Pebbling Game for Quantum Memory Management. CoRR, abs/1904.02121, 2019. URL: http://arxiv.org/abs/1904.02121.
  46. Jakob Nordström. Pebble Games, Proof Complexity and Time-Space Trade-offs. Logical Methods in Computer Science, 9(3):15:1-15:63, September 2013. Google Scholar
  47. Jakob Nordström. New Wine into Old Wineskins: A Survey of Some Pebbling Classics with Supplemental Results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical Computer Science. Current draft version available at http://www.csc.kth.se/~jakobn/research/, 2019.
  48. 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
  49. Nicholas Pippenger. Pebbling. Technical Report RC8258, IBM Watson Research Center, 1980. in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan. Google Scholar
  50. Toniann Pitassi and Robert Robere. Strongly Exponential Lower Bounds for Monotone Computation. In Proceedings of the 49th Annual ACM Symposium on Theory of Computing (STOC '17), pages 1246-1255, June 2017. Google Scholar
  51. Toniann Pitassi and Robert Robere. Lifting Nullstellensatz to Monotone Span Programs over Any Field. In Proceedings of the 50th Annual ACM Symposium on Theory of Computing (STOC '18), pages 1207-1219, June 2018. Google Scholar
  52. Aaron Potechin. Bounds on Monotone Switching Networks for Directed Connectivity. In Proceedings of the 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS '10), pages 553-562, October 2010. Google Scholar
  53. Pavel Pudlák and Jirí Sgall. Algebraic Models of Computation and Interpolation for Algebraic Proof Systems. In Proof Complexity and Feasible Arithmetics, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279-296. American Mathematical Society, 1998. Available at URL: http://users.math.cas.cz/~pudlak/span.pdf.
  54. Robert Robere, Toniann Pitassi, Benjamin Rossman, and Stephen A. Cook. Exponential Lower Bounds for Monotone Span Programs. In Proceedings of the 57th Annual IEEE Symposium on Foundations of Computer Science (FOCS '16), pages 406-415, October 2016. Google Scholar
  55. John E. Savage and Sowmitri Swamy. Space-Time Tradeoffs for Oblivious Interger Multiplications. In Proceedings of the 6th International Colloquium on Automata, Languages and Programming (ICALP '79), pages 498-504, 1979. Google Scholar
  56. Ravi Sethi. Complete Register Allocation Problems. SIAM Journal on Computing, 4(3):226-248, September 1975. Google Scholar
  57. Sowmitri Swamy and John E. Savage. Space-Time Trade-offs on the FFT-algorithm. Technical Report CS-31, Brown University, 1977. Google Scholar
  58. Sowmitri Swamy and John E. Savage. Space-Time Tradeoffs for Linear Recursion. Mathematical Systems Theory, 16(1):9-27, 1983. Google Scholar
  59. Neil Thapen. A Trade-off Between Length and Width in Resolution. Theory of Computing, 12(5):1-14, August 2016. Google Scholar
  60. Martin Tompa. Time-Space Tradeoffs for Computing Functions, Using Connectivity Properties of Their Circuits. In Proceedings of the 10th annual ACM symposium on Theory of computing (STOC '78), pages 196-204, 1978. Google Scholar
  61. Ryan Williams. Space-Efficient Reversible Simulations. Technical report, Cornell University, 2000. Available at URL: http://web.stanford.edu/~rrwill/spacesim9_22.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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact