Document Open Access Logo

The Space Complexity of Cutting Planes Refutations

Authors Nicola Galesi, Pavel Pudlák, Neil Thapen

PDF
Thumbnail PDF

File

LIPIcs.CCC.2015.433.pdf
  • Filesize: 462 kB
  • 15 pages

Document Identifiers

Author Details

Nicola Galesi
Pavel Pudlák
Neil Thapen

Cite AsGet BibTex

Nicola Galesi, Pavel Pudlák, and Neil Thapen. The Space Complexity of Cutting Planes Refutations. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 433-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CCC.2015.433

Abstract

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.
Keywords
  • Proof Complexity
  • Cutting Planes
  • Space Complexity

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. Google Scholar
  2. Chris Beck, Jakob Nordstrom, and Bangsheng Tang. Some trade-off results for polynomial calculus. In Proceedings of the 45th Annual Symposium on the Theory of Computing (STOC 2013), pages 813-822, 2013. Google Scholar
  3. Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Structures and Algorithms, 23(1):92-109, 2003. Google Scholar
  4. 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, 2011. Google Scholar
  5. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Google Scholar
  6. Ilario Bonacina and Nicola Galesi. Pseudo-partitions, transversality and locality: a combinatorial characterization for the space measure in algebraic proof systems. In Proceedings of the 4th conference on Innovations in Theoretical Computer Science (ITCS '13), pages 455-472, 2013. Google Scholar
  7. Ilario Bonacina, Nicola Galesi, and Neil Thapen. Total space in resolution. In 55th IEEE Annual Symposium on Foundations of Computer Science (FOCS 2014), pages 641-650, 2014. Google Scholar
  8. Maria Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. Journal of Symbolic Logic, 62(03):708-728, 1997. Google Scholar
  9. Samuel R Buss and Peter Clote. Cutting planes, connectivity, and threshold logic. Archive for Mathematical Logic, 35(1):33-62, 1996. Google Scholar
  10. Vašek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics, 4(4):305-337, 1973. Google Scholar
  11. William Cook. Cutting-plane proofs in polynomial space. Mathematical Programming, 47(1-3):11-18, 1990. Google Scholar
  12. William Cook, Collette R Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. Google Scholar
  13. Stefan Dantchev and Barnaby Martin. Cutting planes and the parameter cutwidth. Theory of Computing Systems, 51(1):50-64, 2012. Google Scholar
  14. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171(1):84-97, 2001. Google Scholar
  15. Ralph E Gomory. An algorithm for integer solutions to linear programs. Recent Advances in Mathematical Programming, 64:260-302, 1963. Google Scholar
  16. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In Proceedings of the 46th Annual Symposium on the Theory of Computing (STOC 2014), pages 847-856, 2014. Google Scholar
  17. Armin Haken and Stephen A Cook. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences, 58(2):326-335, 1999. Google Scholar
  18. Edward A Hirsch and Sergey I Nikolenko. Simulating cutting plane proofs with restricted degree of falsity by resolution. In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), pages 135-142, 2005. Google Scholar
  19. John N Hooker. Generalized resolution for 0-1 linear inequalities. Annals of Mathematics and Artificial Intelligence, 6(1-3):271-286, 1992. Google Scholar
  20. 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 Symposium on the Theory of Computing (STOC 2012), pages 233-248, 2012. Google Scholar
  21. Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS '94), pages 220-228, 1994. Google Scholar
  22. Jakob Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, 9(3):15, 2013. Google Scholar
  23. Jakob Nordström. A (biased) proof complexity survey for SAT practitioners. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), volume 8561, pages 1-6, 2014. Google Scholar
  24. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(03):981-998, 1997. 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