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 $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.
翻译:我们开发了一个叫Stabbing Planes的新的半数值校验系统,称为Stabbing 平面图,它使用于整数编程的现代分支和切割算法正式化,并且具有DPLL 的现代SAT求解器风格。与DPLL一样,只有一条规则:当前多面图可以通过在不平等及其“内脏否定”上分支分解而进行。也就是说,我们可以(非必然地选择)一个具有整数系数的超平面 $ax\geq b$,它将多面图分为三块:满足 $ax\geq b$, 满足 $ax\leq b$ 的分支算法, 满足 $=leq b$, 和中平面图 $b - 1 < ax < b$。 因为中平面图中没有整数点可以安全丢弃, 算结果会在其他两个分支上递归。 当当前多面图为空时, 多面图可以平衡, 平面图可以检查三个部分: 我们的多面图中显示Stabing Steping Planes Stlakeles 可以有效地模拟切-calviews