Document Open Access Logo

Total Space in Resolution Is at Least Width Squared

Author Ilario Bonacina

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.56.pdf
  • Filesize: 0.51 MB
  • 13 pages

Document Identifiers

Author Details

Ilario Bonacina

Cite As Get BibTex

Ilario Bonacina. Total Space in Resolution Is at Least Width Squared. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 56:1-56:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.56

Abstract

Given an unsatisfiable k-CNF formula phi we consider two complexity measures in Resolution: width and total space. The width is the minimal W such that there exists a Resolution refutation of phi with clauses of at most W literals. The total space is the minimal size T of a memory used to write down a Resolution refutation of phi where the size of the memory is measured as the total number of literals it can contain. We prove that T = Omega((W - k)^2).

Subject Classification

Keywords
  • Resolution
  • width
  • total space

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 J. Comput., 31(4):1184-1211, 2002. URL: http://dx.doi.org/10.1137/S0097539700366735.
  2. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. URL: http://dx.doi.org/10.1016/j.jcss.2007.06.025.
  3. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. In IEEE 29th Conference on Computational Complexity, CCC 2014, Vancouver, BC, Canada, June 11-13, 2014, pages 286-297. IEEE, 2014. URL: http://dx.doi.org/10.1109/CCC.2014.36.
  4. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island., pages 203-208. AAAI Press / The MIT Press, 1997. URL: http://www.aaai.org/Library/AAAI/1997/aaai97-032.php.
  5. Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In Howard J. Karloff and Toniann Pitassi, editors, Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19-22, 2012, pages 213-232. ACM, 2012. URL: http://dx.doi.org/10.1145/2213977.2213999.
  6. Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks. On the complexity of unsatisfiability proofs for random k-CNF formulas. In Jeffrey Scott Vitter, editor, Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23-26, 1998, pages 561-571. ACM, 1998. URL: http://dx.doi.org/10.1145/276698.276870.
  7. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 813-822. ACM, 2013. URL: http://dx.doi.org/10.1145/2488608.2488711.
  8. Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Struct. Algorithms, 23(1):92-109, 2003. URL: http://dx.doi.org/10.1002/rsa.10089.
  9. Eli Ben-Sasson and Jakob Nordström. Understanding space in resolution: optimal lower bounds and exponential trade-offs. In Peter Bro Miltersen, Rüdiger Reischuk, Georg Schnitger, and Dieter van Melkebeek, editors, Computational Complexity of Discrete Problems, 14.09.-19.09.2008, volume 08381 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2008. URL: http://drops.dagstuhl.de/opus/volltexte/2008/1781/.
  10. Eli Ben-Sasson and Jakob Nordström. A space hierarchy for k-DNF resolution. Electronic Colloquium on Computational Complexity (ECCC), 16:47, 2009. URL: http://eccc.hpi-web.de/report/2009/047.
  11. Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Bernard Chazelle, editor, Innovations in Computer Science - ICS 2010, Tsinghua University, Beijing, China, January 7-9, 2011. Proceedings, pages 401-416. Tsinghua University Press, 2011. URL: http://conference.itcs.tsinghua.edu.cn/ICS2011/content/papers/3.html.
  12. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: http://dx.doi.org/10.1145/375827.375835.
  13. Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. Space proof complexity for random 3-CNFs. CoRR, abs/1503.01613, 2015. URL: http://arxiv.org/abs/1503.01613.
  14. Olaf Beyersdorff and Oliver Kullmann. Hardness measures and resolution lower bounds. CoRR, abs/1310.7627, 2013. URL: http://arxiv.org/abs/1310.7627.
  15. Olaf Beyersdorff and Oliver Kullmann. Unified characterisations of resolution hardness measures. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 170-187. Springer, 2014. Google Scholar
  16. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. University of Chicago. Google Scholar
  17. Ilario Bonacina. Space in weak propositional proof systems. PhD thesis, Department of Computer Science, Sapienza University of Rome, 12 2015. Google Scholar
  18. Ilario Bonacina. Total space in resolution is at least width squared. Electronic Colloquium on Computational Complexity (ECCC), 2016. URL: http://eccc.hpi-web.de/report/2016/057/.
  19. Ilario Bonacina and Nicola Galesi. A framework for space complexity in algebraic proof systems. J. ACM, 62(3):23, 2015. URL: http://dx.doi.org/10.1145/2699438.
  20. Ilario Bonacina, Nicola Galesi, and Neil Thapen. Total space in resolution. In 55th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2014, Philadelphia, PA, USA, October 18-21, 2014, pages 641-650. IEEE Computer Society, 2014. URL: http://dx.doi.org/10.1109/FOCS.2014.74.
  21. Maria Luisa Bonet and Nicola Galesi. Optimality of size-width tradeoffs for resolution. Computational Complexity, 10(4):261-276, 2001. URL: http://dx.doi.org/10.1007/s000370100000.
  22. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: http://dx.doi.org/10.1145/368273.368557.
  23. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: http://dx.doi.org/10.1145/321033.321034.
  24. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theor. Comput. Sci., 321(2-3):347-370, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.04.004.
  25. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Inf. Comput., 171(1):84-97, 2001. URL: http://dx.doi.org/10.1006/inco.2001.2921.
  26. Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. From small space to small width in resolution. In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 300-311. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2014.300.
  27. Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space complexity in polynomial calculus. SIAM J. Comput., 44(4):1119-1153, 2015. URL: http://dx.doi.org/10.1137/120895950.
  28. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: http://dx.doi.org/10.1016/0304-3975(85)90144-6.
  29. Oliver Kullmann. Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Electronic Colloquium on Computational Complexity (ECCC), (41), 1999. URL: http://eccc.hpi-web.de/eccc-reports/1999/TR99-041/index.html.
  30. Oliver Kullmann. An improved version of width restricted resolution. In AMAI, 2000. URL: http://rutcor.rutgers.edu/~amai/aimath00/regular/kullmann.ps.
  31. Oliver Kullmann. Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intell., 40(3-4):303-352, 2004. URL: http://dx.doi.org/10.1023/B:AMAI.0000012871.08577.0b.
  32. 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 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: http://dx.doi.org/10.1145/378239.379017.
  33. Jakob Nordström. Narrow proofs may be spacious: Separating space and width in resolution. SIAM J. Comput., 39(1):59-121, 2009. URL: http://dx.doi.org/10.1137/060668250.
  34. Jakob Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, 9(3), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(3:15)2013.
  35. Jakob Nordström. On the interplay between proof complexity and SAT solving. ACM SIGLOG News, 2(3):19-44, August 2015. Google Scholar
  36. Jakob Nordström and Johan Håstad. Towards an optimal separation of space and length in resolution. Theory of Computing, 9:471-557, 2013. URL: http://dx.doi.org/10.4086/toc.2013.v009a014.
  37. Alexander A. Razborov. Proof complexity of pigeonhole principles. In Werner Kuich, Grzegorz Rozenberg, and Arto Salomaa, editors, Developments in Language Theory, 5th International Conference, DLT 2001, Vienna, Austria, July 16-21, 2001, Revised Papers, volume 2295 of Lecture Notes in Computer Science, pages 100-116. Springer, 2001. Google Scholar
  38. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. URL: http://dx.doi.org/10.1145/321250.321253.
  39. Uwe Schöning. Resolution proofs, exponential bounds, and Kolmogorov complexity. In Igor Prívara and Peter Ruzicka, editors, Mathematical Foundations of Computer Science 1997, 22nd International Symposium, MFCS'97, Bratislava, Slovakia, August 25-29, 1997, Proceedings, volume 1295 of Lecture Notes in Computer Science, pages 110-116. Springer, 1997. URL: http://dx.doi.org/10.1007/BFb0029954.
  40. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: http://dx.doi.org/10.1109/12.769433.
  41. G.S. Tseitin. On the complexity of derivation in propositional calculus. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning, Symbolic Computation, pages 466-483. Springer Berlin Heidelberg, 1983. URL: http://dx.doi.org/10.1007/978-3-642-81955-1_28,
  42. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: http://dx.doi.org/10.1145/7531.8928.
  43. Alasdair Urquhart. The depth of resolution proofs. Studia Logica, 99(1-3):349-364, 2011. URL: http://dx.doi.org/10.1007/s11225-011-9356-9.
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