Document Open Access Logo

Supercritical Space-Width Trade-Offs for Resolution

Authors Christoph Berkholz, Jakob Nordström

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.57.pdf
  • Filesize: 499 kB
  • 14 pages

Document Identifiers

Author Details

Christoph Berkholz
Jakob Nordström

Cite As Get BibTex

Christoph Berkholz and Jakob Nordström. Supercritical Space-Width Trade-Offs for Resolution. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 57:1-57:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.57

Abstract

We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben-Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov’s new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].

Subject Classification

Keywords
  • Proof complexity
  • resolution
  • space
  • width
  • trade-offs
  • supercritical

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. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, May 2008. Preliminary version in CCC'03. Google Scholar
  3. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC'14), pages 286-297, June 2014. Google Scholar
  4. 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
  5. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC'12), pages 213-232, May 2012. Google Scholar
  6. Paul Beame, Richard Karp, Toniann Pitassi, and Michael Saks. The efficiency of resolution and Davis-Putnam procedures. SIAM Journal on Computing, 31(4):1048-1075, 2002. Preliminary versions of these results appeared in FOCS'96 and STOC'98. 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. Size-space tradeoffs for resolution. SIAM Journal on Computing, 38(6):2511-2525, May 2009. Preliminary version in STOC'02. Google Scholar
  9. 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
  10. 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
  11. 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
  12. 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
  13. Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. Space proof complexity for random 3-CNFs. Technical Report 1503.01613, arXiv.org, April 2015. Google Scholar
  14. Christoph Berkholz. On the complexity of finding narrow proofs. In Proceedings of the 53rd Annual IEEE Symposium on Foundations of Computer Science (FOCS'12), pages 351-360, October 2012. Google Scholar
  15. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  16. 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), July 2016. To appear. Google Scholar
  17. 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
  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. 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
  20. 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
  21. 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
  22. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. Google Scholar
  23. 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
  24. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  25. Alexander Hertel. Applications of Games to Propositional Proof Complexity. PhD thesis, University of Toronto, May 2008. Available at URL: http://www.cs.utoronto.ca/~ahertel/.
  26. 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
  27. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC'01), pages 530-535, June 2001. Google Scholar
  28. 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
  29. 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
  30. 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
  31. Alexander A. Razborov. An ultimate trade-off in propositional proof complexity. Technical Report TR15-033, Electronic Colloquium on Computational Complexity (ECCC), March 2015. Google Scholar
  32. Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. Journal of the ACM, 63:16:1-16:14, April 2016. Google Scholar
  33. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965. Google Scholar
  34. Neil Thapen. A trade-off between length and width in resolution. Technical Report TR14-137, Electronic Colloquium on Computational Complexity (ECCC), October 2014. Google Scholar
  35. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987. 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