Document Open Access Logo

Stabbing Planes

Authors Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, Robert Robere

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2018.10.pdf
  • Filesize: 0.58 MB
  • 20 pages

Document Identifiers

Author Details

Paul Beame
Noah Fleming
Russell Impagliazzo
Antonina Kolokolova
Denis Pankratov
Toniann Pitassi
Robert Robere

Cite As Get BibTex

Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing Planes. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ITCS.2018.10

Abstract

We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane a x >= b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x >= b, the points satisfying a x <= b-1, and the middle slab b-1 < a x < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show somewhat surprisingly that Stabbing Planes can efficiently simulate Cutting Planes, and moreover, is strictly stronger than Cutting Planes under a reasonable conjecture. We prove linear lower bounds on the rank of Stabbing Planes refutations, by adapting
a lifting argument in communication complexity.

Subject Classification

Keywords
  • Complexity Theory
  • Proof Complexity
  • Communication Complexity
  • Cutting Planes
  • Semi-Algebraic Proof Systems
  • Pseudo Boolean Solvers
  • SAT solvers
  • Inte

Metrics

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

References

  1. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. CoRR, abs/1710.03219, 2017. URL: http://arxiv.org/abs/1710.03219.
  2. Paul Beame, Trinh Huynh, and Toniann Pitassi. Hardness amplification in proof complexity. In STOC'10, pages 87-96, 2010. Google Scholar
  3. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, 2004. Google Scholar
  4. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  5. Daniel Le Berre. Handling Pseudo-Boolean constraints in a CDCL solver: a practical survey. In Dagstuhl Seminar 15171: Theory and Practice of SAT Solving, April 2015. Google Scholar
  6. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput., 30(5):1462-1484, 2000. Google Scholar
  7. 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
  8. William Cook, Collette Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. Google Scholar
  9. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, jul 1962. Google Scholar
  10. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. Google Scholar
  11. Susanna F. de Rezende, Jakob Nordstrom, and Marc Vinyals. How limited interaction hinders real communication (and what it means for proof and circuit complexity). In FOCS'16, pages 295-304, 2016. Google Scholar
  12. Yuval Filmus, Pavel Hrubes, and Massimo Lauria. Semantic versus syntactic cutting planes. In STACS'16, pages 35:1-35:13, 2016. Google Scholar
  13. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random cnfs are hard for cutting planes. Electronic Colloquium on Computational Complexity (ECCC), 24:45, 2017. Google Scholar
  14. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In STOC'14, pages 847-856, 2014. Google Scholar
  15. Mika Göös, Toniann Pitassi, and Thomas Watson. Deterministic communication vs. partition number. In FOCS'15, pages 1077-1088, 2015. Google Scholar
  16. Pavel Hrubes and Pavel Pudlák. A note on monotone real circuits. Electronic Colloquium on Computational Complexity (ECCC), 24:48, 2017. Google Scholar
  17. Pavel Hrubeš and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. Electronic Colloquium on Computational Complexity (ECCC), 24:42, 2017. Google Scholar
  18. Trinh Huynh and Jakob Nordstrom. On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity. In STOC '12, pages 233-248, 2012. Google Scholar
  19. IBM ILOG. The CPLEX optimizer. URL: https://www-01.ibm.com/software/commerce/optimization/cplex-optimizer/.
  20. Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In LICS '94, pages 220-228, 1994. Google Scholar
  21. Stasys Jukna. Boolean function complexity : advances and frontiers. Algorithms and combinatorics. Springer, 2012. Google Scholar
  22. Arist Kojevnikov. Improved lower bounds for tree-like resolution over linear inequalities. In SAT'07, pages 70-79, 2007. Google Scholar
  23. Jan Krajícek. Discretely Ordered Modules as a First-Order Extension of the Cutting Planes Proof System. The Journal of Symbolic Logic, 63(4):1582-1596, 1998. Google Scholar
  24. Jan Krajícek. Interpolation by a Game. Mathematical Logic Quarterly, 44:450-458, 1998. Google Scholar
  25. Saburo Muroga. Threshold logic and its applications. Wiley-Interscience, 1972. Google Scholar
  26. Noam Nisan. The communication complexity of threshold gates. In In Proceedings of “Combinatorics, Paul Erdos is Eighty, pages 301-315, 1994. Google Scholar
  27. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  28. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Combinatorica, 19(3):403-435, 1999. Google Scholar
  29. Olivier Roussel and Vasco M Manquinho. Pseudo-Boolean and Cardinality Constraints. In Handbook of satisfiability, pages 695-733. IOS Press, 2009. Google Scholar
  30. Günter M. Ziegler. Lectures on Polytopes. Springer-Verlag, New York, 1995. 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