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-1$, 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 RCP 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. In doing so, we show that real communication protocols cannot be balanced and establish the first lower bound on the real communication complexity of the set disjointness function.

翻译：我们提出一种新的半代数证明系统——刺平面(Stabbing Planes)，该形式化了整数规划中的现代分支切割算法，并采用了基于DPLL的现代SAT求解器风格。与DPLL类似，系统仅包含单一规则：当前多面体可通过关于一个不等式及其"整数否定"进行分支而细分。即，我们（非确定性选择）一个整系数超平面$ax \geq b$，将多面体划分为三个部分：满足$ax \geq b$的多面体点集，满足$ax \leq b-1$的点集，以及中间层$b - 1 < ax < b$。由于中间层不含整数点，可安全舍弃，算法继续对另外两个分支递归执行。每个路径在当前多面体为空时终止，该过程可在多项式时间内检验。本文主要结果包括：证明刺平面系统能够有效模拟切割平面证明系统，且等价于[Krajicek98]中RCP系统的树状变体；同时证明该系统对标准$\mathbb{F}_2$线性方程组族（即Tseitin公式）具有简短证明。最后，通过适配通信复杂度下界，证明刺平面反驳证明的秩具有线性下界，并利用该下界证明刺平面证明不可平衡。在此过程中，我们揭示了实数通信协议不可平衡，并建立了集合不相交函数实数通信复杂度的首个下界。