Document Open Access Logo

Cumulative Space in Black-White Pebbling and Resolution

Authors Joël Alwen, Susanna F. de Rezende, Jakob Nordström, Marc Vinyals

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2017.38.pdf
  • Filesize: 0.53 MB
  • 21 pages

Document Identifiers

Author Details

Joël Alwen
Susanna F. de Rezende
Jakob Nordström
Marc Vinyals

Cite AsGet BibTex

Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. Cumulative Space in Black-White Pebbling and Resolution. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ITCS.2017.38

Abstract

We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.
Keywords
  • pebble game
  • pebbling
  • proof complexity
  • space
  • cumulative space
  • clause space
  • resolution
  • parallel resolution

Metrics

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

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 Jeremiah Blocki. Efficiently computing data-independent memory-hard functions. In Proceedings of the 36th Annual International Cryptology Conference (CRYPTO '16), pages 241-271, August 2016. Google Scholar
  3. 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
  4. Joël Alwen, Jeremiah Blocki, and Krzysztof Pietrzak. Depth-robust graphs and their cumulative memory complexity. Technical Report 2016/875, Cryptology ePrint Archive, September 2016. Google Scholar
  5. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97), pages 203-208, July 1997. Google Scholar
  6. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. SIAM Journal on Computing, 45(4):1612-1645, August 2016. Preliminary version in STOC '12. Google Scholar
  7. 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
  8. Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Structures and Algorithms, 23(1):92-109, August 2003. Preliminary version in CCC '01. Google Scholar
  9. 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
  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. Ilario Bonacina. Total space in resolution is at least width squared. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP '16), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 56:1-56:13, July 2016. Google Scholar
  13. Ilario Bonacina and Nicola Galesi. A framework for space complexity in algebraic proof systems. Journal of the ACM, 62(3):23:1-23:20, June 2015. Preliminary version in ITCS '13. Google Scholar
  14. Ilario Bonacina, Nicola Galesi, and Neil Thapen. Total space in resolution. In Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS '14), pages 641-650, October 2014. Google Scholar
  15. María Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal on Computing, 30(5):1462-1484, 2000. Preliminary version in FOCS '98. Google Scholar
  16. 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
  17. 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
  18. Vašek Chvátal and Endre Szemerédi. Many hard examples for resolution. Journal of the ACM, 35(4):759-768, October 1988. Google Scholar
  19. Stephen A. Cook and Robert Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, March 1979. Google Scholar
  20. 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. Google Scholar
  21. Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How limited interaction hinders real communication (and what it means for proof and circuit complexity). In Proceedings of the 57th Annual IEEE Symposium on Foundations of Computer Science (FOCS '16), pages 295-304, October 2016. Google Scholar
  22. 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
  23. Patrick W. Dymond and Martin Tompa. Speedups of deterministic machines by synchronous parallel machines. Journal of Computer and System Sciences, 30(2):149-161, April 1985. Preliminary version in STOC '83. Google Scholar
  24. Paul Erdős, Ronald L. Graham, and Endre Szemerédi. On sparse graphs with dense long paths. Technical report, Stanford University, 1975. Google Scholar
  25. 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
  26. Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. Towards an understanding of polynomial calculus: New separations and lower bounds (Extended abstract). In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP '13), volume 7965 of Lecture Notes in Computer Science, pages 437-448. Springer, July 2013. Google Scholar
  27. Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space complexity in polynomial calculus. SIAM Journal on Computing, 44(4):1119-1153, August 2015. Preliminary version in CCC '12. Google Scholar
  28. 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
  29. Nicola Galesi, Pavel Pudlák, and Neil Thapen. The space complexity of cutting planes refutations. In Proceedings of the 30th Annual Computational Complexity Conference (CCC '15), volume 33 of Leibniz International Proceedings in Informatics (LIPIcs), pages 433-447, June 2015. Google Scholar
  30. John R. Gilbert and Robert Endre Tarjan. Variations of a pebble game on graphs. Technical Report STAN-CS-78-661, Stanford University, 1978. URL: http://infolab.stanford.edu/TR/CS-TR-78-661.html.
  31. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC '14), pages 847-856, May 2014. Google Scholar
  32. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  33. 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
  34. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity (Extended abstract). In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12), pages 233-248, May 2012. Google Scholar
  35. 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
  36. George Katsirelos, Ashish Sabharwal, Horst Samulowitz, and Laurent Simon. Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In Proceedings of the 27th AAAI Conference on Artificial Intelligence (AAAI '13), July 2013. Google Scholar
  37. 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
  38. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, May 1999. Preliminary version in ICCAD '96. Google Scholar
  39. Jakob Nordström. Narrow proofs may be spacious: Separating space and width in resolution. SIAM Journal on Computing, 39(1):59-121, May 2009. Preliminary version in STOC '06. Google Scholar
  40. Jakob Nordström. On the relative strength of pebbling and resolution. ACM Transactions on Computational Logic, 13(2):16:1-16:43, April 2012. Preliminary version in CCC '10. Google Scholar
  41. Jakob Nordström. Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science, 9:15:1-15:63, September 2013. Google Scholar
  42. 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/, 2017.
  43. Jakob Nordström and Johan Håstad. Towards an optimal separation of space and length in resolution. Theory of Computing, 9:471-557, May 2013. Preliminary version in STOC '08. Google Scholar
  44. 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
  45. Wolfgang J. Paul and Rüdiger Reischuk. On alternation II. A graph theoretic approach to determinism versus non-determinism. Acta Informatica, 14(4):391-403, 1980. Preliminary version in GITCS '79. Google Scholar
  46. 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
  47. 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
  48. John E. Savage. Models of Computation: Exploring the Power of Computing. Addison-Wesley, 1998. URL: http://www.modelsofcomputation.org.
  49. Georg Schnitger. On depth-reduction and grates. In Proceedings of the 24th Annual IEEE Symposium on Foundations of Computer Science (FOCS '83), pages 323-328, November 1983. Google Scholar
  50. Ravi Sethi. Complete register allocation problems. SIAM Journal on Computing, 4(3):226-248, September 1975. Google Scholar
  51. Sowmitri Swamy and John E. Savage. Space-time trade-offs on the FFT-algorithm. Technical Report CS-31, Brown University, 1977. Google Scholar
  52. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987. Google Scholar
  53. Leslie G. Valiant. Graph-theoretic arguments in low-level complexity. In Proceedings of the 6th International Symposium on Mathematical Foundations of Computer Science (MFCS '77), pages 162-176, September 1977. Google Scholar
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