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.

Abstract. We consider proof complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this proof complexity with the normal unary encoding in several refutation systems, based on Resolution and Sherali–Adams. We first consider [Formula: see text], which is an extension of Resolution working on [Formula: see text]-DNFs (Disjunctive Normal Form formulas). We prove an exponential lower bound of [Formula: see text] for the size of refutations of the binary version of the [Formula: see text]-Clique Principle in [Formula: see text], where [Formula: see text] and [Formula: see text] is a doubly exponential function. Our result improves that of Lauria et al., who proved a similar lower bound for [Formula: see text], i.e., Resolution. For the [Formula: see text]-Clique and other principles we study, we show how lower bounds in Resolution for the unary version follow from lower bounds in [Formula: see text] for the binary version, so we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the (weak) Pigeonhole Principle [Formula: see text]. We prove that for any [Formula: see text], [Formula: see text] requires refutations of size [Formula: see text] in [Formula: see text] for [Formula: see text]. Our lower bound cannot be improved substantially with the same method since for [Formula: see text] we can prove there are [Formula: see text] size refutations of [Formula: see text] in [Formula: see text]. This is a consequence of the same upper bound for the unary weak Pigeonhole Principle of Buss and Pitassi. We contrast unary versus binary encoding in the Sherali–Adams (SA) refutation system where we prove lower bounds for both rank and size. For the unary encoding of the Pigeonhole Principle and the Ordering Principle, it is known that linear rank is required for refutations in SA, although both admit refutations of polynomial size. We prove that the binary encoding of the (weak) Pigeonhole Principle [Formula: see text] requires exponentially sized (in [Formula: see text]) SA refutations, whereas the binary encoding of the Ordering Principle admits logarithmic rank, polynomially sized SA refutations. We continue by considering a natural refutation system we call “SA+Squares,” which is intermediate between SA and Lasserre (Sum-of-Squares). This has been studied under the name static-[Formula: see text] by Grigoriev et al. In this system, the unary encoding of the Linear Ordering Principle [Formula: see text] requires [Formula: see text] rank while the unary encoding of the Pigeonhole Principle becomes constant rank. Since Potechin has shown that the rank of [Formula: see text] in Lasserre is [Formula: see text], we uncover an almost quadratic separation between SA+Squares and Lasserre in terms of rank. Grigoriev et al. noted that the unary Pigeonhole Principle has rank 2 in SA+Squares and therefore polynomial size. Since we show the same applies to the binary [Formula: see text], we deduce an exponential separation for size between SA and SA+Squares.

Stabbing Planes 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 established via communication complexity arguments. 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.