Department of Computer Science, Durham University, UK
<EMAIL_ADDRESS>Department of Computer Science, Sapienza Università
di Roma<EMAIL_ADDRESS>Department of Computer Science, Durham
University, UK<EMAIL_ADDRESS>Department of Computer Science, Durham
University, UK<EMAIL_ADDRESS>S. Dantchev, A. Ghani, N. Galesi
and B. Martin [500]Theory of computation Computational complexity and
cryptography [500]Theory of computation Proof complexity

###### Acknowledgements.

John Q. Open and Joan R. Access 2 42nd Conference on Very Important Topics
(CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging, United
Kingdom 42 23

# Depth lower bounds in Stabbing Planes for combinatorial principles

Stefan Dantchev  Nicola Galesi  Abdul Ghani  Barnaby Martin

###### Abstract

Stabbing Planes (also known as Branch and Cut) is a proof system introduced
very recently which, informally speaking, extends the
$\operatorname{\mathsf{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. As such they work for the lifted version 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.

###### keywords:

proof complexity, computational complexity, lower bounds, cutting planes,
stabbing planes

###### category:

##  1 Introduction

Finding a satisfying assignment for a propositional formula
($\operatorname{\mathsf{SAT}}$) is a central component for many
computationally hard problems. Despite being older than 50 years and
exponential time in the worst-case, the $\operatorname{\mathsf{DPLL}}$
algorithm [7, 8, 20] is the core of essentially all high performance modern
$\operatorname{\mathsf{SAT}}$-solvers. $\operatorname{\mathsf{DPLL}}$ is a
recursive boolean method: at each call one variable $x$ of the formula
$\mathcal{F}$ is chosen and the search recursively branches into the two cases
obtained by setting $x$ respectively to $1$ and $0$ in $\mathcal{F}$. On
$\operatorname{\mathsf{UNSAT}}$ formulas $\operatorname{\mathsf{DPLL}}$
performs the worst and it is well-known that the execution trace of the
$\operatorname{\mathsf{DPLL}}$ algorithm running on an unsatisfiable formula
$\mathcal{F}$ is nothing more than a treelike refutation of $\mathcal{F}$ in
the proof system of Resolution [20] ($\operatorname{\mathsf{Res}}$).

Since $\operatorname{\mathsf{SAT}}$ can be viewed as an optimization problem
the question whether Integer Linear Programming
($\operatorname{\mathsf{ILP}}$) can be made feasible for satisfiability
testing received a lot of attention and is considered among the most
challenging problems in local search [21, 12]. One proof system capturing
$\operatorname{\mathsf{ILP}}$ approaches to $\operatorname{\mathsf{SAT}}$ is
Cutting Planes, a system whose main rule implements the rounding (or Chvátal
cut) approach to $\operatorname{\mathsf{ILP}}$. Cutting planes works with
integer linear inequalities of the form $\mathbf{a}\mathbf{x}\leq b$, with
$\mathbf{a},b$ integers, and, like resolution, is a sound and complete
refutational proof system for $\operatorname{\mathsf{CNF}}$ formulas: indeed a
clause $C=(x_{1}\vee\ldots\vee x_{r}\vee\neg y_{1}\vee\ldots\vee\neg y_{s})$
can be written as the integer inequality $\mathbf{y}-\mathbf{x}\leq s-1$.

Beame et al. [2], extended the idea of $\operatorname{\mathsf{DPLL}}$ to a
more general proof strategy based on $\operatorname{\mathsf{ILP}}$. Instead of
branching only on a variable as in resolution, in this method one considers a
pair $(\mathbf{a},b)$, with $\mathbf{a}\in\mathbb{Z}^{n}$ and
$b\in\mathbb{Z}$, and branches limiting the search to the two half-planes:
$\mathbf{a}\mathbf{x}\leq b-1$ and $\mathbf{a}\mathbf{x}\geq b$. A path
terminates when the $\operatorname{\mathsf{LP}}$ defined by the inequalities
in $\mathcal{F}$ and those forming the path is infeasible. This method can be
made into a refutational treelike proof system for
$\operatorname{\mathsf{UNSAT}}$ CNF’s called Stabbing planes
($\operatorname{\mathsf{SP}}$) ([2]) and it turned out that it is polynomially
equivalent to the treelike version of
$\operatorname{\mathsf{Res}}(\operatorname{\mathsf{CP}})$, a proof system
introduced by Krajíček [14] where clauses are disjunction of linear
inequalities.

In this work we consider the complexity of proofs in
$\operatorname{\mathsf{SP}}$ focusing on the length, i.e. the number of
queries in the proof; the depth (called also rank in [2]), i.e. the length of
the longest path in the proof tree; and the size, i.e. the bit size of all the
coefficients appearing in the proof.

###  1.1 Previous works and motivations

After its introduction as a proof system in the work [2] by Beame, Fleming,
Impagliazzo, Kolokolova, Pankratov, Pitassi and Robere, Stabbing Planes
received great attention. The quasipolynomial upper bound for the size of
refuting Tseitin contradictions in $\operatorname{\mathsf{SP}}$ given in [2]
was surprisingly extended to $\operatorname{\mathsf{CP}}$ in the work of [6]
of Dadush and Tiwari refuting a long-standing conjecture. Recently in [9],
Fleming, Göös, Impagliazzo, Pitassi, Robere, Tan and Wigderson were further
developing the initial results proved in [2] making important progress on the
question whether all Stabbing Planes proofs can be somehow efficiently
simulated by Cutting Planes.

Significant lower bounds for size can be obtained in
$\operatorname{\mathsf{SP}}$, but in a limited way, using modern developments
of a technique for $\operatorname{\mathsf{CP}}$ based on communication
complexity of search problems introduced by Impagliazzo, Pitassi, Urquhart in
[11]: in [2] it is proven that size $S$ and depth $D$
$\operatorname{\mathsf{SP}}$ refutations imply treelike
$\operatorname{\mathsf{Res}}(\operatorname{\mathsf{CP}})$ proofs of size
$O(S)$ and width $O(D)$; Kojevnikov [13], improving the interpolation method
introduced for $\operatorname{\mathsf{Res}}(\operatorname{\mathsf{CP}})$ by
Krajíček [14], gave exponential lower bounds for treelike
$\operatorname{\mathsf{Res}}(\operatorname{\mathsf{CP}})$ when the width of
the clauses (i.e. the number of linear inequalities in a clause) is bounded by
$o(n/\log n)$. Hence these lower bounds are applicable only to very specific
classes of formulas (whose hardness comes from boolean circuit hardness) and
only to $\operatorname{\mathsf{SP}}$ refutations of low depth.

Nevertheless $\operatorname{\mathsf{SP}}$ appears to be a strong proof system.
Firstly notice that the condition terminating a path in a proof is not a
trivial contradiction like in resolution, but is the infeasibility of an
$\operatorname{\mathsf{LP}}$, which is only a polynomial time verifiable
condition. Hence linear size $\operatorname{\mathsf{SP}}$ proofs might be
already a strong class of $\operatorname{\mathsf{SP}}$ proofs, since they can
hide a polynomial growth into one final node whence to run the verification of
the terminating condition.

#### Rank and depth in $\operatorname{\mathsf{CP}}$ and
$\operatorname{\mathsf{SP}}$

It is known that, contrary to the case of other proof systems like Frege,
neither $\operatorname{\mathsf{CP}}$ nor $\operatorname{\mathsf{SP}}$ proofs
can be balanced (see [2]), in the sense that a depth-$d$ proof can always be
transformed into a size $2^{O(d)}$ proof. The depth of
$\operatorname{\mathsf{CP}}$-proofs of a set of linear inequalities ${L}$ is
measured by the Chvátal rank of the associated polytope $P$111This is the
minimal $d$ such that $P^{(d)}$ is empty, where $P^{(0)}$ is the polytope
associated to $L$ and $P^{(i+1)}$ is the polytope defined by all inequalities
which can be inferred from those in $P^{(i)}$ using one Chvátal cut.. It is
known that rank in $\operatorname{\mathsf{CP}}$ and depth in
$\operatorname{\mathsf{SP}}$ are separated, in the sense that Tseitin
principles can be proved in depth $O(\log^{2}n)$ depth in
$\operatorname{\mathsf{SP}}$ [2], but are known to require rank $\Theta(n)$ to
be refuted in $\operatorname{\mathsf{CP}}$ [3]. In this paper we further
develop the study of proof depth for $\operatorname{\mathsf{SP}}$.

Rank lower bound techniques for Cutting Planes are essentially of two types.
The main method is by reducing to the real communication complexity of certain
search problem [11]. As such this method only works for classes of formulas
lifted by certain gadgets capturing specific boolean functions. A second class
of methods have been developed for Cutting Planes, which lower bound the rank
measures of a polytope. In this setting, lower bounds are typically proven
using a geometric method called protection lemmas [3]. These methods were
recently extended in [9] also to the case of Semantic Cutting Planes. In
principle this geometric method can be applied to any formula and not only to
the lifted ones, furthermore for many formulas (such as the Tseitin formulas)
it is known how to achieve $\Omega(n)$ rank lower bounds in
$\operatorname{\mathsf{CP}}$ via protection lemmas, while proving even
$\omega(\log n)$ lower bounds via real communication complexity is impossible,
due to a known folklore upper bound.

Lower bounds for depth in Stabbing Planes, proved in [2], are instead obtained
only as a consequence of the real communication approach extended to Stabbing
Planes. In this paper we introduce two geometric approaches to prove depth
lower bounds in $\operatorname{\mathsf{SP}}$.

Specifically the results we know at present relating
$\operatorname{\mathsf{SP}}$ and $\operatorname{\mathsf{CP}}$ are:

  1. 1.

$\operatorname{\mathsf{SP}}$ polynomially simulates
$\operatorname{\mathsf{CP}}$ (Theorem 4.5 in [2]). Hence in particular the
$\operatorname{\mathsf{PHP}}^{m}_{n}$ can be refuted in
$\operatorname{\mathsf{SP}}$ by a proof of size $O(n^{2})$ ([5]). Furthermore
it can be refuted by a $O(\log n)$ depth proof since polynomial size
$\operatorname{\mathsf{CP}}$ proofs, by Theorem 4.4 in [2], can be balanced in
$\operatorname{\mathsf{SP}}$ 222Another way of proving this result is using
Theorem 4.8 in [2] stating that if there are length $L$ and space $S$
$\operatorname{\mathsf{CP}}$ refutations of a set of linear integral
inequalities, then there are depth $O(S\log L)$ $\operatorname{\mathsf{SP}}$
refutations of the same set of linear integral inequalities; and then use the
result in [10] (Theorem 5.1) that $\operatorname{\mathsf{PHP}}^{m}_{n}$ has
polynomial length and constant space $\operatorname{\mathsf{CP}}$
refutations..

  2. 2.

Beame et al. in [2] proved the surprising result that the class of Tseitin
contradictions $\operatorname{\mathsf{Ts}}(G,\omega)$ over any graph $G$ of
maximum degree $D$, with an odd charging $\omega$, can be refuted in
$\operatorname{\mathsf{SP}}$ in size quasipolynomial in $|G|$ and depth
$O(\log^{2}|G|+D)$.

Depth lower bounds for $\operatorname{\mathsf{SP}}$ are proved in [2]:

  1. 1.

a $\Omega(n/\log^{2}n)$ lower bound for the formula
$\operatorname{\mathsf{Ts}}(G,w)\circ\operatorname{\mathsf{VER}}^{n}$,
composing $\operatorname{\mathsf{Ts}}(G,\omega)$ (over an expander graph $G$)
with the gadget function $\operatorname{\mathsf{VER}}^{n}$ (see Theorem 5.7 in
[2] for details); and

  2. 2.

a $\Omega(\sqrt{n\log n})$ lower bound for the formula
$\operatorname{\mathsf{Peb}}(G)\circ\operatorname{\mathsf{IND}}^{n}_{l}$ over
$n^{5}+n\log n$ variables obtained by lifting a pebbling formula
$\operatorname{\mathsf{Peb}}(G)$ over a graph with high pebbling number, with
a pointer function gadget $\operatorname{\mathsf{IND}}^{n}_{l}$ (see Theorem
5.5. in [2] for details).

Similar to size, these depth lower bounds are applicable only to very specific
classes of formulas. In fact they are obtained by extending to
$\operatorname{\mathsf{SP}}$ the technique introduced in [11, 15] for
$\operatorname{\mathsf{CP}}$ of reducing shallow proofs of a formula
$\mathcal{F}$ to efficient real communication protocols computing a related
search problem and then proving that such efficient protocols cannot exist.

Despite the fact that $\operatorname{\mathsf{SP}}$ is at least as strong as
$\operatorname{\mathsf{CP}}$, in $\operatorname{\mathsf{SP}}$ the known lower
bound techniques are derived from those of treelike
$\operatorname{\mathsf{CP}}$. Hence finding other techniques to prove depth
and size lower bounds for $\operatorname{\mathsf{SP}}$ is important to
understand its proof strength. For instance, unlike
$\operatorname{\mathsf{CP}}$ where we know tight $\Theta(\log n$) rank bounds
for the $\operatorname{\mathsf{PHP}}^{m}_{n}$ [3, 19] and $\Omega(n)$ rank
bounds for Tseitin contradictions [3], for $\operatorname{\mathsf{SP}}$ no
depth lower bound is at present known for purely combinatorial statements.

In this work we address such problems.

###  1.2 Contributions and techniques

The main motivation of this work was to study size and depth lower bounds in
$\operatorname{\mathsf{SP}}$ through new methods, possibly geometric.
Differently from weaker systems like Resolution, except for the technique
highlighted above and based on reducing to the communication complexity of
search problems, we do not know of other methods to prove size and depth lower
bounds in $\operatorname{\mathsf{SP}}$. In $\operatorname{\mathsf{CP}}$ and
Semantic $\operatorname{\mathsf{CP}}$ instead geometrical methods based on
protection lemmas were used to prove rank lower bounds in [3, 9].

Our first steps in this direction were to set up methods working for truly
combinatorial statements, like $\operatorname{\mathsf{Ts}}(G,w)$ or
$\operatorname{\mathsf{PHP}}^{m}_{n}$, which we know to be efficiently
provable in $\operatorname{\mathsf{SP}}$, but on which we cannot use methods
reducing to the complexity of boolean functions, like the ones based on
communication complexity.

We present two new methods for proving depth lower bounds in
$\operatorname{\mathsf{SP}}$ which in fact are the consequence of proving
length lower bounds that do not depend on the bit-size of the coefficients.

As applications of our two methods we respectively prove:

  1. 1.

An exponential separation between the rank in $\operatorname{\mathsf{CP}}$ and
the depth in $\operatorname{\mathsf{SP}}$, using a new counting principle
which we introduce and that we call the Simple Pigeon Principle
$\operatorname{\mathsf{SPHP}}$. We prove that $\operatorname{\mathsf{SPHP}}$
has $O(1)$ rank in $\operatorname{\mathsf{CP}}$ and requires $\Omega(\log n)$
depth in $\operatorname{\mathsf{SP}}$. Together with the results proving that
Tseitin formulas requires $\Omega(n)$ rank lower bounds in
$\operatorname{\mathsf{CP}}$ ([3]) and $O(\log^{2}n)$ upper bounds for the
depth in $\operatorname{\mathsf{SP}}$ ([2]), this proves an incomparability
between the two measures.

  2. 2.

An almost linear lower bounds the size of $\operatorname{\mathsf{SP}}$ proofs
of the $\operatorname{\mathsf{PHP}}^{m}_{n}$ and for Tseitin
$\operatorname{\mathsf{Ts}}(G,\omega)$ contradictions over the complete graph.
These lower bounds immediately give optimal $\Omega(\log n)$ lower bound for
the depth of $\operatorname{\mathsf{SP}}$ proofs of the corresponding
principles.

  3. 3.

A superlinear lower bound for the size of $\operatorname{\mathsf{SP}}$ proofs
of $\operatorname{\mathsf{Ts}}(G,\omega)$, when $G$ is a $n\times n$ grid
graph $H_{n}$. In turn this implies an $\Omega(\log n)$ lower bound for the
depth of $\operatorname{\mathsf{SP}}$ proofs of
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$. Proofs of depth $O(\log^{2}n)$ for
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ are given in [2].

  4. 4.

Finally we prove linear lower bound for the size and $O(\log n)$ lower bounds
of the depth for the the Linear Ordering Principle
$\operatorname{\mathsf{LOP}}$.

Our results are derived from the following initial geometrical observation:
let $\mathbb{S}$ be a space of admissible points in $\\{0,1,1/2\\}^{n}$
satisfying a given unsatisfiable system of integer linear inequalities
$\mathcal{F}(x_{1},\ldots,x_{n})$. In a $\operatorname{\mathsf{SP}}$ proof for
$\mathcal{F}$, at each branch $Q=(\mathbf{a},b)$ the set of points in the
$\operatorname{\mathsf{slab}}(Q)=\\{\mathbf{s}\in\mathbb{S}:b-1<\mathbf{a}\mathbf{x}<b\\}$
does not survive in $\mathbb{S}$. At the end of the proof on the leaves, where
we have infeasible $\operatorname{\mathsf{LP}}$’s, no point in $\mathbb{S}$
can survive the proof. So it is sufficient to find conditions such that, under
the assumption that a proof of $\mathcal{F}$ is “small”, even one point of
$\mathbb{S}$ survives the proof. In pursuing this approach we use two methods.

The antichain method. Here we use a well-known bound based on Sperner’s
Theorem [4, 23] to upper bound the number of points in the slabs where the set
of non-zero coefficients is sufficiently large. Trading between the number of
such slabs and the number of points ruled out from the space $\mathbb{S}$ of
admissible points, we obtain the lower bound.

We initially present the method and the $\Omega(\log n)$ lower bound on a set
of unsatisfiable integer linear inequalities - the Simple Pigeonhole Principle
($\operatorname{\mathsf{SPHP}}$) - capturing the core of the counting argument
used to prove the PHP efficiently in CP. Since
$\operatorname{\mathsf{SPHP}}_{n}$ has rank $1$ $\operatorname{\mathsf{CP}}$
proofs, it entails a strong separation between $\operatorname{\mathsf{CP}}$
rank and $\operatorname{\mathsf{SP}}$ depth. We then apply the method to
$\operatorname{\mathsf{PHP}}^{m}_{n}$ and to
$\operatorname{\mathsf{Ts}}(K_{n},\omega)$.

The covering method. The antichain method appears too weak to prove size and
depth lower bounds on $\operatorname{\mathsf{Ts}}(G,w)$, when $G$ is for
example a grid or a pyramid. To solve this case, we consider another approach
that we call the covering method: we reduce the problem of proving that one
point in $\mathbb{S}$ survives from all the $\operatorname{\mathsf{slab}}(Q)$
in a small proof of $\mathcal{F}$, to the problem that a set of polynomials
which essentially covers the boolean cube $\\{0,1\\}^{n}$ requires at least
$\sqrt{n}$ polynomials, which is a well-known problem faced by Alon and Füredi
in [1] and by Linial and Radhakrishnan in [16]. For this reduction to work we
have to find a high dimensional projection of $\mathbb{S}$ covering the
boolean cube and defined on variables effectively appearing in the proof. We
prove that cycles of distance at least 2 in $G$ work properly to this aim on
$\operatorname{\mathsf{Ts}}(G,\omega)$. Since the grid $H_{n}$ has many such
cycles, we can obtain the lower bound on
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$. The use of Linial and
Radhakrishnan’s result is not new in proof complexity. Part and Tzameret in
[18], independently of us, were using this result in a completely different
way from us in the proof system $\operatorname{\mathsf{Res}}(\oplus)$ handling
clauses over parity equations, and not relying on integer linear inequalities
and geometrical reasoning.

We remark that while we were writing this version of the paper, Yehuda and
Yehudayoff in [24] slightly improved the results of [16] with the consequence,
noticed in their paper too, that our size lower bounds for
$\operatorname{\mathsf{Ts}}(G,\omega)$ over a grid graph is in fact
superlinear.

The paper is organized as follows: We give the preliminary definitions in the
next section and then we move to other sections: one on the lower bounds by
the antichain method and the other on lower bounds by the covering method. The
antichain method is presented on the formulas $\operatorname{\mathsf{SPHP}}$
and the lower bound for $\operatorname{\mathsf{PHP}}^{m}_{n}$ and that for the
Tseitin formulas are moved in the Appendix as well as and that for the Linear
Ordering Principle.

##  2 Preliminaries

We use $[n]$ for the set $\\{1,2,\ldots,n\\}$, $\mathbb{Z}/2$ for
$\mathbb{Z}\cup(\mathbb{Z}+\frac{1}{2})$ and $\mathbb{Z}^{+}$ for
$\\{1,2,\ldots\\}$.

###  2.1 Proof systems

Here we recall the definition of the Stabbing Planes proof system from [2].

######  Definition 2.1.

A _linear integer inequality_ in the variables $x_{1},\ldots,x_{n}$ is an
expression of the form $\sum_{i=1}^{n}a_{i}x_{i}\geq b$, where each $a_{i}$
and $b$ are integral. A set of such inequalities is said to be unsatisfiable
if there are no $0/1$ assignments to the $x$ variables satisfying each
inequality simultaneously.

Note that we reserve the term infeasible, in contrast to unsatisfiable, for
(real or rational) linear programs.

######  Definition 2.2.

Fix some variables $x_{1},\ldots,x_{n}$. A _Stabbing Planes (
$\operatorname{\mathsf{SP}}$)_ proof of a set of integer linear inequalities
$\mathcal{F}$ is a binary tree ${\cal T}$, with each node labeled with a
_query_ $(\mathbf{a},b)$ with $\mathbf{a}\in\mathbb{Z}^{n},b\in\mathbb{Z}$.
Out of each node we have an edge labeled with $\mathbf{a}x\geq b$ and the
other labeled with its integer negation $\mathbf{a}x\leq b-1$. Each leaf
$\ell$ is labeled with a $\operatorname{\mathsf{LP}}$ system $P_{\ell}$ made
by a nonnegative linear combination of inequalities from $\mathcal{F}$ and the
inequalities labelling the edges on the path from the root of ${\cal T}$ to
the leaf $\ell$.

If $\mathcal{F}$ is an unsatisfiable set of integer linear inequalities,
${\cal T}$ is a _Stabbing Planes ( $\operatorname{\mathsf{SP}}$)_ refutation
of $\mathcal{F}$ if all the $\operatorname{\mathsf{LP}}$’s $P_{\ell}$ on the
leaves of ${\cal T}$ are infeasible.

######  Definition 2.3.

The _slab_ corresponding to a query $Q=(\mathbf{a},b)$ is the set
$\operatorname{\mathsf{slab}}(Q)=\\{\mathbf{x}\in\mathbb{R}^{n}:b-1<\mathbf{a}\mathbf{x}<b\\}$
satisfying neither of the associated inequalities.

Since each leaf in a $\operatorname{\mathsf{SP}}$ refutation is labelled by an
infeasible $\operatorname{\mathsf{LP}}$, throughout this paper we will
actually use the following geometric observation on
$\operatorname{\mathsf{SP}}$ proofs ${\cal T}$: the set of points in
$\mathbb{R}^{n}$ must all be ruled out by a query somewhere in ${\cal T}$. In
particular this will be true for those points in $\mathbb{R}^{n}$ which
satisfy a set of integer linear inequalities $\mathcal{F}$ and which we call
feasible points for $\mathcal{F}$.

######  Fact 1.

The slabs associated with a $\operatorname{\mathsf{SP}}$ refutation must cover
the feasible points of $\mathcal{F}$. That is,

$\\{\mathbf{y}\in\mathbb{R}^{n}:\mathbf{a}\mathbf{y}\geq b\text{ for all
}(\mathbf{a},b)\in\mathcal{F}\\}\subseteq\bigcup_{(\mathbf{a},b)\in\mathcal{F}}\\{\mathbf{x}\in\mathbb{R}^{n}:b-1<\mathbf{a}\mathbf{x}<b\\}$

The length of a $\operatorname{\mathsf{SP}}$ refutation is the number of
queries in the proof tree. The depth of a $\operatorname{\mathsf{SP}}$
refutation ${\cal T}$ is the longest root-to-leaf path in ${\cal T}$. The size
(respectively depth) of refuting $\mathcal{F}$ in $\operatorname{\mathsf{SP}}$
is the minimum size (respectively depth) over all $\operatorname{\mathsf{SP}}$
refutations of $\mathcal{F}$. We call bit-size of a
$\operatorname{\mathsf{SP}}$ refutation ${\cal T}$ the total number of bits
needed to represent every inequality in the refutation.

######  Definition 2.4 ([5]).

The _Cutting Planes (CP)_ proof system is equipped with boolean axioms and two
inference rules:

$\begin{array}[]{c|c|c}\mbox{Boolean Axioms}&\mbox{Linear
Combination}&\mbox{Rounding}\\\ \frac{\quad\quad}{x\geq
0}\quad\frac{\quad\quad}{-x\geq-1}&\frac{\mathbf{a}\mathbf{x}\geq
c\quad\quad\mathbf{b}\mathbf{x}\geq
d}{\alpha\mathbf{a}\mathbf{x}+\beta\mathbf{b}\mathbf{x}\geq\alpha c+\beta
d}&\frac{\alpha\mathbf{a}\mathbf{x}\geq b}{\mathbf{a}\mathbf{x}\geq\lceil
b/\alpha\rceil}\end{array}$

where $\alpha,\beta,b\in\mathbb{Z}^{+}$ and
$\mathbf{a},\mathbf{b}\in\mathbb{Z}^{n}$. A CP refutation of some
unsatisfiable set of integer linear inequalities is a derivation of $0\geq 1$
by the aforementioned inference rules from the inequalities in $\cal F$.

A $\operatorname{\mathsf{CP}}$ refutation is treelike if the directed acyclic
graph underlying the proof is a tree. The length of a
$\operatorname{\mathsf{CP}}$ refutation is the number of inequalities in the
sequence. The depth is the length of the longest path from the root to a leaf
(sink) in the graph. The rank of a $\operatorname{\mathsf{CP}}$ proof is the
maximal number of rounding rules used in a path of the proof graph. The size
of a $\operatorname{\mathsf{CP}}$ refutation is the bit-size to represent all
the inequalities in the proof.

###  2.2 Restrictions

Let $V=\\{x_{1},\ldots,x_{n}\\}$ be a set of $n$ variables and let
$\mathbf{a}\mathbf{x}\leq b$ be a linear integer inequality. We say that a
variable $x_{i}$ appears in, or is mentioned by a query $Q=(\mathbf{a},b)$ if
$a_{i}\not=0$ and does not appear otherwise.

A restriction $\rho$ is a function $\rho:D\rightarrow\\{0,1\\}$, $D\subseteq
V$. A restriction acts on a half-plane $\mathbf{a}\mathbf{x}\leq b$ setting
the $x_{i}$’s according to $\rho$. Notice that the variables $x_{i}\in D$ do
not appear in the restricted half-plane.

By ${\cal T}\\!\\!\restriction_{\rho}$ we mean to apply the restriction $\rho$
to all the queries in a $\operatorname{\mathsf{SP}}$ proof ${\cal T}$. The
tree ${\cal T}\\!\\!\restriction_{\rho}$ defines a new
$\operatorname{\mathsf{SP}}$ proof: if some $Q\\!\\!\restriction_{\rho}$
reduces to $0\leq-b$, for some $b\geq 1$, then that node becomes a leaf in
${\cal T}\\!\\!\restriction_{\rho}$. Otherwise in ${\cal
T}\\!\\!\restriction_{\rho}$ we simply branch on $Q\\!\\!\restriction_{\rho}$.
Of course the solution space defined by the linear inequalities labelling a
path in ${\cal T}\\!\\!\restriction_{\rho}$ is a subset of the solution space
defined by the corresponding path in ${\cal T}$. Hence the leaves of ${\cal
T}\\!\\!\restriction_{\rho}$ define an infeasible
$\operatorname{\mathsf{LP}}$.

We work with linear integer inequalities which are a translation of families
of CNFs ${\cal F}$. Hence when we write ${\cal F}\\!\\!\restriction_{\rho}$ we
mean the applications of the restriction $\rho$ to the set of linear integer
inequalities defining ${\cal F}$.

##  3 The antichain method

This method is based on Sperner’s theorem. Using it we can prove depth lower
bounds in $\operatorname{\mathsf{SP}}$ for
$\operatorname{\mathsf{PHP}}^{m}_{n}$ and for Tseitin contradictions
$\operatorname{\mathsf{Ts}}(K_{n},\omega)$ over the complete graph. To
motivate and explain the main definitions, we use as an example a
simplification of the $\operatorname{\mathsf{PHP}}^{m}_{n}$, the Simplified
Pigeonhole principle $\operatorname{\mathsf{SPHP}}_{n}$, which has some
interest since (as we will show) it exponentially separates
$\operatorname{\mathsf{CP}}$ rank from $\operatorname{\mathsf{SP}}$ depth.

###  3.1 Simplified Pigeonhole Principle

As mentioned in the Introduction, the $\operatorname{\mathsf{SPHP}}_{n}$
intends to capture the core of the counting argument used to efficiently
refute the $\operatorname{\mathsf{PHP}}$ in $\operatorname{\mathsf{CP}}$.

######  Definition 3.1.

The $\operatorname{\mathsf{SPHP}}_{n}$ is the following unsatisfiable family
of inequalities:

$\begin{array}[]{l}\sum_{i=1}^{n}x_{i}\geq 2\\\ x_{i}+x_{j}\leq 1\qquad\text{
(for all $i\neq j\in[n]$)}\end{array}$

######  Lemma 3.2.

$\operatorname{\mathsf{SPHP}}_{n}$ has a rank $1$ $\operatorname{\mathsf{CP}}$
refutation, for $n\geq 3$.

######  Proof 3.3.

Let $S:=\sum_{i=1}^{n}x_{i}$ (so we have $S\geq 2$). We fix some $i\in[n]$ and
sum $x_{i}+x_{j}\leq 1$ over all $j\in[n]\setminus\\{i\\}$ to find
$S+(n-2)x_{i}\leq n-1$. We add this to $-S\leq-2$ to get

$x_{i}\leq\frac{n-3}{n-2}$

which becomes $x_{i}\leq 0$ after a single cut. We do this for every $i$ and
find $S\leq 0$ \- a contradiction when combined with the axiom $S\geq 2$.

It is easy to see that $\operatorname{\mathsf{SPHP}}_{n}$ has depth $O(\log
n)$ proofs in $\operatorname{\mathsf{SP}}$, either by a direct proof or
appealing to the polynomial size proofs in $\operatorname{\mathsf{CP}}$ of the
$\operatorname{\mathsf{PHP}}^{m}_{n}$ ([5]) and then using the Theorem 4.4 in
[2] informally stating that “$\operatorname{\mathsf{CP}}$ proofs can be
balanced in $\operatorname{\mathsf{SP}}$”.

######  Corollary 3.4.

The $\operatorname{\mathsf{SPHP}}_{n}$ has $\operatorname{\mathsf{SP}}$
refutations of depth $O(\log n)$.

We will prove that this bound is tight.

###  3.2 Sperner’s Theorem

Let $\mathbf{a}\in\mathbb{R}^{n}$. The width $w(\mathbf{a})$ of $\mathbf{a}$
is the number of non-zero coordinates in $\mathbf{a}$. The width of a query
$(\mathbf{a},b)$ is $w(\mathbf{a})$, and the width of a
$\operatorname{\mathsf{SP}}$ refutation is the minimum width of its queries.

Let $n\in\mathbb{N}$. Fix $W\subseteq[0,1]\cap\mathbb{Q}^{+}$ of finite size
$k\geq 2$ and insist that $0\in W$. The $W$’s we work with in this paper are
$\\{0,1/2\\}$ and $\\{0,1/2,1\\}$.

######  Definition 3.5.

A $(n,W)$-word is an element in $W^{n}$.

We consider the following extension of Sperner’s theorem.

######  Theorem 3.6 ([17, 4]).

Fix any $t\geq 2,t\in\mathbb{N}$. For all $f\in\mathbb{N}$, with the pointwise
ordering of $[t]^{f}$, any antichain has size at most
$t^{f}\sqrt{\frac{6}{\pi(t^{2}-1)f}}(1+o(1)).$

We will use the simplified bound that any antichain ${\cal A}$ has size
$|{\cal A}|\leq\frac{t^{f}}{\sqrt{f}}$.

######  Lemma 3.7.

Let $\mathbf{a}\in\mathbb{Z}^{n}$ and $|W|=k\geq 2$. The number of
$(n,W)$-words $\mathbf{s}$ such that $\mathbf{a}\mathbf{s}=b$, where
$b\in\mathbb{Q}$, is at most $\frac{k^{n}}{\sqrt{w(\mathbf{a})}}$.

######  Proof 3.8.

Define $I_{\mathbf{a}}=\\{i\in[n]:a_{i}\not=0\\}$. Let $\preceq$ be the
partial order over $W^{I_{\mathbf{a}}}$ where $\mathbf{x}\preceq\mathbf{y}$ if
$x_{i}\leq y_{i}$ for all $i$ with $a_{i}>0$ and $x_{i}\geq y_{i}$ for the
remaining $i$ with $a_{i}<0$. Clearly the set of solutions to
$\mathbf{a}\mathbf{s}=b$ forms an antichain under $\preceq$. Noting that
$\preceq$ is isomorphic to the typical pointwise ordering on
$W^{I_{\mathbf{a}}}$, we appeal to Theorem 3.6 to upper bound the number of
solutions in $W^{I_{\mathbf{a}}}$ by
$\frac{k^{w(\mathbf{a})}}{\sqrt{w(\mathbf{a})}}$, each of which corresponds to
at most $k^{n-w(\mathbf{a})}$ vectors in $W^{n}$.

###  3.3 Large admissibility

A $(n,W)$-word $s$ is admissible for an unsatisfiable set of integer linear
inequalities ${\cal F}$ over $n$ variables if $s$ satisfies all constraints of
${\cal F}$. A set of $(n,W)$-words is admissible for ${\cal F}$ if all its
elements are admissible. ${\cal A}({\cal F},W)$ is the set of all admissible
$(n,W)$-words for ${\cal F}$.

The interesting sets $W$ for an unsatisfiable set of integer linear
inequalities ${\cal F}$ are those such that almost all $(n,W)$-words are
admissible for ${\cal F}$. We will apply our method on sets of integer linear
inequalities which are a translation of unsatisfiable CNF’s generated over a
given domain. Typically these formulas on a size $n$ domain have a number of
variables which is not exactly $n$ but a function of $n$, $\nu(n)\geq n$.
Hence for the rest of this section we consider ${\mathscr{F}}:=\\{{\cal
F}_{n}\\}_{n\in\mathbb{N}}$ as a family of sets of unsatisfiable integer
linear inequalities, where ${\cal F}_{n}$ has $\nu(n)\geq n$ variables. We
call ${\mathscr{F}}$ an unsatisfiable family.

Consider then the following definition (recalling that we denote $k=|W|$):

######  Definition 3.9.

${\mathscr{F}}$ is almost full if $|{\cal A}({\cal F}_{n},W)|\geq
k^{\nu(n)}-o(k^{\nu(n)})$.

Notice that, because of the $o$ notation, Definition 3.9 might be not
necessarily true for all $n\in\mathbb{N}$, but only starting from some
$n_{{\mathscr{F}}}$.

######  Definition 3.10.

Given some almost full family ${\mathscr{F}}$ (over $\nu(n)$ variables) we let
$n_{{\mathscr{F}}}$ be the natural number with

$\frac{k^{\nu(n)}}{|{\cal A}({\cal F}_{n},W)|}\leq 2\text{\quad for all
\quad}n\geq n_{{\mathscr{F}}}.$

As an example we prove $\operatorname{\mathsf{SPHP}}$ is almost full (notice
that in the case of $\operatorname{\mathsf{SPHP}}_{n}$, $\nu(n)=n$).

######  Lemma 3.11.

$\operatorname{\mathsf{SPHP}}_{n}$ is almost full.

######  Proof 3.12.

Fix $W=\\{0,1/2\\}$ so that $k=|W|=2$. Let $U$ be the set of all $(n,W)$-words
with at least four coordinates set to $1/2$. $U$ is admissible for
$\operatorname{\mathsf{SPHP}}_{n}$ since inequalities $x_{i}+x_{j}\leq 1$ are
always satisfied for any value in $W$ and inequalities $x_{1}+\ldots+x_{n}\geq
2$ are satisfied by all points in $U$ which contain at least four $1/2$s. By a
simple counting argument, in $U$ there are $2^{n}-4n^{3}=2^{n}-o(2^{n})$
admissible $(n,W)$-words. Hence the claim.

######  Lemma 3.13.

Let ${\mathscr{F}}=\\{{\cal F}_{n}\\}_{n\in\mathbb{N}}$ be an almost full
unsatisfiable family, where ${\cal F}_{n}$ has $\nu(n)$ variables. Further let
${\cal T}$ be a $\operatorname{\mathsf{SP}}$ refutation of ${\cal F}$ of
minimal width $\omega$. If $n\geq n_{{\mathscr{F}}}$ then $|{\cal
T}|=\Omega(\sqrt{w})$.

######  Proof 3.14.

We estimate at what rate the slab of the queries in ${\cal T}$ rule out
admissible points in $U$. Let $\ell$ be the least common multiple of the
denominators in $W$. Every $(n,W)$-word $x$ falling in the slab of some query
$(\mathbf{a},b)$ satisfies one of $\ell$ equations $\mathbf{a}x=b+i/\ell,1\leq
i<\ell$ (as $\mathbf{a}$ is integral). Note that as $|W|$ is a constant
independent of $n$, so is $\ell$.

Since all the queries in ${\cal T}$ have width at least $w$, according to
Lemma 3.7, each query in ${\cal T}$ rules out at most
$\ell\cdot\frac{k^{\nu(n)}}{\sqrt{w}}$ admissible points. By Fact 1 no point
survives at the leaves, in particular the admissible points. Then it must be
that

$|{\cal T}|\ell\cdot\frac{k^{\nu(n)}}{\sqrt{w}}\geq|{\cal A}({\cal
F}_{n},W)|\text{ \quad which means \quad}|{\cal
T}|\ell\cdot\frac{k^{\nu(n)}}{|{\cal A}({\cal F}_{n},W)|}\geq\sqrt{w}$

We finish by noting that, by the assumption $n\geq n_{{\mathscr{F}}}$, and
then by Definition 3.10, we have $2\geq\cdot\frac{k^{\nu(n)}}{|{\cal A}({\cal
F}_{n},W)|}$, so $|{\cal T}|\geq\sqrt{w}/(2\ell)\in\Omega(\sqrt{w})$.

###  3.4 Main theorem

We focus on restrictions $\rho$ that after applied on an unsatisfiable family
${\mathscr{F}}=\\{{\cal F}_{n}\\}_{n\in\mathbb{N}}$, reduce the set ${\cal F}$
to another set in the same family.

######  Definition 3.15.

Let ${\mathscr{F}}=\\{{\cal F}_{n}\\}_{n\in\mathbb{N}}$ be an unsatisfiable
family and $c$ a positive constant. ${\mathscr{F}}$ is $c$-self-reducible if
for any set $V$ of variables, with $|V|=v<n/c$, there is a restriction $\rho$
with domain $V^{\prime}\supseteq V$, such that ${\cal
F}_{n}\\!\\!\restriction_{\rho}={\cal F}_{n-cv}$ (up to renaming of
variables).

Let us motivate the definition with an example.

######  Lemma 3.16.

$\operatorname{\mathsf{SPHP}}_{n}$ is $1$-self-reducible.

######  Proof 3.17.

Whatever set of variables $x_{i}$, $i\in I\subset[n]$ we consider, it is
sufficient to set $x_{i}$ to $0$ to fulfill Definition 3.15.

######  Theorem 3.18.

Let ${\mathscr{F}}:=\\{{\cal F}_{n}\\}_{n\in\mathbb{N}}$ be a unsatisfiable
set of integer linear inequalities which is almost full and $c$-self-
reducible. If ${\cal F}_{n}$ defines a feasible $\operatorname{\mathsf{LP}}$
whenever $n>n_{{\mathscr{F}}}$, then for $n$ large enough, the shortest
$\operatorname{\mathsf{SP}}$ proof of ${\cal F}_{n}$ is of length
$\Omega(\sqrt[4]{n})$.

######  Proof 3.19.

Take any $\operatorname{\mathsf{SP}}$ proof $\mathcal{T}$ refuting ${\cal
F}_{n}$ and fix $t=\sqrt[4]{n}$.

The proof proceeds by stages $i\geq 0$ where ${\cal T}_{0}={\cal T}$. The
stages will go on while the invariant property (which at stage $0$ is true
since $n>n_{{\mathscr{F}}}$ and $c$ a positive constant)

$n-ict^{3}>\max\\{n_{{\mathscr{F}}},n(1-1/c)\\}$

holds.

At the stage $i$ we let $\Sigma_{i}=\\{(\mathbf{a},b)\in{\cal
T}_{i}:w(\mathbf{a})\leq t^{2}\\}$ and $s_{i}=|\Sigma_{i}|$. If $s_{i}\geq t$
the claim is trivially proven. If $s_{i}=0$, then all queries in ${\cal
T}_{i}$ have width at least $t^{2}$ and by Lemma 3.13 (which can be applied
since $n-ict^{3}>n_{{\mathscr{F}}}$) the claim is proven (for $n$ large
enough).

So assume that $0<s_{i}<t$. Each of the queries in $\Sigma_{i}$ involves at
most $t^{2}$ nonzero coefficients, hence in total they mention at most
$s_{i}t^{2}\leq t^{3}$ variables. Extend this set of variables to some
$V^{\prime}$ in accordance with Definition 3.15 (which can be done since, by
the invariant, $ict^{3}<n/c$). Set all these variables according to self-
reducibility of ${\cal F}$ in a restriction $\rho_{i}$ and define ${\cal
T}_{i+1}={\cal T}_{i}\\!\\!\restriction\\!\\!_{\rho_{i}}$. Note that by
Definition 3.15 and by that of restriction, ${\cal T}_{i+1}$ is a
$\operatorname{\mathsf{SP}}$ refutation of ${\cal F}_{n-ict^{3}}$ and we can
go on with the next stage. (Also note that we do not hit an empty refutation
this way, due to the assumption that ${\cal F}_{n}$ defines a feasible LP.)

Assume that the invariant does not hold. If this is because
$n-ict^{3}<n_{{\mathscr{F}}}$ then, as each iteration destroys at least one
node,

$|{\cal T}|\geq i>\frac{n-n_{{\mathscr{F}}}}{ct^{3}}\in\Omega(n^{1/4}).$

If this is because $n-ict^{3}<n-n/c$, then again for the same reason it holds
that

$|{\cal T}|\geq i>\frac{n}{c^{2}n^{3/4}}\in\Omega(n^{1/4}).$

Using Lemmas 3.11 and 3.16 and the previous Theorem we get:

######  Corollary 3.20.

The length of any $\operatorname{\mathsf{SP}}$ refutation of
$\operatorname{\mathsf{SPHP}}_{n}$ is $\Omega(\sqrt[4]{n})$. Hence the minimal
depth is $\Omega(\log n)$.

###  3.5 Lower bounds for the Pigeonhole principle

######  Definition 3.21.

The _Pigeonhole Principle_ $\operatorname{\mathsf{PHP}}^{m}_{n}$, $m(n)>n$, is
the family of unsatisfiable integer linear inequalities defined over the
variables $\\{P_{i,j}:i\in[m],j\in[n]\\}$ consisting of the following
inequalities:

$\begin{array}[]{ll}\sum_{j=1}^{n}P_{i,j}\geq 1\quad\forall
i\in[m]&\text{(every pigeon goes into some hole)}\\\ P_{i,k}+P_{j,k}\leq
1\quad\forall k\in[n],i\neq j\in[m]&\text{(at most one pigeon enters any given
hole)}\end{array}$

We present a lower bound for $\operatorname{\mathsf{PHP}}^{m}_{n}$ closely
following that for $\operatorname{\mathsf{SPHP}}_{n}$, in which we largely
ignore the diversity of different pigeons (which makes the principle rather
like $\operatorname{\mathsf{SPHP}}_{n}$).

In this subsection we fix $W=\\{0,1/2\\}$, and for the sake of brevity refer
to $(n,W)$-words as _biwords_.

In this section we fix $m$ to be $n+d$, for any fixed $d\in\mathbb{N}$ at
least one.

######  Lemma 3.22.

The $\operatorname{\mathsf{PHP}}^{n+d}_{n}$ is almost full.

######  Proof 3.23.

We show that there are at least $2^{mn-1}$ admissible biwords (for
sufficiently large $n$). For each pigeon $i$, there are admissible valuations
to holes so that, so long as at least two of these are set to $1/2$, the
others may be set to anything in $\\{0,1/2\\}$. This gives at least
$2^{n}-(n+1)$ possibilities. Since the pigeons are independent, we obtain at
least $(2^{n}-(n+1))^{m}$ biwords. Now this is
$2^{mn}\left(1-\frac{n+1}{2^{n}}\right)^{m}$ where
$\left(1-\frac{n+1}{2^{n}}\right)^{m}\sim e^{\frac{-(n+1)m}{2^{n}}}$ whence,
$\left(1-\frac{n+1}{2^{n}}\right)^{m}\geq e^{\frac{-(n+2)m}{2^{n}}}$ for
sufficiently large $n$. It follows there is a constant $c$ so that:

$2^{mn}\left(1-\frac{n+1}{2^{n}}\right)^{m}\geq
2^{mn-\frac{c(n+2)m}{2^{n}}}\geq 2^{mn-1}$

for sufficiently large $n$.

######  Lemma 3.24.

The $\operatorname{\mathsf{PHP}}^{n+d}_{n}$ is $1$-self-reducible.

######  Proof 3.25.

We are given some set $I$ of variables from
$\operatorname{\mathsf{PHP}}^{n+c}_{n}$. These variables will mention some set
of holes $H:=\\{j:P_{i,j}\in I\text{ for some i}\\}$ and similarly a set of
pigeons $P$. Each of $P$, $H$ have size at most $|I|$ and we extend them both
arbitrarily to have size exactly $|I|$. Our restriction matches $P$ and $H$ in
any way and then sets any other variable mentioning a pigeon in $P$ or a hole
in $H$ to $0$.

######  Theorem 3.26.

The length of any $\operatorname{\mathsf{SP}}$ refutation of
$\operatorname{\mathsf{PHP}}^{n+d}_{n}$ is $\Omega(n^{1/4})$.

######  Proof 3.27.

Note that the all $1/2$ point is feasible for
$\operatorname{\mathsf{PHP}}^{n+d}_{n}$. Then with Lemma 3.22 and Lemma 3.24
in hand we meet all the prerequisites for Theorem 3.18.

By simply noting that a $\operatorname{\mathsf{SP}}$ refutation is a binary
tree, we get the following corollary.

######  Corollary 3.28.

The $\operatorname{\mathsf{SP}}$ depth of the
$\operatorname{\mathsf{PHP}}^{n+d}_{n}$ is $\Omega(\log n)$.

###  3.6 Lower bounds for Tseitin contradictions over the complete graph

######  Definition 3.29.

For a graph $G=(V,E)$ along with a charging function $\omega:V\to\\{0,1\\}$
satisfying $\sum_{v\in V}\omega(v)=1\mod 2$. The _Tseitin contradiction_
$\operatorname{\mathsf{Ts}}(G,\omega)$ is the set of linear inequalities which
translate the CNF encoding of

$\sum_{\begin{subarray}{c}e\in E\\\ e\ni v\end{subarray}}x_{e}=\omega(v)\mod
2.$

for every $v\in V$, where the variables $x_{e}$ range over the edges $e\in E$.

In this subsection we consider $\operatorname{\mathsf{Ts}}(K_{n},\omega)$ and
$\omega$ will always be an odd charging for $K_{n}$. We let $N:=\binom{n}{2}$
and we fix $W=\\{0,1/2,1\\}$, $k=3$ and for the sake of brevity refer to
$(n,W)$-words as _triwords_. We will abuse slightly the notation of Section
3.3 and consider the family
$\\{\operatorname{\mathsf{Ts}}(K_{n},\omega)\\}_{n\in\mathbb{N},\;\omega\text{
odd}}$ as a single parameter family in $n$. The reason we can do this is
because the following proofs of almost fullness and self reducibility do not
depend on $\omega$ at all (so long as it is odd, which we will always ensure).

######  Lemma 3.30.

$\operatorname{\mathsf{Ts}}(K_{n},\omega)$ is almost full.

######  Proof 3.31.

We show that $\operatorname{\mathsf{Ts}}(K_{n},\omega)$ has at least $c3^{N}$
admissible triwords, for any constant $0<c<1$ and $n$ large enough. We define
the assignment $\rho$ setting all edges (i.e. $x_{e}$) to a value in
$W=\\{0,1,1/2\\}$ independently and uniformly at random, and inspecting the
probability that some fixed constraint for a node $v$ is violated by $\rho$.

Clearly if at least $2$ edges incident to $v$ are set to $1/2$ its constraint
is satisfied. If none of its incident edges are set to $1/2$ then it is
satisfied with probability $1/2$. Let $A(v)$ be the event “no edge incident to
$v$ is set to $1/2$ by $\rho$” and let $B(v)$ be the event that “exactly one
edge incident to $v$ is set to $1/2$ by $\rho$”. Then:

$\displaystyle\Pr[\text{$v$ is
violated}]\leq\frac{1}{2}\Pr[A(v)]+\Pr[B(v)]=\frac{1}{2}\frac{2^{n-1}}{3^{n-1}}+\frac{(n-1)2^{n-2}}{3^{n-1}}=n\frac{2^{n-2}}{3^{n-1}}.$

Therefore, by a union bound, the probability that there exists a node with
violated parity is bounded above by $n^{2}\frac{2^{n-2}}{3^{n-1}}$, which
approaches $0$ as $n$ goes to infinity.

######  Lemma 3.32.

$\operatorname{\mathsf{Ts}}(K_{n},\omega)$ is $2$-self-reducible.

######  Proof 3.33.

We are given some set of variables $I$. Each variable mentions $2$ nodes, so
extend these mentioned nodes arbitrarily to a set $S$ of size exactly $2|I|$,
which we then hit with the following restriction: if $S$ is evenly charged,
pick any matching on the set $\\{s\in S:w(s)=1\\}$, set those edges to $1$,
and set any other edges involving some vertex in $S$ to $0$. Otherwise (if $S$
is oddly charged) pick any $l\in\\{s\in S:w(s)=1\\}$ and $r\in[n]\setminus S$
and set $x_{lr}$ to $1$. $\\{s\in S:w(s)=1\\}\setminus l$ is now even so we
can pick a matching as before. And as before we set all other edges involving
some vertex in $S$ to 0. In the first case the graph induced by $[n]\setminus
S$ must be oddly charged (as the original graph was). In the second case this
induced graph was originally evenly charged, but we changed this when we set
$x_{lr}$ to $1$.

######  Lemma 3.34.

For any oddly charged $\omega$ and $n$ large enough, all
$\operatorname{\mathsf{SP}}$ refutations of
$\operatorname{\mathsf{Ts}}(K_{n},\omega)$ have length $\Omega(\sqrt[4]{n})$.

######  Proof 3.35.

We have that the all $1/2$ point is feasible for
$\operatorname{\mathsf{Ts}}(K_{n},\omega)$. Then we can simply apply Theorem
3.18.

######  Corollary 3.36.

The depth of any SP refutation of $\operatorname{\mathsf{Ts}}(K_{n},\omega)$
is $\Omega(\log{n})$.

###  3.7 Lower bound for the Least Ordering Principle

######  Definition 3.37.

Let $n\in\mathbb{N}$. The _Least Ordering Principle_ ,
$\operatorname{\mathsf{LOP}}_{n}$, is the following set of unsatisfiable
linear inequalities over the variables $P_{i,j}$ ($i\neq j\in[n]$):

$\displaystyle P_{i,j}+P_{j,i}=1\quad\text{ for all $i\neq j\in[n]$}$
$\displaystyle P_{i,k}-P_{i,j}-P_{j,k}\geq 1\text{ for all $i\neq j\neq
k\in[n]$}$ $\displaystyle\sum_{i=1,i\neq j}^{n}P_{i,j}\geq 1\text{ for all
$j\in[n]$}$

######  Lemma 3.38.

For any $X\subseteq[n]$ of size at most $n-3$, there is an admissible point
for $\operatorname{\mathsf{LOP}}_{n}$ integer on any edge mentioning an
element in $X$.

######  Proof 3.39.

Let $\preceq$ be any total order on the elements in $X$. Our admissible point
$x$ will be

$x(P_{i,j})=\begin{cases}1&\text{ if $i,j\in X$ and $i\preceq j$, or if
$i\not\in X,j\in X$}\\\ 0&\text{ if $i,j\in X$ and $j\preceq i$, or if $i\in
X,j\not\in X$}\\\ 1/2&\text{otherwise (if $i,j\not\in X$)}.\end{cases}$

The existential axioms $\sum_{i=1,i\neq j}^{n}P_{i,j}$ are always satisfied -
if $j\in X$ then there is some $i\not\in X$ with $P_{i,j}=1$, and otherwise
there are at least two distinct $i,k\neq j\in X$ with $P_{i,j},P_{k,j}=1/2$.
For the transitivity axioms $P_{i,k}-P_{i,j}-P_{j,k}\geq 1$, note that if $2$
or more of $i,j,k$ are not in $X$ there are at least $2$ variables set to
$1/2$, and otherwise it is set in a binary fashion to something consistent
with a total order.

We will assume that a $\operatorname{\mathsf{SP}}$ refutation ${\cal T}$ of
$\operatorname{\mathsf{LOP}}_{n}$ only involves variables $P_{i,j}$ where
$i<j$ \- this is without loss of generality as we can safely set $P_{j,i}$ to
$1-P_{i,j}$ whenever $i>j$, and will often write $P_{\\{i,j\\}}$ for such a
variable. We consider the underlying graph of the support of a query, i.e. an
undirected graph with edges $\\{i,j\\}$ for every variable $P_{\\{i,j\\}}$
that appears with non-zero coefficient in the query.

For some function $f(n)$, we say the query is _$f(n)$ -wide_ if the smallest
edge cover of its graph has at least $f(n)$ nodes . A query that is not
$f(n)$-wide is _$f(n)$ -narrow_. The next lemma works much the same as Theorem
3.18.

######  Lemma 3.40.

Fix $\epsilon>0$ and suppose we have some $\operatorname{\mathsf{SP}}$
refutation ${\cal T}$ of $\operatorname{\mathsf{LOP}}_{n}$, where $|{\cal
T}|\leq n^{\frac{1-\epsilon}{4}}$. Then, if $n$ is large enough, we can find
some $\operatorname{\mathsf{SP}}$ refutation ${\cal T}^{\prime}$ of
$\operatorname{\mathsf{LOP}}_{c\cdot n}$, where $c$ is a positive universal
constant that may be taken arbitrarily close to $1$, ${\cal T}^{\prime}$
contains only $n^{3/4}$-wide queries, and $|T^{\prime}|\leq|{\cal T}|$.

######  Proof 3.41.

We iteratively build up an initially empty restriction $\rho$. At every stage
$\rho$ imposes a total order on some subset $X\subseteq[n]$ and places the
elements in $X$ above the elements not in $X$. So $\rho$ sets every edge not
contained entirely in $[n]\setminus X$ to something binary, and
$\operatorname{\mathsf{LOP}}_{n}\\!\\!\restriction_{\rho}=\operatorname{\mathsf{LOP}}_{n-|X|}$
(up to a renaming of variables).

While there exists a $n^{3/4}$-narrow query $q\in{\cal
T}\\!\\!\restriction_{\rho}$ we simply take its smallest edge cover, which has
size at most $n^{3/4}$ by definition, and add its nodes in any fashion to the
total order in $\rho$. Now all of the variables mentioned by $q\in{\cal
T}\\!\\!\restriction_{\rho}$ are fully evaluated and $q$ is redundant. We
repeat this at most $n^{\frac{1-\epsilon}{4}}$ times (as $|{\cal T}|\leq
n^{\frac{1-\epsilon}{4}}$ and each iteration renders at least one query in
${\cal T}$ redundant). At each stage we grow the domain of the restriction by
at most $n^{3/4}$, so the domain of $\rho$ is always bounded by
$n^{1-\epsilon/4}$. We also cannot exhaust the tree ${\cal T}$ in this way, as
otherwise ${\cal T}$ mentioned at most $n^{1-\epsilon/4}<n-3$ elements and by
Lemma 3.38 there is an admissible point not falling in any slab of ${\cal T}$,
violating 1.

When this process finishes we are left with a $n^{3/4}$-wide refutation ${\cal
T}^{\prime}$ of $\operatorname{\mathsf{LOP}}_{n-n^{1-\epsilon/4}}$. As
$\epsilon$ was fixed we find that as $n$ goes to infinity $n-n^{1-\epsilon/4}$
tends to $n$.

######  Lemma 3.42.

Let $d\leq(n-3)/2$. Given any disjoint set of pairs
$D=\\{\\{l_{1},r_{1}\\},\ldots,\\{l_{d},r_{d}\\}\\}$ (where WLOG $l_{i}<r_{i}$
in $[n]$ as natural numbers) and any binary assignment $b\in\\{0,1\\}^{D}$,
the assignment $x_{b}$ with

$x_{b}(P_{\\{i,j\\}})=\begin{cases}b(\\{l_{k},r_{k}\\})&\text{ if
$\\{i,j\\}=\\{l_{k},r_{k}\\}\in X$ for some $k$}\\\
1/2&\text{otherwise}\end{cases}$

is admissible.

######  Proof 3.43.

The existential axioms $\sum_{i=1,i\neq j}^{n}P_{i,j}$ are always satisfied,
as for any $j$ there are at least $n-2$ $i\in[n]$ different from $j$ with
$P_{i,j}=1/2$. For the transitivity axioms $P_{i,k}-P_{i,j}-P_{j,k}\geq 1$,
note that due to the disjointness of $D$ at least two variables on the left
hand side are set to $1/2$.

######  Theorem 3.44.

Fix some $\epsilon>0$ and let ${\cal T}$ any $\operatorname{\mathsf{SP}}$
refutation of $\operatorname{\mathsf{LOP}}_{n}$. Then, for $n$ large enough,
$|{\cal T}|\in\Omega(n^{\frac{1-\epsilon}{4}})$.

######  Proof 3.45.

Suppose otherwise - then, by Lemma 3.40, we can find some ${\cal T}^{\prime}$
refuting $\operatorname{\mathsf{LOP}}_{cn}$, with $|{\cal
T}^{\prime}|\leq|{\cal T}|$, every query $n^{3/4}$-wide, and $c$ independent
of $n$. We greedily create a set of pairs $D$ by processing the queries in
${\cal T}^{\prime}$ one by one and choosing in each a matching of size
$n^{1/2}$ disjoint from the elements appearing in $D$ \- this always succeeds,
as at every stage $|D|\in O(n^{\frac{1-\epsilon}{4}}\cdot n^{1/2})$ and
involves at most $O(2n^{\frac{3-\epsilon}{4}})<n^{3/4}-n^{1/2}$ elements.

So by Lemma 3.42, after setting every edge not in $D$ to $1/2$, we have some
set of linear polynomials ${\cal
R}=\\{a(x)=\mathbf{a}x-b-1/2:(\overline{a},b)\in{\cal T}^{\prime}\\}$ covering
the hypercube $\\{0,1\\}^{D}$, where every polynomial $p\in{\cal R}$ mentions
at least $n^{1/2}$ edges. By Lemma 3.7 each such polynomial in ${\cal R}$
rules out at most $\nicefrac{{2^{|D|}}}{{n^{1/4}}}$ points, and so we must
have $|{\cal T}|\geq|T^{\prime}|\geq|{\cal R}|\geq n^{1/4}$.

##  4 The covering method

######  Definition 4.1.

A set $L$ of linear polynomials with real coefficients is said to be a _cover_
of the cube $\\{0,1\\}^{n}$ if for each $v\in\\{0,1\\}^{n}$, there is a $p\in
L$ such that $p(v)=0$.

In [16] Linial and Radhakrishnan considered the problem of the minimal number
of hyperplanes needed to cover the cube $\\{0,1\\}^{n}$. Clearly every such
cube can be covered by the zero polynomial, so to make the problem more
meaningful they defined the notion of an essential covering of
$\\{0,1\\}^{n}$.

######  Definition 4.2 ([16]).

A set $L$ of linear polynomials with real coefficients is said to be an
_essential cover_ of the cube $\\{0,1\\}^{n}$ if

  1. (E1)

$L$ is a cover of $\\{0,1\\}^{n}$,

  2. (E2)

no proper subset of $L$ satisfies (E1), that is, for every $p\in L$, there is
a $v\in\\{0,1\\}^{n}$ such that $p$ alone takes the value $0$ on $v$, and

  3. (E3)

every variable appears (in some monomial with non-zero coefficient) in some
polynomial of $L$.

They then proved that any essential cover $E$ of the hypercube $\\{0,1\\}^{n}$
must satisfy $|E|\geq\sqrt{n}$. We will use the slightly strengthened lower
bound given in [25]:

######  Theorem 4.3.

Any essential cover $L$ of the cube with $n$ coordinates satisfies
$|L|\in\Omega(n^{0.52})$.

We will need an auxillary definition and lemma.

######  Definition 4.4.

Let $L$ be a cover of $\\{0,1\\}^{I}$ for some index set $I$. Some subset
$L^{\prime}$ of $L$ is an _essentialisation_ of $L$ if $L^{\prime}$ also
covers $\\{0,1\\}^{I}$ but no proper subset of it does.

######  Lemma 4.5.

Let $L$ be a cover of the cube $\\{0,1\\}^{n}$ and $L^{\prime}$ be any
essentialisation of $L$. Let $M^{\prime}$ be the set of variables appearing
with nonzero coefficient in $L^{\prime}$. Then $L^{\prime}$ is an essential
cover of $\\{0,1\\}^{M^{\prime}}$.

######  Proof 4.6.

  * (E1)

Given any point $x\in\\{0,1\\}^{M^{\prime}}$, we can extend it arbitrarily to
a point $x^{\prime}\in\\{0,1\\}^{M}$. Then there is some $p\in L^{\prime}$
with $p(x^{\prime})=0$ \- but $p(x^{\prime})=p(x)$, as $p$ doesn’t mention any
variable outside of $M^{\prime}$.

  * (E2)

Similarly to the previous point, this will follow from the fact that if some
set ${\cal T}$ covers a hypercube $\\{0,1\\}^{I}$, it also covers
$\\{0,1\\}^{I^{\prime}}$ for any $I^{\prime}\supseteq I$.

Suppose some proper subset $L^{\prime\prime}\subset L^{\prime}$ covers
$\\{0,1\\}^{M^{\prime}}$, then it covers $\\{0,1\\}^{M}$ \- but we picked
$L^{\prime}$ to be a minimal set with this property.

  * (E3)

We defined $M^{\prime}$ to be the set of variables appearing with nonzero
coefficient in $L^{\prime}$.

###  4.1 The covering method and Tseitin

Let $H_{n}$ denote the $n\times n$ grid graph. Fix some $\omega$ with odd
charge and a $\operatorname{\mathsf{SP}}$ refutation ${\cal T}$ of
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$. 1 tells us that for every point
$x$ admissible for $\operatorname{\mathsf{Ts}}(H_{n},\omega)$, there exists a
query $(\mathbf{a},b)\in{\cal T}$ such that $b<\mathbf{a}x<b+1$. In this
section we will only consider admissible points with entries in
$\\{0,1/2,1\\}$, turning the slab of a query $(\mathbf{a},b)$ into the
solution set of the single linear equation $\mathbf{a}\cdot x=b+1/2$. So we
consider ${\cal T}$ as a set of such equations.

We say that an edge of $H_{n}$ is mentioned in ${\cal T}$ if the variable
$x_{e}$ appears with non-zero coefficient in some query in ${\cal T}$. We can
see $H_{n}$ as a set of $(n-1)^{2}$ squares (4-cycles), and we can index them
as if they were a Cartesian grid, starting from $1$. Let $S$ be the set of
$\lfloor(n/3)^{2}\rfloor$ squares in $H_{n}$ gotten by picking squares with
indices that become $2\text{ (mod }3)$. This ensures that every two squares in
$S$ in the same row or column have at least two other squares between them,
and that no selected square is on the perimeter.

We will assume WLOG that $n$ is a multiple of 3, so $|S|=(n/3)^{2}$. Let
$K=\bigcup_{t\in S}t$ be the set of edges mentioned by $S$, and for some $s\in
S$, let $K_{s}:=\bigcup_{t\in S,t\neq s}t$ be the set of edges mentioned in
$S$ by squares other than $s$.

######  Lemma 4.7.

For every $s\in S$ we can find an admissible point
$b_{s}\in\\{0,1/2,1\\}^{E(H_{n})}$ such that

  1. 1.

$b_{s}(x_{e})=0$ for all $e\in K_{s}$, and

  2. 2.

$b_{s}$ is fractional only on the edges in $s$.

######  Proof 4.8.

We use the following fact due to A. Urquhart in [22]

######  Fact 2.

For each vertex $v$ in $H_{n}$ there is a totally binary assignment, called
$v$-critical in [22], satisfying all parity axioms in
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ except the parity axiom of node
$v$.

Pick any corner $c$ of $s$. Let $b_{s}$ be the result of taking any
$c$-critical assignment of the variables of
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ and setting the edges in $s$ to
$1/2$. $b_{s}$ is admissible, as $c$ is now adjacent to two variables set to
$1/2$ (so its originally falsified parity axiom becomes satisfied) and every
other vertex is either unaffected or also adjacent to two $1/2$s. While
$b_{s}$ sets some edge $e\in K_{s}$ to 1, flip all of the edges in the unique
other square containing $e$. This other square always exists (as no square
touches the perimeter) and also contains no other edge in $K_{s}$ (as there
are at least two squares between any two squares in $S$). Flipping the edges
in a cycle preserves admissibility, as every vertex is adjacent to $0$ or $2$
flipped edges.

######  Definition 4.9.

Let $V_{S}:=\\{v_{s}:s\in S\\}$ be a set of new variables. For $s\in S$ define
the substitution $h_{s}$, taking the variables of
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ to $V_{S}\cup\\{0,1/2,1\\}$, as

$h_{s}(x_{e}):=\begin{cases}b_{s}(e)&\text{ if $e$ is not mentioned in $S$, or
if $e$ is mentioned by $s$,}\\\ v_{t}&\text{if $e$ is mentioned by some square
$t\neq s\in S$.}\\\ \end{cases}$

(where $b_{s}$ is from Lemma 4.7).

######  Definition 4.10.

Say that a linear polynomial $p=c+\sum_{e\in E(H_{n})}\mu_{e}x_{e}$ with
coefficients $\mu_{e}\in\mathbb{Z}$ and some constant part $c\in\mathbb{R}$
has _odd coefficient in $X\subseteq E(H_{n})$_ if $\sum_{e\in X}\mu_{e}$ is an
odd integer. Given some polynomial $p$ in the variables $x_{e}$ of Tseitin,
and some square $s\in S$, let $p_{s}$ be the polynomial in variables $V_{S}$
gotten by applying the substitution $x_{e}\to h_{s}(x_{e})$. Also, for any set
of polynomials ${\cal T}$ in the variables $x_{e}$ let ${\cal
T}_{s}:=\\{p_{s}:p\in{\cal T},p\text{ has odd coefficient in }s\\}.$

Given some assignment $\alpha\in\\{0,1\\}^{V_{S}\setminus\\{v_{s}\\}}$, and
some $h_{s}$ as in Definition 4.9, we let $\alpha(h_{s})$ be the assignment to
the variables of $\operatorname{\mathsf{Ts}}(H_{n},\omega)$ gotten by
replacing the $v_{t}$ in the definintion of $h_{s}$ by $\alpha(v_{t})$.

######  Lemma 4.11.

Let $s\in S$. For all $2^{|S|-1}$ settings $\alpha$ of the variables in
$V_{S}\setminus\\{s\\}$, $\alpha(h_{s})$ is admissible.

######  Proof 4.12.

When $\alpha(v_{t})$ is all $0$, $h_{s}=b_{s}$ is admissible (by Lemma 4.7).
Toggling some $v_{t}$ only has the effect of flipping every edge in a cycle,
which preserves admissibility.

######  Lemma 4.13.

${\cal T}_{s}$ covers $\\{0,1\\}^{V_{S}\setminus\\{s\\}}$.

######  Proof 4.14.

For every setting of $\alpha\in\\{0,1\\}^{V_{S}\setminus\\{s\\}}$,
$\alpha(h_{s})$ as defined above is admissible and therefore covered by some
$p\in{\cal T}$, which has constant part $1/2+b$ for some $b\in\mathbb{Z}$.
Furthermore, as $\alpha(h_{s})$ sets every edge in $s$ to $1/2$, every such
$p$ must have odd coefficient in front of $s$ \- otherwise

$p(\alpha(h_{s}))=1/2+b+(1/2)\left(\sum_{e\in s}\mu_{e}\right)+\sum_{e\not\in
s}\mu_{e}\alpha(h_{s})(x_{e})$

can never be zero, as the $1/2$ is the only non integral term in the
summation.

######  Theorem 4.15.

Any $\operatorname{\mathsf{SP}}$ refutation ${\cal T}$ of
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ must have $|{\cal
T}|\in\Omega(n^{1.04})$.

######  Proof 4.16.

We are going to find a set of pairs
$(L_{1},M_{1}),(L_{2},M_{2}),\ldots,(L_{q},M_{q})$, where the $L_{i}$ are
pairwise disjoint nonempty subsets of ${\cal T}$, the $M_{i}$ are subsets of
$V_{S}$, and for every $i$ there is some $s_{i}\in
S\setminus\bigcup_{i=1}^{q}M_{i}$ such that
$|(L_{i})_{s_{i}}|\geq|M_{i}|^{0.52}$. These pairs will also satisfy the
property that

$\\{s_{i}:1\leq i\leq q\\}\cup\bigcup_{i=1}^{q}M_{i}=S.$ (1)

As $|S|=(n/3)^{2}$ this would imply that
$\sum_{i=1}^{q}|M_{i}|\geq(n/3)^{2}-q$. If $q\geq(n/3)^{2}/2$, then (as the
$L_{i}$ are nonempty and pairwise disjoint) we have $|{\cal
T}|\geq(n/3)^{2}/2\in\Omega(n^{1.04})$. Otherwise
$\sum_{i=1}^{q}|M_{i}|\geq(n/3)^{2}/2$, and as (by Theorem 4.3) each
$|L_{i}|\geq|M_{i}|^{0.52}$,

$|{\cal
T}|\geq\sum_{i=1}^{q}|L_{i}|\geq\sum_{i=1}^{q}|M_{i}|^{0.52}\geq\left(\sum_{i=1}^{q}|M_{i}|\right)^{0.52}\geq\left((n/3)^{2}/2\right)^{0.52}\in\Omega(n^{1.04}).$
(2)

We create the pairs by stages. Let $S_{1}=S$ and start by picking any
$s_{1}\in S_{1}$. By Lemma 4.13 ${\cal T}_{s_{1}}$ covers
$\\{0,1\\}^{V_{S_{1}}\setminus\\{s_{1}\\}}$ and has as an essentialisation
$E$, which will be an essential cover of $\\{0,1\\}^{V^{\prime}}$ for some
$V^{\prime}\subseteq V_{S_{1}}\setminus\\{s_{1}\\}$. We create the pair
$(L_{1},M_{1})=(\\{p:p_{s_{1}}\in E\\},V^{\prime})$ and update
$S_{2}=S_{1}\setminus\left(V^{\prime}\cup\\{s_{1}\\}\right)$. (Note that
$V^{\prime}$ could possibly be empty - for example, if the polynomial
$x_{e}=1/2$ appears in ${\cal T}$, where $e\in s_{1}$. In this case however we
still have $|L_{1}|\geq|M_{1}|^{0.52}$. If $V^{\prime}$ is not empty we have
the same bound due to Theorem 4.3.) If $S_{2}$ is nonempty we repeat with any
$s_{2}\in S_{2}$, and so on.

We now show that as promised the left hand sides of these pairs partition a
subset of ${\cal T}$, which will give us the first inequality in Equation 2.
Every polynomial $p$ with $p_{s_{i}}\in L_{i}$ has every $v_{t}$ mentioned by
$p_{s_{i}}$ removed from $S_{j}$ for all $j\geq i$, so the only way $p$ could
reappear in some later $L_{j}$ is if $p_{s_{j}}\in{\cal T}_{s_{j}}$, where
$v_{s_{j}}$ does _not_ appear in $p_{s_{i}}$. Let $\mu_{e},e\in s_{j}$ be the
coefficients of $p$ in front of the four edges of $s_{j}$. The coefficient in
front of $v_{s_{j}}$ in $p_{s_{i}}$ is just $\sum_{e\in s_{j}}\mu_{e}$. As
$v_{s_{j}}$ failed to appear this sum is $0$ and $p$ does not have the odd
coefficient sum it would need to appear in ${\cal T}_{s_{j}}$.

##  5 Conclusions and acknowledgements

The $\Omega(\log n)$ depth lower bound for
$\operatorname{\mathsf{Ts}}(H_{n},\omega)$ is not optimal since [2] proved an
$O(\log^{2}n)$ upper bound for $\operatorname{\mathsf{Ts}}(G,\omega)$, for any
bounded-degree $G$. Even to apply the covering method to prove a depth
$\Omega(\log^{2}n)$ lower bound on $\operatorname{\mathsf{Ts}}(K_{n},\omega)$
(notice that it would imply a superpolynomial length lower bound), the
polynomial covering of the boolean cube should be improved to work on general
cubes. To this end the algebraic method used in [16] should be improved to
work with generalizations of multilinear polynomials.

While finishing the writing of this manuscript we learned about [9] from Noah
Fleming. We would like to thank him for answering some questions on his paper
[2], and sending us the manuscript [9] and for comments on a preliminary
version of this work.

## References

  * [1] Noga Alon and Zoltán Füredi.  Covering the cube by affine hyperplanes.  Eur. J. Comb., 14(2):79–83, 1993.  doi:10.1006/eujc.1993.1011.
  * [2] Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere.  Stabbing planes.  In Anna R. Karlin, editor, 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, volume 94 of LIPIcs, pages 10:1–10:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  doi:10.4230/LIPIcs.ITCS.2018.10.
  * [3] Joshua Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi.  Rank bounds and integrality gaps for cutting planes procedures.  Theory of Computing, 2(4):65–90, 2006.  arXiv:toc:v002/a004.
  * [4] Teena Carroll, Joshua Cooper, and Prasad Tetali.  Counting antichains and linear extensions in generalizations of the boolean lattice, 2009.
  * [5] W. Cook, C. R. Coullard, and G. Turán.  On the complexity of cutting-plane proofs.  Discrete Appl. Math., 18(1):25–38, 1987.  doi:http://dx.doi.org/10.1016/0166-218X(87)90039-4.
  * [6] Daniel Dadush and Samarth Tiwari.  On the complexity of branching proofs.  In Shubhangi Saraf, editor, 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169 of LIPIcs, pages 34:1–34:35. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.CCC.2020.34.
  * [7] Martin Davis, George Logemann, and Donald W. Loveland.  A machine program for theorem-proving.  Commun. ACM, 5(7):394–397, 1962.  doi:10.1145/368273.368557.
  * [8] Martin Davis and Hilary Putnam.  A computing procedure for quantification theory.  J. ACM, 7(3):201–215, 1960.  URL: http://doi.acm.org/10.1145/321033.321034, doi:10.1145/321033.321034.
  * [9] Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson.  On the power and limitations of branch and cut.  In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 6:1–6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.CCC.2021.6.
  * [10] Nicola Galesi, Pavel Pudlák, and Neil Thapen.  The space complexity of cutting planes refutations.  In David Zuckerman, editor, 30th Conference on Computational Complexity, CCC 2015, June 17-19, 2015, Portland, Oregon, USA, volume 33 of LIPIcs, pages 433–447. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.  doi:10.4230/LIPIcs.CCC.2015.433.
  * [11] Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart.  Upper and lower bounds for tree-like cutting planes proofs.  In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pages 220–228. IEEE, 1994.
  * [12] Henry A. Kautz and Bart Selman.  Ten challenges redux: Recent progress in propositional reasoning and search.  In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 1–18. Springer, 2003.  doi:10.1007/978-3-540-45193-8\\_1.
  * [13] Arist Kojevnikov.  Improved lower bounds for tree-like resolution over linear inequalities.  In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 70–79. Springer, 2007.  doi:10.1007/978-3-540-72788-0\\_10.
  * [14] Jan Krajícek.  Discretely ordered modules as a first-order extension of the cutting planes proof system.  J. Symb. Log., 63(4):1582–1596, 1998.  doi:10.2307/2586668.
  * [15] Jan Krajícek.  Interpolation by a game.  Math. Log. Q., 44:450–458, 1998.  doi:10.1002/malq.19980440403.
  * [16] Nathan Linial and Jaikumar Radhakrishnan.  Essential covers of the cube by hyperplanes.  Journal of Combinatorial Theory, Series A, 109(2):331–338, 2005\.
  * [17] Lutz Mattner and Bero Roos.  Maximal probabilities of convolution powers of discrete uniform distributions.  Statistics & probability letters, 78(17):2992–2996, 2008.
  * [18] Fedor Part and Iddo Tzameret.  Resolution with counting: Dag-like lower bounds and different moduli.  Comput. Complex., 30(1):2, 2021.  doi:10.1007/s00037-020-00202-x.
  * [19] Mark Nicholas Charles Rhodes.  On the chvátal rank of the pigeonhole principle.  Theor. Comput. Sci., 410(27-29):2774–2778, 2009.  doi:10.1016/j.tcs.2009.03.035.
  * [20] John Alan Robinson.  A machine-oriented logic based on the resolution principle.  J. ACM, 12(1):23–41, 1965.  URL: http://doi.acm.org/10.1145/321250.321253, doi:10.1145/321250.321253.
  * [21] Bart Selman, Henry A. Kautz, and David A. McAllester.  Ten challenges in propositional reasoning and search.  In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes, pages 50–54. Morgan Kaufmann, 1997.  URL: http://ijcai.org/Proceedings/97-1/Papers/008.pdf.
  * [22] Alasdair Urquhart.  Hard examples for resolution.  J. ACM, 34(1):209–219, 1987.  doi:10.1145/7531.8928.
  * [23] Jacobus Hendricus van Lint and Richard Michael Wilson.  A Course in Combinatorics.  Cambridge University Press, Cambridge, U.K.; New York, 2001.
  * [24] Gal Yehuda and Amir Yehudayoff.  A lower bound for essential covers of the cube.  CoRR, abs/2105.13615, 2021.  URL: https://arxiv.org/abs/2102.05536, arXiv:2102.05536.
  * [25] Gal Yehuda and Amir Yehudayoff.  A lower bound for essential covers of the cube.  arXiv preprint arXiv:2105.13615, 2021.