Document Open Access Logo

Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems

Authors Theodoros Papamakarios, Alexander Razborov

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.100.pdf
  • Filesize: 0.69 MB
  • 20 pages

Document Identifiers

Author Details

Theodoros Papamakarios
  • Department of Computer Science, University of Chicago, IL, USA
Alexander Razborov
  • University of Chicago, IL, USA
  • Steklov Mathematical Institute, Moscow, Russia

Cite As Get BibTex

Theodoros Papamakarios and Alexander Razborov. Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 100:1-100:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.100

Abstract

We identify two new big clusters of proof complexity measures equivalent up to polynomial and log n factors. The first cluster contains, among others, the logarithm of tree-like resolution size, regularized (that is, multiplied by the logarithm of proof length) clause and monomial space, and clause space, both ordinary and regularized, in regular and tree-like resolution. As a consequence, separating clause or monomial space from the (logarithm of) tree-like resolution size is the same as showing a strong trade-off between clause or monomial space and proof length, and is the same as showing a super-critical trade-off between clause space and depth. The second cluster contains width, Σ₂ space (a generalization of clause space to depth 2 Frege systems), both ordinary and regularized, as well as the logarithm of tree-like size in the system R(log). As an application of some of these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In terms of lower bounds, we show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4. We introduce on our way yet another proof complexity measure intermediate between depth and the logarithm of tree-like size that might be of independent interest.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Resolution
  • Size-Space Trade-offs

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 Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM Journal of Computing, 31:1184-1211, 2002. Google Scholar
  2. Albert Atserias and Victor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74:323-334, 2008. Google Scholar
  3. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing, pages 813-822, 2013. Google Scholar
  4. Eli Ben-Sasson. Size-space tradeoffs for resolution. SIAM Journal of Computing, 38, 2009. Google Scholar
  5. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24:585-603, 2004. Google Scholar
  6. 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, pages 709-718, 2008. Google Scholar
  7. 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, pages 401-416, 2011. Google Scholar
  8. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48:149-169, 2001. Google Scholar
  9. Ilario Bonacina. Total space in resolution is at least width squared. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, volume 55, pages 56:1-56:13, 2016. Google Scholar
  10. Maria Luisa Bonet and Nicola Galesi. Optimality of size-width tradeoffs for resolution. Computational Complexity, 10:261-276, 2002. Google Scholar
  11. Samuel Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 7, pages 233-350. IOS Press, 2nd edition, 2021. Google Scholar
  12. 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, pages 174-183, 1996. Google Scholar
  13. Stephen Cook and Robert Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36-50, 1979. Google Scholar
  14. Stephen Cook and Ravi Sethi. Storage requirements for deterministic polynomial time recognizable languages. Journal of Computer and System Sciences, 13:25-37, 1976. Google Scholar
  15. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theoretical Computer Science, 321:347-370, 2004. Google Scholar
  16. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171:84-97, 2001. Google Scholar
  17. Juan Luis Esteban and Jacobo Torán. A combinatorial characterization of treelike resolution space. Information Processing Letters, 87:295-300, 2003. Google Scholar
  18. Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From small space to small width in resolution. ACM Transactions of Computational Logic, 16:28:1-28:15, 2015. Google Scholar
  19. Nicola Galesi, Leszek Kołodziejczyk, and Neil Thapen. Polynomial calculus space and resolution width. In Proceedings of the 60th Annual IEEE Symposium on Foundations of Computer Science, pages 1325-1337, 2019. Google Scholar
  20. Nicola Galesi and Neil Thapen. Resolution and pebbling games. In Proceedings of the 8th Theory and Applications of Satisfiability Testing Conference, volume 3569, pages 76-90, 2005. Google Scholar
  21. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM Journal of Computing, 47:1778-1806, 2018. Google Scholar
  22. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing Conference, pages 233-248, 2012. Google Scholar
  23. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Computational Complexity, 8:127-144, 1999. Google Scholar
  24. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 59:73-86, 1994. Google Scholar
  25. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123-140, 2001. Google Scholar
  26. Jan Krajíček. Proof Complexity. Cambridge University Press, 2019. Google Scholar
  27. Massimo Lauria. A note about k-DNF resolution. Information Processing Letters, 137:33-39, 2018. Google Scholar
  28. Thomas Lengauer and Robert Tarjan. Asymptotically tight bounds on time-space trade-offs in a pebble game. Journal of the ACM, 29:1087-1130, 1982. Google Scholar
  29. Bruno Loff and Sagnik Mukhopadhyay. Lifting theorems for equality. In Proceedings of the 36th International Symposium on Theoretical Aspects of Computer Science, volume 126, pages 50:1-50:19, 2019. Google Scholar
  30. Jakob Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, 9, 2013. Google Scholar
  31. Jakob Nordström and Johan Håstad. Towards an optimal separation of space and length in resolution. Theory of Computing, 9:471-557, 2013. Google Scholar
  32. Theodoros Papamakarios. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. Electronic Colloqium on Computational Complexity, Report No. 176, 2021. Google Scholar
  33. Theodoros Papamakarios and Alexander Razborov. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. Electronic Colloqium on Computational Complexity, Report No. 74, 2021. Google Scholar
  34. Wolfgang Paul, Robert Tarjan, and James Celoni. Space bounds for a game on graphs. Mathematical Systems Theory, 10:239-251, 1977. Google Scholar
  35. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-SAT. In Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms, pages 128-136, 2000. Google Scholar
  36. Alexander Razborov. A new kind of tradeoffs in propositional proof complexity. Journal of the ACM, 63:16:1-16:14, 2016. Google Scholar
  37. Alexander Razborov. On space and depth in resolution. Computational Complexity, 27:511-559, 2018. Google Scholar
  38. Alasdair Urquhart. The depth of resolution proofs. Studia Logica, 99:349-364, 2011. 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 About DROPS Imprint Privacy Contact