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

TL;DR
Stabbing Planes is a new proof system modeling modern branch-and-cut algorithms for integer programming, capable of simulating cutting plane proofs, with proven lower bounds on proof complexity and communication complexity.
Contribution
It introduces Stabbing Planes, a semi-algebraic proof system that formalizes branch-and-cut methods and demonstrates equivalence to certain proof systems, with new lower bounds on proof and communication complexity.
Findings
Stabbing Planes can simulate Cutting Planes proofs efficiently.
It is equivalent to a tree-like RCP system.
Linear lower bounds on proof rank and unbalanced proofs are established.
Abstract
We develop a new semi-algebraic proof system called Stabbing Planes which formalizes modern branch-and-cut algorithms for integer programming and is in the style of DPLL-based modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying , the points satisfying , and the middle slab . 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 that Stabbing Planes can…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
