Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system. For size lower bounds these are established by monotone circuit arguments, while for depth these are found via communication complexity and protection. As such these bounds apply for lifted versions of combinatorial statements. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner's Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon's combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.

翻译：Stabbing Planes（也称为分支切割）是一种近期引入的证明系统，非正式地说，它通过分支整数线性不等式而非单个变量来扩展 DPLL 方法。目前已知用于证明 Stabbing Planes 大小和深度下界的技术，是切割平面证明系统所用方法的推广。对于大小下界，这些结论通过单调电路论证建立；对于深度下界，则借助通信复杂性和保护技术获得。因此这些下界适用于组合命题的提升版本。切割平面的秩下界也通过称为保护引理的几何论证得到。在本文中，我们引入两种新的几何方法来证明 Stabbing Planes 中任意公式的大小/深度下界：（1）反链方法，依赖于 Sperner 定理；（2）覆盖方法，利用布尔立方体被线性多项式本质覆盖的结果，而这又依赖于 Alon 的组合零点定理。我们展示了这些方法在鸽巢原理、Tseitin 矛盾式及线性序原理等组合原理类上的应用。通过第一种方法，我们证明了鸽巢原理的几乎线性大小下界和最优对数深度下界，以及完全图上的 Tseitin 矛盾式和线性序原理的类似下界。通过覆盖方法，我们得到了网格图上 Tseitin 矛盾式的 Stabbing Planes 证明的超线性大小下界和对数深度下界。