Document Open Access Logo

Depth Lower Bounds in Stabbing Planes for Combinatorial Principles

Authors Stefan Dantchev, Nicola Galesi, Abdul Ghani, Barnaby Martin

PDF
Thumbnail PDF

File

LIPIcs.STACS.2022.24.pdf
  • Filesize: 0.76 MB
  • 18 pages

Document Identifiers

Author Details

Stefan Dantchev
  • Department of Computer Science, Durham University, UK
Nicola Galesi
  • Department of Computer Science, Sapienza University of Rome, Italy
Abdul Ghani
  • Department of Computer Science, Durham University, UK
Barnaby Martin
  • Department of Computer Science, Durham University, UK

Acknowledgements

While finishing the writing of this manuscript we learned about [Noah Fleming et al., 2021] from Noah Fleming. We would like to thank him for answering some questions on his paper [Paul Beame et al., 2018], and sending us the manuscript [Noah Fleming et al., 2021] and for comments on a preliminary version of this work.

Cite AsGet BibTex

Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin. Depth Lower Bounds in Stabbing Planes for Combinatorial Principles. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.STACS.2022.24

Abstract

Stabbing Planes is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system established via communication complexity arguments. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner’s Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon’s combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • computational complexity
  • lower bounds
  • cutting planes
  • stabbing planes

Metrics

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

Related Versions

References

  1. Noga Alon and Zoltán Füredi. Covering the cube by affine hyperplanes. Eur. J. Comb., 14(2):79-83, 1993. URL: https://doi.org/10.1006/eujc.1993.1011.
  2. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In Anna R. Karlin, editor, 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, volume 94 of LIPIcs, pages 10:1-10:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.10.
  3. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Comb., 24(4):585-603, 2004. URL: https://doi.org/10.1007/s00493-004-0036-5.
  4. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Inf. Process. Lett., 110(23):1074-1077, 2010. URL: https://doi.org/10.1016/j.ipl.2010.09.007.
  5. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A characterization of tree-like resolution size. Inf. Process. Lett., 113(18):666-671, 2013. URL: https://doi.org/10.1016/j.ipl.2013.06.002.
  6. Joshua Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi. Rank bounds and integrality gaps for cutting planes procedures. Theory of Computing, 2(4):65-90, 2006. Google Scholar
  7. Teena Carroll, Joshua Cooper, and Prasad Tetali. Counting antichains and linear extensions in generalizations of the boolean lattice, 2009. Google Scholar
  8. W. Cook, C. R. Coullard, and G. Turán. On the complexity of cutting-plane proofs. Discrete Appl. Math., 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  9. Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In Shubhangi Saraf, editor, 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169 of LIPIcs, pages 34:1-34:35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CCC.2020.34.
  10. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  11. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  12. Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.6.
  13. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-cnfs are hard for cutting planes. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.19.
  14. Nicola Galesi, Pavel Pudlák, and Neil Thapen. The space complexity of cutting planes refutations. In David Zuckerman, editor, 30th Conference on Computational Complexity, CCC 2015, June 17-19, 2015, Portland, Oregon, USA, volume 33 of LIPIcs, pages 433-447. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CCC.2015.433.
  15. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  16. Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pages 220-228. IEEE, 1994. Google Scholar
  17. Henry A. Kautz and Bart Selman. Ten challenges redux: Recent progress in propositional reasoning and search. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 1-18. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_1.
  18. Arist Kojevnikov. Improved lower bounds for tree-like resolution over linear inequalities. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 70-79. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_10.
  19. Jan Krajícek. Discretely ordered modules as a first-order extension of the cutting planes proof system. J. Symb. Log., 63(4):1582-1596, 1998. URL: https://doi.org/10.2307/2586668.
  20. Jan Krajícek. Interpolation by a game. Math. Log. Q., 44:450-458, 1998. URL: https://doi.org/10.1002/malq.19980440403.
  21. Nathan Linial and Jaikumar Radhakrishnan. Essential covers of the cube by hyperplanes. Journal of Combinatorial Theory, Series A, 109(2):331-338, 2005. Google Scholar
  22. Lutz Mattner and Bero Roos. Maximal probabilities of convolution powers of discrete uniform distributions. Statistics & probability letters, 78(17):2992-2996, 2008. Google Scholar
  23. Fedor Part and Iddo Tzameret. Resolution with counting: Dag-like lower bounds and different moduli. Comput. Complex., 30(1):2, 2021. URL: https://doi.org/10.1007/s00037-020-00202-x.
  24. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-sat (preliminary version). In David B. Shmoys, editor, Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9-11, 2000, San Francisco, CA, USA, pages 128-136. ACM/SIAM, 2000. URL: http://dl.acm.org/citation.cfm?id=338219.338244.
  25. Mark Nicholas Charles Rhodes. On the chvátal rank of the pigeonhole principle. Theor. Comput. Sci., 410(27-29):2774-2778, 2009. URL: https://doi.org/10.1016/j.tcs.2009.03.035.
  26. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  27. Bart Selman, Henry A. Kautz, and David A. McAllester. Ten challenges in propositional reasoning and search. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes, pages 50-54. Morgan Kaufmann, 1997. URL: http://ijcai.org/Proceedings/97-1/Papers/008.pdf.
  28. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  29. Jacobus Hendricus van Lint and Richard Michael Wilson. A Course in Combinatorics. Cambridge University Press, Cambridge, U.K.; New York, 2001. Google Scholar
  30. Gal Yehuda and Amir Yehudayoff. A lower bound for essential covers of the cube. CoRR, abs/2105.13615, 2021. URL: http://arxiv.org/abs/2105.13615.
  31. Gal Yehuda and Amir Yehudayoff. A lower bound for essential covers of the cube. arXiv preprint, 2021. URL: http://arxiv.org/abs/2105.13615.
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