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证明的超线性规模下界与对数深度下界。