ECCC-Report TR17-151https://eccc.weizmann.ac.il/report/2017/151Comments and Revisions published for TR17-151en-usFri, 17 Mar 2023 17:14:30 +0200
Revision 3
| Stabbing Planes |
Noah Fleming,
Paul Beame,
Russell Impagliazzo,
Robert Robere,
Antonina Kolokolova,
Toniann Pitassi,
Denis Pankratov
https://eccc.weizmann.ac.il/report/2017/151#revision3We 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 \geq b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x \geq b, the points satisfying a x \leq 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.Fri, 17 Mar 2023 17:14:30 +0200https://eccc.weizmann.ac.il/report/2017/151#revision3
Revision 2
| Stabbing Planes |
Noah Fleming,
Paul Beame,
Russell Impagliazzo,
Robert Robere,
Antonina Kolokolova,
Toniann Pitassi,
Denis Pankratov
https://eccc.weizmann.ac.il/report/2017/151#revision2We 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 \geq b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x \geq b, the points satisfying a x \leq 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.Sun, 27 Nov 2022 17:50:59 +0200https://eccc.weizmann.ac.il/report/2017/151#revision2
Revision 1
| Stabbing Planes |
Noah Fleming,
Paul Beame,
Russell Impagliazzo,
Robert Robere,
Antonina Kolokolova,
Toniann Pitassi,
Denis Pankratov
https://eccc.weizmann.ac.il/report/2017/151#revision1We 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 $ax \geq b$ with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying $ax \geq b$, the points satisfying $ax \leq b$, and the middle slab $b - 1 <
ax < 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 that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a tree-like variant of the R(CP) system of Krajicek98. As well, we show that it possesses short proofs of the canonical family of systems of $\mathbb{F}_2$-linear equations known as the Tseitin formulas.
Finally, we prove linear lower bounds on the rank of Stabbing Planes refutations by adapting lower bounds in communication complexity and use these bounds in order to show that Stabbing Planes proofs cannot be balanced. Wed, 18 May 2022 19:52:52 +0300https://eccc.weizmann.ac.il/report/2017/151#revision1
Paper TR17-151
| Stabbing Planes |
Noah Fleming,
Paul Beame,
Russell Impagliazzo,
Robert Robere,
Antonina Kolokolova,
Toniann Pitassi,
Denis Pankratov
https://eccc.weizmann.ac.il/report/2017/151We 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 \geq b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x \geq b, the points satisfying a x \leq 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.Mon, 09 Oct 2017 02:20:35 +0300https://eccc.weizmann.ac.il/report/2017/151