Extremely Deep Proofs
Noah Fleming†

Toniann Pitassi‡

Robert Robere†

University of California,
San Diego
Memorial University

Columbia University
University of Toronto
IAS

McGill University

November 24, 2021
Abstract
We further the study of supercritical tradeoffs in proof and circuit complexity, which is a
type of tradeoff between complexity parameters where restricting one complexity parameter
forces another to exceed its worst-case upper bound. In particular, we prove a new familyof supercritical tradeoffs between depth and size for Resolution, Res(k), and Cutting Planes
proofs. For each of these proof systems we construct, for each c ≤ n1−ε , a formula with nO(c)clauses and n variables that has a proof of size nO(c) but in which any proof of size no morethan roughly exponential in n1−ε /c must necessarily have depth ≈ nc . By setting c = o(n1−ε )we therefore obtain exponential lower bounds on proof depth; this far exceeds the trivial worstcase upper bound of n. In doing so we give a simplified proof of a supercritical depth/widthtradeoff for tree-like Resolution from [31]. Finally, we outline several conjectures that would
imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting
theorems.

†‡

Research supported by NSERC, the IAS School of Mathematics and NSF Grant No. CCF-1900460.
Research supported by NSERC.

1

Introduction

Beame, Beck, and Impagliazzo recently initiated the study of supercritical tradeoffs in proof and circuit
complexity [4]. In its simplest form, a supercritical tradeoff is a tradeoff between two complexity
parameters in which a restriction on one parameter forces an increase in the second parameter that
goes above the trivial worst-case upper bound on the second parameter. Beame et. al. establisheda supercritical tradeoff between size and space in the Resolution proof system, showing there is anunsatisfiable CNF formula on n variables which admits quasi-polynomial size refutations, but in which
any quasi-polynomial size refutation must also use quasi-polynomial clause-space. Since every formulaon n variables has a Resolution proof of space n + O(1) and exponential size [16], their result showsthat limiting the size of refutations causes the space to go significantly beyond the trivial worst-case
upper bound on the space complexity. Recently, Razborov showed that in certain cases restrictions inparameters can lead to extreme results [31]. He exhibited a strong supercritical size/width for tree-like
Resolution [31], showing that there are unsatisfiable formulas on n variables such that if the width isrestricted, then the tree-like Resolution size must be doubly exponential in n.
Despite the intuitive appeal of supercritical tradeoffs, only a few have been observed and, with the
exception of length versus space, most of these tradeoffs have been for somewhat artificial combinations of parameters. Furthermore, to our knowledge, the existence of supercritical tradeoffs in circuit
complexity has yet to be explored.
In this work we study supercritical tradeoffs between size and depth in both proof complexity andcircuit complexity. For both proof systems and circuit models, depth captures the degree to which they
— and therefore the families of algorithms which they capture — can be parallelized. Furthermore,
for proof systems such as Cutting Planes, depth is closely related to measures of polytope rank whichhave been extensively studied in combinatorial optimization [12,34]. For many standard proof systems(and, indeed, for all of the proof systems studied in this paper) the worst-case upper bound on depth
is always at most n — this is because all of these proof systems can efficiently simulate tree-like
Resolution, which trivially has depth-n proofs for every formula. A supercritical tradeoff in this setting
for a particular proof system P would therefore exhibit a family of CNF formulas over n variables thathave P refutations of size s(n), however there is a size bound s0  s such that any P -refutation ofsize s00  s0 requires depth that is superlinear in n. Similarly, since any n-bit boolean function can becomputed by a fanin-2 circuit of depth at most n, a supercritical tradeoff in this setting would proves
the existence of a function fn with s(n)-size circuits, but for which there is a size bound s0 such thatany circuit of size s00  s0 requires superlinear depth.

1.1Supercritical Size/Depth Tradeoffs in Proof Complexity.

For some sufficiently strong propositional proof systems (such as Frege systems), it is known that
proofs can be balanced: given a Frege proof Π of size s, there exists another Frege proof of the sametautology of size O(s) and depth O(log s). However, for weaker proof systems such as Resolution(Res), k-DNF Resolution (Res(k)), and Cutting Planes (CP), balancing is not always possible. For
example, there are known families of CNF formulas {Fn } with polynomial-size Res proofs, but suchthat any proof requires depth Ω(n/ log n) [1, 11]. However, none of these results have breached thesupercritical threshold, and it was not previously known whether an upper bound of O(n) could beassumed on the depth of short proofs.
Our main result establishes the following supercritical depth/size tradeoffs for Res, Res(k), and CP
refutations, which resolves conjectures made in [18].

1Theorem 1.1. For any constant ε > 0, positive integers k, n sufficiently large, P ∈ {Res, Res(k), CP},1−εand any arbitrary real parameter 1 ≤ c < n 2+ε , there is a CNF formula F on n variables and nO(c)clauses such that
• There is a P-refutation of F of size nO(c) .
• If Π is a P-refutation of F with size(Π) = 2o n1−ε2+ε /c2depth(Π) log size(Π) = Ωthennc/(2+ε)c log n

!
.

Ω(1)

2n

depth

Ω(1)

2n

poly(n)gap

Figure 1: A depiction of our size/depth tradeoffs as we range the compression parameter c. The depth
value represents the depth required to refute the formula F , while the gap value represents by how
much the size of the minimal P-proof of F needs to be increased before the supercritical depth lower
bound no longer holds.
Varying the “compression parameter” c between O(1) and nδ (for some small constant δ) allows
us to obtain an interesting family of tradeoff results; this is depicted in Figure 1. In one extreme, whenc = O(1) we obtain a formula F which has refutations of size poly(n), however any proof of size1−ε
 2nmust have depth that is polynomial (and superlinear!) in n. In the other extreme, settingc = nδ implies formulas with exponential-size (in n; the refutations are polynomial in the size of theformula) and exponential-depth refutations, but any refutation must have exponential depth.
Our proof builds on Razborov’s hardness condensation method [31]; we briefly describe Razborov’s
method next, and a detailed description is given in Section 3. Let F be a CNF formula over N variables
satisfying the following properties:
1. There are Resolution refutations of F with small size.
2. Any Resolution refutation of F requires depth d(N ).
The strategy is to find a way to compress the variables y1 , . . . , yN of F to a much smaller set of variables
x1 , . . . , xn with n  N in a way which preserves the depth lower bound. Indeed, we will argue that any
small refutation of the compressed formula must have depth approximately d(N ). We stress that the2lower bound of d(N ) is in terms of the original number of variables N , and therefore if n is sufficiently
small compared to N , we obtain a supercritical depth lower bound for small proofs. Razborov provedthat such a compression argument was possible for tree-like Resolution, assuming that the width of therefutation is bounded [31]. As a secondary contribution, we give a significantly simplified proof of thistradeoff in Section 5 using the “top-down” language of Prover-Adversary games.
Once we have established our size/depth tradeoff for Resolution using the aforementioned strategy,
the lower bounds for CP and Res(k) are straightforward applications of lifting theorems. For CP, weutilize the depth-preserving lifting theorem of Garg et al. [20]. For Res(k), we show how the lower
bound of Segerlind et al. [35] immediately gives rise to a lifting theorem for Res(k) which preserves
depth.
Supercritical Tradeoffs for Tseitin and Matching. The Tseitin formulas have a storied history in
proof complexity. They were one of the first examples shown to be hard to refute in Resolution,
and were long conjectured to also be exponentially hard for Cutting Planes. Recently, [13] disproved
this conjecture, obtaining quasipolynomial-size Cutting Planes refutations for the Tseitin formulas bytranslating an upper bound in the Stabbing Planes proof system [5] into Cutting Planes. Their upperbound was generalized in [18], which showed that any unsatisfiable system of equations over a prime
finite field also have quasipolynomial-size CP refutations. Quite interestingly, in both cases the CP
refutations not only have quasipolynomial size but also have quasipolynomial depth — that is, thedepth of these proofs is supercritical. In [18], it was conjectured that there are unsatisfiable formulas
such that any small CP refutation requires superlinear depth, and moreover, they conjectured that the
Tseitin formulas are an example of such formulas. We restate this conjecture for Tseitin formulas next.
Conjecture 1.2. There is an unsatisfiable system of mod2 linear equations such that any proof of
quasipolynomial size requires depth that is superlinear in n (or even quasipolynomial).
One potential interest in resolving this conjecture is the similarity between the Tseitin formulas
and related counting principles and the perfect matching function. The seminal paper of Razborov [30]proved that monotone circuits for matching require quasipolynomial size, and it is also known thatmonotone circuits require linear depth [29]. Furthermore, it is known [19, 22, 27] that small Cutting Planes proofs imply small monotone circuits. This brings up the intriguing possibility that thesize/depth of Cutting Planes proofs the Tseitin formulas could inform the size/depth monotone circuits
for perfect matching.

1.2

Supercritical Tradeoffs for Boolean Circuits.

It is well-known that every monotone function has monotone circuits of depth at most n. We ask if
every monotone function with polynomial monotone circuit complexity can also be computed by amonotone circuit of both polynomial size and linear depth. For monotone circuits, it is known that it is
not possible to reduce the depth below n/polylogn while maintaining polynomial size [14]. However,these tradeoffs are proven using communication complexity, and are therefore limited to size/depth
tradeoffs where the depth is at most n.
Conjecture 1.3. There exists a monotone function which admits polynomial size monotone circuits, but
any circuit of depth at most n1+ for some ε > 0 requires superpolynomial-size monotone circuits.
One promising avenue for resolving the this conjecture is to lift our supercritical tradeoffs for
Resolution to supercritical tradeoffs for monotone circuits. Indeed, lifting has already been used toobtain monotone circuit lower bounds from Resolution lower bounds [20].
3In more detail, using lifting techniques it is known that given an unsatisfiable formula F , Resolution size lower bounds for F imply monotone circuit lower bounds for a related monotone function,mCSP-SATF . Stated contrapositively, given a small circuit C for mCSP-SATF , one can extract asmall Resolution refutation for F of roughly the same size. Moreover, the structure of C is nearly thesame as the structure of the Resolution refutation — thus if C has small size and depth, then F also has
a Resolution refutation of small size and depth. It follows that a strong enough supercritical size/depth
tradeoff for Resolution would imply a supercritical size/depth tradeoff for monotone circuits as well!
Unfortunately, our current supercritical tradeoff for Resolution isn’t strong enough to obtain interesting size/depth tradeoffs for monotone circuits for the following reason. The reduction from monotone circuits for mCSP-SATF to Resolution proofs of F incurs a seemingly necessary blowup in theparameters — the number of clauses m in F corresponds to the number of variables in mCSP-SATF ,and thus in order to prove a supercritical tradeoff for monotone circuit complexity via this route, one
needs to prove the following strong supercritical tradeoff:
Conjecture 1.4. There are families of unsatisfiable formulas {Fn } with m = m(n) clauses such that
Fn has Resolution refutations of size polynomial in m, but any polynomial-size (or subexponential-size)
refutation of Fn requires depth that is superlinear in m.
Under this conjecture, we obtain supercritical tradeoffs for monotone circuits, which we prove in
Section 7. We note that it is entirely possible that the above conjecture is false — that is, it seems
possible that Resolution refutations could be balanced to depth O(m) without incurring a significant
increase in size. Indeed, a potentially relevant construction is the classic work of Ben-Sasson and√
Wigderson [7] which converts a size s Resolution refutation into a refutation of low width ( n log s).
The next problem asks whether their construction can be improved to keep low width and low depth.
Problem 1.5. Prove or disprove that for any k-CNF formula on m clauses and n variables,√ any size s
Resolution refutation can be converted into a refutation of depth O(m) and width k + O( n log s).
A positive resolution to the above problem would give a counterexample to our conjecture andwould also give a very surprising upper bound on the depths of arbitrary Resolution proofs, while anegative answer would imply (conditional) supercritical tradeoffs for monotone circuits (see Section 7).
Given this “win-win” situation, we believe that studying this problem is of fundamental interest for
future work.
Thirdly, we ask about supercritical size/depth tradeoffs for non-monotone circuits.
Conjecture 1.6. There is a function f with polynomial-size circuits but for which any polynomial-size
circuit requires superlinear depth.
Given that an unconditional supercritical tradeoff for general circuits is beyond the reach of current
techniques, it is even interesting to prove such a tradeoff under a standard complexity assumption, suchas those concerning the existence of one-way functions or other cryptographic primitives.

1.3

Related Work

Besides the work of Beame, Beck and Impagliazzo [4] and Razborov [31], several supercritical tradeoffs have been observed in proof complexity. Razborov [32] considered a notion of width for Cutting Planes, which measures the number of distinct variables with non-zero coefficients which appear
in a Cutting Planes line. Using similar machinery as in [31], Razborov established a supercritical
width/depth tradeoff for CP.
4

Much of the work on supercritical tradeoffs has focused on notions of proof space. Extending
Beame et al. [4], Beck et al. [6] exhibited supercritical size/clause-space tradeoffs for the Polynomial
Calculus. Berkholz and Nordström [9] exhibited a strong supercritical tradeoff between width andclause-space for Resolution, and Razborov [33] established a supercritical tradeoff between variablespace and size for Resolution. Finally, Papamakarios and Razborov [25] showed that separating clauseor monomial-space from proof size for tree-like Resolution is the equivalent to showing a supercriticalclause-space/depth tradeoff.
Proof Depth and Algorithm Analysis. One of the primary motivations for studying tradeoffs inproof complexity is the existence of deep connections to the analysis of practical algorithms. Proofsystems in a specific, formal sense correspond to families of efficient, provably correct algorithms. For
example, Resolution captures the reasoning used in state-of-the-art (CDCL) algorithms for SAT, while
Cutting Planes (CP) was introduced in order to model a broad family of optimization algorithms used
in integer programming based on Chvátal-Gomory cuts. Therefore resource tradeoffs for these proof
systems apply to the corresponding family of algorithms. The depth in proofs captures the degree towhich the associated families of algorithms can be paralellized, and so supercritical size/depth tradeoffs
imply that the associated families of algorithms are inherently sequential in the worst case.
As well, the depth of Cutting Planes proofs has been thoroughly studied in integer programming
theory under the name of Chvátal rank [12]. A number of results in this area obtained nearly tightworst-case bounds on the Chvátal rank of a number of polytopes [10, 15, 34]. Our main result implies
Chvátal rank lower bounds that are exponentially stronger than previously known, under the condition
that the Chátal-Gomory Cutting Planes procedures is efficient.

2Preliminaries

We recall some preliminaries from proof complexity. A clause C is a disjunction of boolean literals,
and the width of a clause is the number of literals in C. If C = C1 ∧ C2 ∧ · · · ∧ Cm is a CNF formulathen the width of C, denoted width(C), is the maximum width of any clause in C.
Resolution. Fix an unsatisfiable CNF formula F over variables x1 , . . . , xn . A Resolution (Res) refutation of F is a sequence of clauses {Ci }i∈[s] ending with the empty clause Cs = ⊥ such that each Ci
is either in F or is derived from earlier clauses Cj , Ck with j, k < i by one of the following inference
rules:
• Resolution. Ci = (Cj \ {`k }) ∪ (Ck \ `k ) where `k ∈ Cj , `k ∈ Ck is a literal.
• Weakening. Ci ⊇ Cj .
The size of a Res proof Π of F is s, the number of clauses in Π, and we denote by sizeRes (F ) the
minimum size of any Res proof of F . The size of resolution proofs is intimately related to their width,
width(Π), which is the maximum number of literals occurring in any clause in the proof.
Any Res proof can be represented as a directed acyclic graph (DAG) in which the nodes represent
clauses in the proof, each clause of F has in-degree 0 and, and any other clause has at most two
incoming arcs from the at most two clauses that produced it. With this in mind, we can define the depthof a Res proof to be the length of the longest root-to-leaf path in the proof, and denote by depthRes(F )the minimum depth of any Res proof of F . It is not difficult to see that for any CNF formula F ,sizeRes (F ) ≤ 2n and depthRes (F ) ≤ n.
5One can obtain generalizations of Res by allowing the proof system to have more general types ofboolean formulas as lines. In this paper, we will also be interested in the proof system Res(k) which
operates with k-DNF formulas. The details of particular rules of this proof system will not be necessary
for us, however we introduce them for completeness.
DNF Resolution. Let F be an unsatisfiable CNF formula over variables x1 , . . . , xn and let k besome fixed constant. A k-DNF Resolution (Res(k)) refutation of F is a sequence of k-DNF formulas {Di }i∈[s] such that Ds = Λ and each Di is either a clause of F or is deduced from earlier k-DNFs
by one of the following inference rules, where a literal `i is either xi or ¬xi :• Cut. From k-DNFs A ∨ (∧i∈I `i ) and B ∨ (∨i∈I ¬`i ) deduce A ∨ B.
• Weakening. From a (k − 1)-DNF A deduce A ∨ ` for any literal `.
• ∧-Introduction. From {A ∨ `i }i∈I deduce A ∨ (∧i∈I `i ).
• ∧-Elimination. From A ∨ (∧i∈I `i ) deduce A ∨ `i for any i ∈ I.
The size of a Res(k) refutation is s, the number of DNFs in the resolution, and the depth of the refutationis the length of the longest path in the proof DAG. Since Res = Res(1), there is a Res(k) refutation ofsize 2n and depth n of any CNF formula.
The final proof system which we will be interested in is of the algebraic variety, refuting the existence of integer solutions to systems of linear inequalities. We can encode a CNF formula F overvariables x1 , . . . , xn as an equisatisfiable system of linear
W in the following way. First, inWinequalities
troduce inequalities 0 ≤ xi ≤ 1 for all i ∈ [n]. If Ci = i∈I xi ∨ j∈J ¬xi is a clause in F , add theinequalityXX
xi +(1 − xi ) ≥ 1.
i∈I

j∈J

It is not difficult to see that the {0, 1}-solutions to F are exactly the solutions to this system of inequalities.
Cutting Planes and Semantic Cutting Planes. Let P be a system of integer-linear inequalities whichis infeasible over Zn . A Cutting Planes (CP) refutation of P is a sequence of integer-linear inequalities{ai x ≥ bi }i∈[s] ending with the trivially false inequality 0 ≥ 1 such that each inequality is either
belongs to P , or is deduced from earlier inequalities by one of the following inference rules:• Linear Combination. From ax ≥ b, cx ≥ d deduce any non-negative linear combination withinteger coefficients.
• Division. From ax ≥ b, if d ∈ Z with d ≥ 0 divides a, deduce (a/d)x ≥ db/de.
The rules of Cutting Planes preserve integer solutions, and therefore a refutation exists if and only if P
is infeasible over Zn .
The following transformation will allow us to talk about Cutting Planes refutations of CNF formulas. We can encode a CNF formula F over variables x1 , . . . , xn as an equisatisfiable system ofinteger-linear
in the following way. First, introduce inequalities 0 ≤ xi ≤ 1 for all i ∈ [n].
W inequalitiesW
If Ci = i∈I xi ∨ j∈J ¬xi is a clause in F , add the inequalityXX
xi +(1 − xi ) ≥ 1.
i∈I

j∈J

6

Observe that the satisfying assignments to F are exactly the integer solutions to the resulting system of
linear inequalities. With this transformation we will say that a Cutting Planes refutation is a refutationof F if it is a refutation of the associated system of linear inequalities.
The semantic Cutting Planes (sCP) proof system is a strengthening of CP to allow any deduction
which is sound over boolean points. Like CP, an sCP refutation of a CNF formula F is a sequenceof integer-linear inequalities {ai x ≥ bi }i∈[s] , however we are now permitted to use the following
extremely strong semantic deduction rule:• Semantic Deduction. From previously derived inequalities ax ≥ b, a0 x ≥ b0 , deduce any inequality cx ≥ d such that every {0, 1} assignment satisfying both ax ≥ b and a0 x ≥ b0 alsosatisfies cx ≥ d.
The size of a CP or sCP refutation is the number of inequalities s appearing in it. As well, analogous to
Resolution, the depth of a refutation is the longest root-to-leaf path in its representation as a DAG. It is
not difficult to see that any Res proof can be transformed into CP (and therefore sCP) while preserving
both the size and depth up to a constant factor, and therefore there is always a CP refutation of any
CNF formula F which has size 2n and linear depth.
Filmus et al. [17] showed that sCP can be significantly more expressive than CP: there are formulaswith polynomial size sCP proofs requiring exponential size proofs in CP. In fact, inferences made withthe semantic deduction rule are not even verifiable in polynomial time unless P = NP.

3

Proof Overview

Our proof will follow the general approach of Razborov [31], which established a supercritical width/size
tradeoff for tree-like Resolution. The key machinery in his proof is a technique — which has beentermed hardness condensation — that compresses the number of variables of the formula F in sucha way that the depth of any bounded width tree-like resolution refutation of the compressed formularemains proportional to the tree-like resolution depth of refuting F .
The compression is done by composing the formula F with an XOR gadget. However, unlike
standard lifting theorems, the XOR gadgets will be defined on overlapping sets of variables. This willallow us to reduce the total number of variables of the composed function.
XOR Substitution. Let G = ([N ] ∪ [n], E) be a bipartite graph and {y1 , . . . , yN }, {x1 , . . . , xn }be sets of propositional variables. For a clause C in the variables {y1 , . . . , yN } we will denote by
C ◦ XORG the CNF obtained from C by the F2 -linear substitution
M
yi 7→
xj ,
j:(i,j)∈E

and then rewriting the formula in CNF (see Figure 2). For a CNF F , let F ◦ XORG be the CNF formulathat results from this substitution. If the clauses of F have width at most k and G has left-degree at
most `, then F ◦ XORG is a CNF formula on n variables and at most m · 2k`−1 clauses of width at most`k.
Similarly, we write F ◦ XORN
2 to represent the CNF formula obtained by the substitution yi 7→
ui ⊕ vi for each i, where ui and vi are new variables.

7

[N ] = [nc ]x1 ⊕ x2[n]x1 ⊕ x3x3

x2 ⊕ x3
x2
x1 ⊕ x3
x1

x1 ⊕ x2
x1 ⊕ x3`

Figure 2: The bipartite graph G, together with the XOR constraints that each left-vertex (y-variable) is
replaced with.
Now, if G disperses the variables of [n] among the gadgets in such a way that learning the value of
yi does not reveal too much information about the values of any yj , then the best-possible Res proof
should essentially be one which simply simulates the proof for F . Indeed, Razborov proved that this is
the case under the assumption that G has sufficiently strong expansion properties. For S ⊆ [n], letΓ(S) := {yi ∈ [N ] : ∃xj ∈ S, (yi , xj ) ∈ E}
be the neighbourhood of S in G. The following definition records the expansion properties of bipartite
graphs that we will use.
Boundary Expansion. For a bipartite graph G = (U ∪ V, E) the boundary of a set W ⊆ U isδ(W ) := {v ∈ V : |Γ(v) ∩ W | = 1}.
The boundary expansion of a set W ⊆ U is |δ(W )|/|W |. The graph G is a (r, s)-boundary expander
if the boundary expansion of every set W ⊆ U with |W | ≤ r has boundary expansion at least s.
That is, G is a boundary expander if for any small enough subset of left-vertices, the number of
unique neighbours is large.
We are now ready to state Razborov’s hardness condensation theorem. [31]. We note that Razborov
originally proved his theorem for the case of tree-like Resolution, but (as we will see) it also holds forgeneral Resolution.
Depth Condensation Theorem. Let F be an unsatisfiable CNF formula on N variables and let G =([N ] ∪ [n], E) be an (r, 2)-boundary expander. If Π is a Resolution refutation of F ◦ XORG withwidth(Π) ≤ r/4, thendepthRes (F )depth(Π)width(Π) ≥.
28

In Section 5, we give a simplified proof of Depth Condensation Theorem. By combining thistheorem with known reductions from Resolution size to Resolution width [20, 35], we are able toestablish the following depth-to-size lifting theorems. When instantiated, these will allow us to prove
our tradeoffs.
Theorem 3.1. Let F be any CNF formula on N variables and let G = ([N ] ∪ [n], E) be an (r, 2)boundary expander. If Π is a resolution refutation of F ◦ XORG ◦ XORn2 such that log(size(Π) + 1) ≤r/12, thendepthRes (F )depth(Π) log(size(Π) + 1) ≥.
6
Theorem 3.2. Let k ≥ 1 be any constant, let F be any CNF formula on N variables, and let G =([N ] ∪ [n], E) be an (r, 2)-boundary expander. There is a constant δ := δ(k) > 0 such that if Π is aRes(k) refutation of F ◦ XORG ◦ XORn2 with log(size(Π) + 1) ≤ δ · r, then
depth(Π) log2 (size(Π)) = Ω depthRes (F )To obtain the depth-to-size lifting theorem for semantic Cutting Planes, we will instead use thet-bit index function as our outer gadget. Recall that INDt : [t] × {0, 1}t → {0, 1} maps (x, y) to yx .
For a CNF formula on variables z1 , . . . , zn , let F ◦ INDnt be the CNF formula obtained from F by
the substitution zi 7→ INDt (xi , yi ) on new sets of variables xi , yi . Note that if F is an unsatisfiable
k-CNF formula with m clauses, then F ◦ INDnt is an unsatisfiable CNF formula on O(nt) variables andO(tmk + n) clauses.
Theorem 3.3. Let ε > 0 be any constant, let F be any CNF formula on N variables, and let G =([N ] ∪ [n], E) be an (r, 2)-boundary expander. There is a constant δ > 0 such that if Π is a semantic
CP refutation of F ◦ XORG ◦ INDnn1+ε with log(size(Π)) ≤ δ · r log n, thendepth(Π) log2 (size(Π)) = Ω(depthRes (F ) log2 n).
We delay the proofs of these theorems until Section 6. Instead, we will first instantiate them toobtain our tradeoffs.

4

Parameterizing the Tradeoffs

From the previous theorems we can obtain a family of supercritical tradeoffs. To do so, we will needa formula which has small resolution refutations, but requires large depth. The canonical example ofsuch formulas are the pebbling formulas of [1] on some hard-to-pebble graph H. It is known that for
N -vertex graph H, PebH has resolution refutations of size O(N ) and width O(1). However, resolution
depth required to refute these formulas is equal to the reversible pebbling number of the graph [11].
Furthermore, there exist O(1)-degree graphs with reversible pebbling number Ω(N/ log N ) [26].
By combining the lower and upper bounds for the pebbling formulas with the previous lemmas we
can obtain a family of supercritical tradeoffs by varying the underlying expander graph G = ([N ] ∪[n], E). The following lemma provides us with a sufficient family of expander graphs.
Lemma 4.1 (Razborov [31]). Let n be any sufficiently large positive integer, and let N, r, ` be positive
integers depending on n such that ` ≥ 4. If
rN 4/` = o(n/`)
then an (r, 2) boundary expander G = ([N ] ∪ [n], E) exists with left-degree `.
9Our tradeoffs will be in terms of the number of variables n that we are“compressing” [N ] into. It
will be convenient to set N = nc , for some real parameter c ≥ 1, which we will call our compression
parameter. As well, let ε > 0 be some arbitrarily small real parameter. We will set
N := nc ,r := n1−ε /c,` := 8c/ε.
We can verify that1n1−ε/21= o(n/`).
rN 4/` = n1−ε n4c/` ≤ n1−ε nε/2 =cccNow, choosing different ranges of c allow us to obtain the following interesting tradeoff results.
For convenience, we record the following proposition stating how the parameters of F transform
under composition.
Proposition 4.2. Let H be any graph on N vertices with indegree O(1). Let G = ([N ] ∪ [n], E) be a
bipartite graph with left-degree at most `. Then,• PebH has N variables, N + 1 clauses, and width O(1).
• PebH ◦ XORG ◦ XORn2 has 2n variables, n2O(`) clauses, and width O(`).
• PebH ◦ XORG ◦ INDnn1+ε has O(n2+ε ) variables, nO(`) clauses, and width O(`)
Proof. We obtain PebH ◦ XORG by replacing each variable yi with an XOR of at most ` variables.
After expanding, this yields a CNF formula with n2(`−1)width(PebH ) + n = n2O(`) clauses and widthO(`). Composing this with XOR2 has the same effect. To handle composition with the index gadget,
we use the encoding of [20] which, for any k-CNF formula F on n variables and m clauses, encodes
F ◦ INDnn1+ε as a 2k-CNF formula on O(n2+ε ) variables and O(m · nk(1+ε) ) clauses. For our choiceof parameters, including ε > 0 an arbitrarily small constant, this will be nO(`) .
Now we can test different parameter regimes. In each of our regimes our tradeoffs are basically as
follows: we have a trivial proof of size 2n and depth n. However, if we demand that the proof has size
1−ε
 2n , then the depth of the proof will explode to roughly nc (which is supercritical in that it lies
above the worst-case upper bound of n). Increasing c obviously increases the final depth lower bound,but since we must choose ` = O(c) it also increases the number of clauses proportionally. We firststate a general tradeoff parameterized by c (a formal version of Theorem 1.1), and then instantiate c.
Theorem 4.3. For all constants ε > 0, positive integers k, n sufficiently large, P ∈ {Res, Res(k), CP},and arbitrary real parameter c ≥ 1, there is an unsatisfiable CNF formula FP on n variables such that
• If P = Res, then FP has a resolution refutation of size nc · 2O(c) . However, any resolution
1−εrefutation Π of FP with size(Π) = 2o(n /c) satisfiesnc
depth(Π) log size(Π) = Ω.
c log n10• If P = Res(k), then FP has a Res(k) refutation of size nc ·2O(c) . However, any Res(k) refutation1−εΠ of FP with size(Π) = 2o(n /c) satisfies
nc2
depth(Π) log (size(Π)) = Ω
c log n• If P = sCP, then FP has a sCP refutation of size nO(c) . However, any sCP refutation Π of FP
1−εwith size(Π) = exp o n( 2+ε ) /c satisfies!
c/(2+ε) log nn.
depth(Π) log2 (size(Π)) = Ωc
Proof. Let the parameters N, r, ` be set as above, and let G = ([N ] ∪ [n], E) be an (r, 2)-boundary
expander whose existence is guaranteed by Lemma 4.1. Let H be any directed graph on N vertices
with indegree O(1) whose reversible pebbling number is Ω(N/ log N ). Then PebH requires resolution
refutations of depth Ω(N/ log N ), but has resolution refutations of size O(N ). For Res and Res(k),let F be PebH ◦ XORG ◦ XORn2 . The lower bounds on F follow from Theorem 3.1 and Theorem 3.2.
For the upper bound, we simulate the upper bound for PebH : every time the resolution proof for PebH
would query a variable yi , we query all of the variables that yi was replaced with in F ; that is, we query
all uj , vj such that (i, j) is an edge of G, in order to evaluateM(uj ⊕ vj ),j:(i,j)∈E

which gives a value for yj . Because the left-degree of G is at most `, we query at most 2` = O(c)variables. This can be done in a subproof (a decision tree) of size 2O(c) . Altogether, this is a refutationof size N · 2O(c) = nc · 2O(c) of F .
For sCP, let F be PebH ◦ XORG ◦ INDnn1+ε . By Proposition 4.2, F has O(n2+ε ) variables. The
lower bound follows from Theorem 3.3 together with the lower bound on PebH . For the upper bound,note that INDn1+ε can be evaluated in resolution by querying (1+ε) log n+1 variables (the (1+ε) log n“pointer variables” x together with the single bit yx ). Thus, by following the same strategy as before,
we can simulate the resolution refutation of PebH by every time the Res refutation queries a variable
yi , evaluating the index gadgets of all j ∈ [n] such that (i, j) ∈ E. As G has left-degree at most `,evaluating yi can be done by querying at most ` · ((1 + ε) log n + 1) variables. This results in a Res(and therefore sCP) refutation of size N · 2`·((1+ε) log n+1) = nO(c) .
In what follows we will explore different ranges of the compression parameter c. The next corollaries are somewhat lossy, as they are stated in order to hold simultaneously for resolution, Res(k), andsCP. The first interesting regime is when c = O(1). In this case, F is a polynomial size and constant1−εwidth formula which has a trivial depth n and size 2n proof, however any refutation of size  2n ,for some ε > 0, must have polynomial depth.
Corollary 4.4. Let c = O(1) be any constant, let ε > 0 be an arbitrarily small constant, and let∆sCP = 1 + ε and ∆Res = ∆Res(k) = 0. For any P ∈ {Res, Res(k), CP} there is a CNF formula FP
on n variables, such that
• There is a P-refutation of FP of size poly(n).
11

1−ε

• Any P-refutation Π of FP with size(Π) = exp(o(n 1+∆P )) has depth(Π) = Ω̃(nc/(1+∆P ) ).
The second interesting regime is when c = logO(1) n. In this case, we are compressing the numberof variables quasipolynomially, and we obtain quasipolynomial depth lower bounds for small proofs.
Corollary 4.5. Let c = logO(1) n and let ε > 0 be an arbitrarily small constant, and let ∆sCP = 1 + ε
and ∆Res = ∆Res(k) = 0. For any P ∈ {Res, Res(k), CP} there is a CNF formula FP on n variables,such that• There is a P-refutation of FP of size 2log

O(1)

n.
1−ε

• Any P-refutation Π of FP has with size(Π) = exp(õ(n 1+∆P )) has depth(Π) = Ω̃(nlog

O(1)

n ).

Finally, we would like to test how large we can set c. The best possible compression afforded by
Theorem 4.3 is c = nδ for some small constant δ > 0. Surprisingly, this implies an exponential blowup
in the depth.
Corollary 4.6. Let ε > 0 be an arbitrarily small constant, and let ∆sCP = 1+ε and ∆Res = ∆Res(k) =0. For P ∈ {Res, Res(k), CP} and any 0 < δ < (1 − ε)/(1 + ∆). There is a CNF formula FP on nvariables such thatδ• FP has a P-refutation of size 2O(n / log n) .
1−ε• Any P-refutation Π of FP with size(Π) = exp(o(n 1+∆P

5−δ)) has depth(Π) = exp(Ω(nδ )).

Proof of the Depth Condensation Theorem

In this section we prove the Depth Condensation Theorem. To do so, it will be convenient to workwith the following variant of the classic Prover-Adversary games of Pudlák [28] (this game was also
considered in the work of Atserias and Dalmau [3]). Our variant characterizes the depth of boundedwidth Resolution proofs.
Width–Bounded Prover–Adversary Game. The Prover–Adversary game associated with an n-variate
formula F is played between two competing players, Prover and Adversary. The game proceeds inrounds, where in each round the state of the game is recorded by a partial assignment ρ ∈ {0, 1, ∗}n tothe variables of F . Initially the state is the empty assignment ρ = ∗n . Then, in each round, the Prover
performs the following:• Query. The Prover chooses an i ∈ [n] with ρi = ∗, and the Adversary chooses b ∈ {0, 1}. The
state is updated by ρi ← b and play continues.
• Forget. The prover chooses a (possibly empty) set S ⊆ [n] with ρi 6= ∗ for all i ∈ S. The stateis updated by ρi ← ∗ for all i ∈ S.
The game ends when the state ρ falsifies an axiom of F .
Let w > 0 be an integer. A Prover–Adversary game is a w-bounded Game if at every step in game,the Prover’s memory ρ remembers assignments to at most w variables; i.e., |[n] \ ρ−1 (∗)| ≤ w.
We will say that a game is non-bounded if it is not necessarily w-bounded. The next lemma is
precisely Lemma 6 in [8], and can be proved using the methods of Pudlák [28].
12Lemma 5.1. For any unsatisfiable k-CNF formula F , there is a depth d, width w ≥ k resolution
refutation of F if and only if there the Prover has a strategy that ends the (w + 1)-bounded game in drounds, regardless of the strategy for the Adversary.
Proof. Let Π be a resolution proof of width w and depth d. We extract a strategy for the Prover asfollows: the Prover will take a root-to-leaf walk down the proof. At each step, corresponding to someclause C in the resolution proof, she will maintain that she is remembering exactly the unique falsifying
assignment ¬C to the clause C. If C was obtained by resolving C1 ∨ x and C2 ∨ ¬x then she willquery the variable x. If the Adversary responds with x = 0 then she will move to C1 ∨ x and forget all
assignments except for ¬C1 ∧ ¬x. Proceeding in this way, we arrive at a leaf C of Π in at most d steps.
By our invariant, the Prover remembers at most w + 1 variables at any point.
As the converse direction will not be used in our proofs, we only provide a sketch of the argument.
We can view the Prover’s strategy for a (w + 1)-bounded game as a dag, where every node is labelledwith the memory of the Prover at that step in the strategy, along with the variable that the Prover queries,
and there are two outgoing edges labelled 0 and 1 respectively, corresponding to possible answers of
the Adversary. For each node labelled with some memory ρ and variable x, we will relabel it with theclause formed by the negation of the literals fixed by ρ, which will be obtained from its children byresolving on x.
Let us set up some notation. Let G = ([N ] ∪ [n], E) be a bipartite graph; we will think of theleft-vertices as the variables of F and the right-vertices as the variables of F ◦ XORG . For a set S ⊆ [n]of right-vertices of G, denote by
Fixed(S) := {i ∈ [N ] : ∀(i, j) ∈ E, j ∈ S}
the set of left-vertices which become isolated after removing the set S of right vertices. Similarly, fora partial assignment ρ ∈ {0, 1, ∗}n let Fixed(ρ) := Fixed(S), where S = [n] \ ρ−1 (∗), be the set ofvariables of F which are determined by ρ. Finally, let G  ρ denote the graph obtained by removing allleft-vertices that have been set by ρ (i.e., those in [n] \ ρ−1 (∗)), and removing all isolated vertices.
Proof Overview. First, we give a high-level sketch of the proof. Let F be a CNF formula which
requires depth d to refute in resolution. This gives us a strategy for the Adversary (for the non-boundedgame) which ensures that it will proceed for at least d rounds. We will use this strategy to construct a
strategy for the Adversary in the w-bounded–game for F ◦ XORG . Ideally, we would like to proceed asfollows: if the Prover (in the w-bounded game for F ◦ XORG ) queries a variable, we would like to set it
according to the Adversary strategy of the non-bounded game for F if it would determine the value ofsome variable yi of F , that is, i would be added to Fixed(ρ), and set it arbitrarily otherwise. However,in this setting the XOR gadgets may share variables and so variables may be correlated. To circumvent
this, we will exploit expansion. Indeed, if G is a good enough boundary expander, then we can always
set the constraints to whatever value we like. That is, for any subset I ⊆ [N ] of XOR-constraints, we
can always find a strong system of distinct representative variables.
Strong SDR. If G = ([N ] ∪ [n], E) is a bipartite graph and I = {I1 , . . . , It } ⊆ [N ] then a system of
distinct representatives (SDR) for I is a set J = {J1 , . . . , Jt } ⊆ [n] such that I and J form a matchingwhere (Ii , Ji ) ∈ E for all i ∈ [t]. The SDR of I is strong if, furthermore, Ii is not adjacent to Jj for all
j > i.
The following lemma can be viewed as a strengthening of the claim that expanders have matchingson small sets.
13

Lemma 5.2. If G = ([N ] ∪ [n], E) is an (r/2, 1/2)-boundary expander, then any I ⊆ [N ] with|I| ≤ r/2 has a strong SDR.
Proof. For i = 1 . . . t perform the following. Because I has boundary at least |I|/2 within G, by the
pigeonhole principle there exists ` ∈ I and a column j ∈ [n] such that (`, j) ∈ E and (`0 , j) 6∈ E forevery `0 ∈ I with `0 6= `; fix Ii := ` and Ji := j. Set G to be the graph obtained by removing vertices
Ii and Ji and any edge incident to either of them, and update I ← I \Ii . Because Ji was not adjacent toany vertex besides Ii , removing Ji does not decrease the expansion of I in G and we can recurse.
If a partial restriction ρ ∈ {0, 1, ∗}n (thought of as the Prover’s memory) sets some variables,
this may decrease the boundary expansion of the current graph G  ρ. Therefore, at each step of thesimulation, the Adversary will track a closure of ρ which will set some additional variables, but will
ensure that the residual graph is a good boundary expander. The following operator will allow us torestore the expansion of G after removing a subset of the vertices.
Closure Operator. For a J ⊆ [n], denote by G \ J the graph obtained by taking the subgraph inducedby the vertex set [N ] ∪ ([n] \ J) and removing any isolated vertices (i.e. yi for which i ∈ Fixed(J))
from [N ]. The following lemma states that for any small J there is a closure Cl(J) ⊇ J such thatG \ Cl(J) is still expanding; a proof can be found in [31] (Lemma 2.3), building on ideas in [2, 35].
Lemma 5.3. Let G = ([N ]∪[n], E) be an (r, 2)-boundary expander. For every J ⊆ [n] with |J| ≤ r/4
there exists Cl(J) ⊇ J such that |Fixed(Cl(J))| ≤ 2|J| and G \ Cl(J) is an (r/2, 3/2)-boundary
expander.
We are now ready to prove the main theorem of this section.
Proof of the Depth Condensation Theorem. Fix an optimal strategy D for the Adversary (in theunbounded game) which delays the game for at least d rounds on F . We will construct a Adversary
strategy for the w-bounded game which delays the game for at least d/2w rounds on the composed
formula F ◦ XORG for any w ≤ r/4. We denote Prover’s memory at each step in the game byρ ∈ {0, 1, ∗}n , and let set(ρ) be the collection of coordinates i ∈ [n] such that ρi ∈ {0, 1}. We also
track a partial assignment ρ∗ ⊇ ρ that satisfies following invariants:– Expansion. G \ set(ρ∗ ) is an (r/2, 3/2)-boundary expander.
– Satisfying. ρ∗ does not falsify any of the constraints of F ◦ XORG .
Initially ρ = ρ∗ = ∗n and the invariants are satisfied.
In each round we will query the Adversary strategy D at most 2w times. Suppose that we (as theAdversary) have played for less than d/2w rounds such the invariants are satisfied, then we can claim
we can continue for another round and restore the invariants.
So, suppose in the current round that the Prover queries the variable xi . If i ∈ set(ρ) then we assign
ρi = ρ∗i ; otherwise, we simply respond with an arbitrary bit. The Prover then chooses an arbitrary setof indices I ⊆ set(ρ) and forgets all assignments in them. Let µ ⊆ ρ ∪ {xi = b} denote the partial
assignment after the Adversary responds and the Prover forgets the chosen subset.
First, we note that by the Expansion invariant, each constraint not in Fixed(set(ρ∗ )) had at least
two free variables before xi was set, and therefore setting xi could not have fixed any of the XORs. So,
we only need to describe how to restore the invariants. If G \ set(µ) is a (r/2, 3/2)-boundary expander
then we are done: we simply update ρ = ρ∗ = µ and continue to the next stage. The interesting case iswhen G \ set(µ) is not an (r/2, 3/2)-boundary expander.
14

Because G \ set(ρ∗ ) was an (r/2, 3/2)-boundary before setting xi , it follows that after setting it,
G \ (set(ρ∗ ) ∪ {i}) is, at worst, an (r/2, 1/2)-boundary expander. Applying Lemma 5.3 to set(µ) we
get a new collection of coordinates Cl(set(µ)) ⊇ set(µ) such that |Fixed(Cl(set(µ)))| ≤ 2|set(µ)| andG \ Cl(set(µ)) is an (r/2, 3/2) boundary expander. We will now extend µ to µ∗ such that set(µ∗ ) =Cl(set(µ)) and µ∗ satisfies the invariants.
First, for every XOR constraint Ij ∈ Fixed(Cl(set(µ))) ∩ Fixed(set(ρ∗ )), we have that Vars(Ij ) is
contained in both Cl(set(µ)) and set(ρ∗ ), so for every such variable xi we simply assign µ∗i = ρ∗i . Let
I = {I1 , . . . , It } := Fixed(Cl(set(µ))) \ Fixed(set(ρ∗ ))be the set of indices of XOR-constraints whose variables must be updated. Because G \ (set(ρ∗ ) ∪ {i})is an (r/2, 1/2)-boundary expander, by Lemma 5.2 we can find a strong SDR J = {J1 , . . . , Jt } for I.
Therefore, for every variable xj which is in Cl(set(µ)) \ J and which has not yet been assigned, weassign xj arbitrarily in µ∗ . This leaves just the variables in the strong SDR J, which we will assign
according to the Adversary strategy D.
For ` = 1, . . . , t perform the following: Query the Adversary strategy D for the response β ∈{0, 1} when the current state is XORG (µ∗ ) and the Prover is querying the variable yI` (of F ). Observethat because we have already fixed all of the other variables in the neighbourhood of yI` , the only freevariable in the constraint corresponding to yI` is xJ` . Therefore, we fix µ∗J` so thatM

xj = β.

j:(I` ,k)∈E

Doing this for all ` satisfies all constraints by the correctness of the Adversary strategy and, as we havestated before, G \ Cl(set(µ)) = G \ set(µ∗ ) is an (r/2, 3/2)-expander. We can now update ρ = µ andρ∗ = µ∗ , restoring our invariants.
Finally, observe that since |set(µ)| ≤ w by definition of a w-bounded game, it follows by Lemma 5.3
that|Fixed(Cl(set(µ)))| ≤ 2w,
and we can conclude that we query the Adversary strategy at most 2w times during this round. Because
we have played for less than d/2w − 1 rounds, the Adversary has answered at most d − 2w queries sofar. This means that the Adversary can still provide answers to these ≤ 2w queries so that no constraintof F (and thus, F ◦ XORG )) is falsified.

6

Proofs of the Tradeoffs

6.1

Proof of the Resolution Tradeoff

We begin with Theorem 3.1, which we restate next for convenience.
Theorem 3.1. Let F be any CNF formula on N variables and let G = ([N ] ∪ [n], E) be an (r, 2)boundary expander. If Π is a resolution refutation of F ◦ XORG ◦ XORn2 such that log(size(Π) + 1) ≤r/12, thendepthRes (F )depth(Π) log(size(Π) + 1) ≥.
6
We require the following simple size-width lifting theorem for resolution.

15

Lemma 6.1. Let F be any unsatisfiable CNF formula. For any resolution refutation Π∗ of F ◦ XORn2
there is a resolution refutation Π of F such thatwidth(Π) ≤ 3 log(size(Π∗ ) + 1),
depth(Π) ≤ depth(Π∗ ).
Proof. Let x1 , . . . , xn be the variables of F and let u1 , v1 , . . . , un , vn be the variables of F ◦ XORn2 .
Let D be the collection of partial restrictions ρ ∈ {0, 1, ∗} that, for every i ∈ [n], set exactly one of ui
or vi to a value in {0, 1} and leave the other unset. Denote by ρ ∼ D sampling a restriction ρ uniformly
at random from D. It is easy to see that for any resolution refutation Π∗ of F ◦ XORn2 and any ρ∗ ∈ D,Π∗  ρ is a resolution refutation of F , and furthermore by closure under restrictions it follows that
depth(Π∗  ρ) ≤ depth(Π∗ ).
Let t be a positive integer to be set later. For any clause C of width(C) ≥ t in Π∗ , it follows thatfor ρ ∼ D, the probability C  ρ is not satisfied is at most (3/4)t . By a union bound, it follows that theprobability that Π∗  ρ has a clause of width ≥ t is at most size(Π∗ )(3/4)t , which is strictly less than 1
as long as size(Π∗ ) ≤ (4/3)t . Choosing t = log4/3 (size(Π∗ ) + 1) ≤ 3 log(size(Π∗ ) + 1) completes
the proof.
By combining this lemma with the Depth Condensation Theorem, we can prove Theorem 3.1.
Proof of Theorem 3.1. Let Π∗ be a resolution refutation of F ◦ XORG ◦ XORn2 . By Lemma 6.1, there
is a resolution refutation Π of F ◦ XORG with depth(Π) ≤ depth(Π∗ ) andwidth(Π) ≤ 3 log(size(Π∗ ) + 1) ≤ 3r/14 = r/4.
By the Depth Condensation Theorem, it follows that
depth(Π) log(size(Π) + 1) ≥ depthRes (F )/6.

6.2

Proof of the k-DNF Resolution Tradeoff

Next, we establish Theorem 3.2, which we restate next.
Theorem 3.2. Let k ≥ 1 be any constant, let F be any CNF formula on N variables, and let G =([N ] ∪ [n], E) be an (r, 2)-boundary expander. There is a constant δ := δ(k) > 0 such that if Π is aRes(k) refutation of F ◦ XORG ◦ XORn2 with log(size(Π) + 1) ≤ δ · r, then
depth(Π) log2 (size(Π)) = Ω depthRes (F )To do so, we will prove a generic lifting theorem for Res(k). For this, it will not be necessary torecall the specific rules of Res(k), only that every line in a Res(k) proof is a k-DNF formula.
Res(k) Lifting Theorem. Let k ≥ 1 be an integer and F be any CNF formula. For any Res(k)refutation Π∗ of F ◦ XORn2 there is a resolution refutation Π of F such that  4k+1 k k∗width(Π) ≤ k log size(Π ) − log(4k)
,
log e

  4k+1 k k∗∗depth(Π) ≤ k · depth(Π ) log size(Π ) − log(4k)
.
log e
16

This theorem follows in a straightforward way from the switching lemma of Segerlind Buss andImpagliazzo [35], which shows that low-width DNFs can be converted into short decision trees undera random restriction.
Definition 6.2. A decision tree is a rooted binary tree in which every non-leaf node is labelled with avariable, the edges leaving a a node are labelled with 0 and 1, and the leaves are labelled either 0 or
1. Every root-to-leaf path π in a decision tree T can be viewed as a partial assignment π ∈ {0, 1, ∗}n ,where, if the π takes the edge labelled α ∈ {0, 1} at node xi then πi = α. We say that T computes afunction f : {0, 1}n → {0, 1} if for every x ∈ {0, 1}n , the leaf of the unique root-to-leaf path π in T
which agrees with x is labelled with f (x). The decision tree complexity of computing f , DT(f ) is theminimum depth of any decision tree computing f .
For a DNF D over variables {x1 , . . . xn }, let C(D) denote the covering number of D — the minimum size of a set S ⊆ {x1 , . . . xn } such that for every term T of D, S contains at least one variable in
T . The switching lemma is argued by showing that if the size of C(D) is large, then many terms of D
are independent and thus D is set to 1 with high probability, and if C(D) is small then we can build asmall decision tree computing D.
Lemma 6.3 ( [35]). Let s0 , . . . , sk−1 and p1 , . . . , pk be positive numbers and let D set of partial
assignments such that for every i ≤ k and every i-DNF D0 , if C(D0 ) > si−1 then Prρ∼D [D0  ρ 6= 1] ≤pi . Then, for every k-DNF D,
"
#
k−1
k
Pk−1
X
X
Pr DT(D  ρ) >s ≤p · 2( j=i sj ) .
ρ∼D

i

i=0

i

i=1

In the same paper, they showed that Res(k) refutations in which every line can be represented by ashort decision tree can be transformed into a low-width resolution refutation.
Lemma 6.4 ( [35]). Let F be any unsatisfiable CNF formula. If Π is a Res(k) refutation of F such thatfor every line D ∈ Π, DT(D) ≤ t then there is a resolution refutation Π∗ of F withwidth(Π∗ ) ≤ kt,
depth(Π∗ ) ≤ kt · depth(Π).
To prove the Res(k) Lifting Theorem, our strategy will be to show that for any small Res(k) refutation of F ◦ XOR2 there is a restriction such that under this restriction every line in the proof can becomputed by a short decision tree.
Proof of the Res(k) Lifting Theorem. Let F ◦ XORn2 be defined over variables u1 , v1 , . . . , un , vn . Let
D be the set of restrictions ρ ∈ {0, 1, ∗}2n such that for every i ∈ [n], ρ sets exactly one of ui , vi tosome value in {0, 1} and leaves the other unset. Note that for any ρ ∈ D, F ◦ XORn2  ρ = F . Fix
a Res(k) refutation Π of F ◦ XORn2 satisfying the assumption of the lemma. It remains to argue that
there exists a restriction ρ ∈ D such that every line in Π  ρ can be computed by a short decision tree.
Fix any k-DNF D. By the pigeonhole principle, there is a set of at least C(D)/k variable-disjointterms T1 , . . . , TC(D)/k ∈ D. Denote by ρ ∼ D sampling a restriction ρ from D uniformly at random,and observe that the probability that ρ satisfies any term T is at most (1/4)k . Therefore,
Pr [D  ρ 6= 1] ≤ (1 − (1/4)k )C(D)/k ≤ exp(−(1/4)k C(D)/k).

ρ∼D

17

Denote w := (log size(Π) − log(2k))(4k+1 k/ log e)k and let si := (w/2)(log e/4i+1 i)k and pi :=2−4si . Observe that si−1 /4 ≤ si . Therefore,
k−1
X

sj ≤

j=i

and in particular,k−1
Xsi /4j−i ≤ 2si ,

j=i

Pk−1

i=0 si ≤ 2s0 ≤ (w/2) log e ≤ w. For any i-DNF D with C(D) ≥ si−1 , we have

Pr [D  ρ 6= 1] ≤ exp(−(1/4)i C(D)/i) ≤ exp(−si−1 pi /i).

ρ∼D

Therefore, for any k-DNF, it follows from the switching lemma (Lemma 6.3) that
"
#
k−1
k
k
Pk−1
X
X
X
Pr [DT(D) > w] ≤ Pr DT(D) >s ≤p · 2( j=i sj ) ≤k22si (2−4si ) ≤ k2−2sk .
ρ∼D

ρ∼D

i

i=0

i

i=1

i=1

Finally, we can conclude the lemma by taking a union bound over all DNFs in Π,−2skPr [∃D ∈ Π : DT(D  ρ) > w] ≤ size(Π)k2

ρ∼D

−w

= size(Π) · k2



log e
4k+1 kk= 1/2,

where the final equality follows by our setting of w. Thus, there exists some restriction ρ ∈ D suchthat every D ∈ Π  ρ has DT(D) ≤ w. Applying Lemma 6.4 we can conclude that there is a resolution
refutation of width at most kw and depth dkw.
With this lifting theorem in hand, we are ready to prove Theorem 3.2.
Proof of Theorem 3.2. Set δ > 0 such that δ = (4k+1 k/ log e)−k /4k + log(4k)/r. Let Π∗ be any
Res(k) refutation of F ◦ XORn2 with log size(Π∗ ) ≤ δ · r, and denote by t := (log size(Π∗ ) −log(4k))(4k+1 k/ log e)k . By the Res(k) Lifting Theorem, there exists a resolution refutation Π withdepth(Π) ≤ kt · depth(Π∗ ) and k+1 k
4 k
width(Π) ≤ kt ≤ k(δr − log(4k))= r/4.
log e
Applying the Depth Condensation Theorem, we have that
depthRes (F )≤ depth(Π)size(Π) ≤ (kt)2 depth(Π∗ ) = O log2 size(Π∗ )depth(Π) ,2which completes the proof.

6.3

Proof of the Semantic Cutting Planes Tradeoff

Finally, we establish Theorem 3.3.
Theorem 3.3. Let ε > 0 be any constant, let F be any CNF formula on N variables, and let G =([N ] ∪ [n], E) be an (r, 2)-boundary expander. There is a constant δ > 0 such that if Π is a semantic
CP refutation of F ◦ XORG ◦ INDnn1+ε with log(size(Π)) ≤ δ · r log n, thendepth(Π) log2 (size(Π)) = Ω(depthRes (F ) log2 n).
18This theorem follows almost immediately by applying the dag-like lifting theorem of Garg etal. [20], with the improved parameters from [23], and observing that their proof also preserves depth.
We state this theorem next, specialized to semantic Cutting Planes.
Theorem 6.5 ( [20, 23]). Let ε > 0 be any constant and let F be an unsatisfiable CNF formula on nvariables. For any semantic CP Π of F ◦ INDnn1+ε there is a resolution refutation Π∗ of F satisfying

log size(Π)∗
width(Π ) = O
,
log n


depth(Π) log size(Π)∗
depth(Π ) = O.
log n
By combining this lifting theorem with the Depth Condensation Theorem, we can prove Theorem 3.3.
Proof of Theorem 3.3. Let Π be a semantic CP refutation of F ◦ XORG ◦ INDnn1+ε . By Theorem 6.5
there is a semantic Cutting Planes refutation Π∗ of F ◦XORG with depth(Π∗ ) = O(log size(Π)/ log n)
and width(Π∗ ) = α · log size(Π)/ log n for some constant α > 0. Setting δ > 0 so that αδ = 1/4,
width(Π∗ ) =α · log size(Π)≤ αδ · r = r/4.
log n

By the Depth Condensation Theorem, it follows that
depth(Π) log2 size(Π) = Ω depthRes (F ) log2 n .

7Conditional Supercritical Tradeoffs for Monotone Circuits

We end by recording a supercritical size/depth tradeoff for monotone circuits, assuming the following
conjecture which asserts a (quantatively) stronger supercritical size/depth tradeoff for Resolution.
Conjecture 1.4. There are families of unsatisfiable formulas {Fn } with m = m(n) clauses such that
Fn has Resolution refutations of size polynomial in m, but any polynomial-size (or subexponential-size)
refutation of Fn requires depth that is superlinear in m.
Denote by Search(F ) the canonical CNF search problem associated with a CNF formula F . For
any k-CNF formula F with m variables and n clauses, and any gadget g : [D] × {0, 1}D → {0, 1}, itis known that the dag-like communication complexity of Search(F ) ◦ g n is equivalent to the monotone
circuit complexity of computing an associated monotone function mCSP-SATF,g on N = O(mDk )many variables [20, 21]. Garg et al. [20] proved a dag-like lifting theorem, showing that there exists
a gadget g such that from a dag-like communication protocol for Search(F ) ◦ g n , one can extract a
Resolution proof of essentially the same size. We state this lifting theorem next, with the improved
parameters due to Lovett et al. [24].
Theorem 7.1 ([20, 24]). Let F be any unsatisfiable k-CNF formula on n variables and m clauses andlet ε > 0 be any constant. There is a monotone boolean function fF on mnk(1+ε) 2k variables suchthat any monotone circuit C computing fF implies a resolution refutation Π∗ of F satisfyingsize(Π∗ ) = O (size(C)) ,depth(C) log size(C)∗depth(Π ) = O
.
log n
19

Note that Garg et al. [20] state the lifting theorem for Resolution width, rather than size; the statement for size simply follows by the simple observation that there are at most nw+1 distinct clauses ofwidth at most w.
Now, suppose that there is an O(1)-CNF formula F on m clauses such that any polynomial size
Resolution refutation of F requires depth Ω(m4+ε ) for an arbitrarily small constant ε > 0. Then,
applying this lifting theorem we obtain a supercritical size/depth tradeoff for Resolution. We state thisformally for k-CNF formulas next.
Theorem 7.2. Let ε > 0 be an arbitrarily small constant and let F be an unsatisfiable 3-CNF formulawith m clauses on n variables and define N := 8mn3(1+ε) . If any polynomial size Resolution refutationof F requires depth ω(N ), then there is a size/depth supercritical tradeoff for monotone circuits.
Proof. Suppose that any polynomial size Resolution refutation of F requires depth at least d for d =ω(N ). Applying Theorem 7.1 completes the proof.
Note that the assumption that F is a 3-CNF formula is essentially without loss of generality. Indeed,
if F is a k-CNF formula on m clauses and n variables, then by introducing additional “extension”
variables, we can transform it into an equivalent 3-CNF formula as follows: for each k-clause C =`1 ∨ . . . ∨ `k with k > 3, introduce k − 1 new variables y1 , . . . , yk−1 , and replace C by the following
k-clausesy1 ∨ `1 , ¬y1 ∨ `2 ∨ y2 , . . . , ¬`k−1 ∨ `k .
The resulting CNF formula has at most n + mk variables and at most mk clauses. Finally, observe thatthe original CNF formula can be derived from the extended formula in size at most O(mk) and depthlog(k) by simply resolving on the y-variables. Thus, for k-CNF formulas we obtain Theorem 7.2 with
N = O(mk(n + mk)3(1+ε) ).
Finally, note that a lifting theorems for a constant-size gadget would allow us to obtain supercriticalsize/depth tradeoffs for monotone circuits from supercritical tradeoffs for Resolution that are barely
superlinear in m (in constrast with the Ω(m4 ) required by the current lifting theorem). We state thisnext.
Observation 7.3. Let F be any unsatisfiable k-CNF formula on n variables and m clauses and let
g : [D] × {0, 1}D → {0, 1} be any function such that any dag-like communication protocol for
Search(F ) ◦ g n implies a Resolution refutation Π∗ of F satisfyingsize(Π∗ ) = poly(size(C)),
depth(C) log size(C)∗depth(Π ) = O.
log n
If any polynomial size Resolution refutation of F requires depth at least ω(mDk ) then there is a supercritical size/depth tradeoff for monotone circuits.
Proof. Recall from the beginning of this section that a dag-like communication protocol for solving
Search(F ) ◦ g n is equivalent to a monotone circuit computing the monotone function mCSP-SATF,gon N = O(mDk ) many variables. By the assumption that any polynomial-size Resolution refutationof F requires depth ω(mDk ), and the assumed lifting theorem, we obtain a supercritical size/depth
tradeoff for monotone circuits.

20

References[1] Karen Aardal, Robert E. Bixby, Cor A. J. Hurkens, Arjen K. Lenstra, and Job W. Smeltink. Market
split and basis reduction: Towards a solution of the cornuéjols-dawande instances. INFORMS J.
Comput., 12(3):192–202, 2000.
[2] Michael Alekhnovich. Lower bounds for k-DNF resolution on random 3-CNFs. In Harold N.
Gabow and Ronald Fagin, editors, Proceedings of the 37th Annual ACM Symposium on Theory ofComputing, Baltimore, MD, USA, May 22-24, 2005, pages 251–256. ACM, 2005.
[3] Albert Atserias and Vı́ctor Dalmau. A combinatorial characterization of resolution width. J.
Comput. Syst. Sci., 74(3):323–334, 2008.
[4] Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space trade-offs in resolution: Superpolynomial lower bounds for superlinear space. SIAM J. Comput., 45(4):1612–1645, 2016.
[5] Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In 9th Innovations in Theoretical Computer
Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, pages 10:1–10:20,
2018.
[6] Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC’13, Palo Alto, CA, USA, June 1-4, 2013, pages
813–822. ACM, 2013.
[7] Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM,
48(2):149–169, 2001.
[8] Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October
20-23, 2012, pages 351–360. IEEE Computer Society, 2012.
[9] Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution.
SIAM J. Comput., 49(1):98–118, 2020.
[10] 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.
[11] Siu Man Chan. Just a pebble game. In Proceedings of the 28th Conference on Computational
Complexity, CCC 2013, K.lo Alto, California, USA, 5-7 June, 2013, pages 133–143. IEEE Computer Society, 2013.
[12] Vašek Chvátal, William Cook, and Mark Hartmann. On cutting-plane proofs in combinatorial
optimization. Linear algebra and its applications, 114:455–499, 1989.
[13] 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, Saarbrücken,
Germany (Virtual Conference), volume 169 of LIPIcs, pages 34:1–34:35. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2020.
21

[14] Susanna F. de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc
Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In 61stIEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA,
November 16-19, 2020, pages 24–30. IEEE, 2020.
[15] Friedrich Eisenbrand and Andreas S. Schulz. Bounds on the chvátal rank of polytopes in the
0/1-cube. In Gérard Cornuéjols, Rainer E. Burkard, and Gerhard J. Woeginger, editors, Integer
Programming and Combinatorial Optimization, 7th International IPCO Conference, Graz, Austria, June 9-11, 1999, Proceedings, volume 1610 of Lecture Notes in Computer Science, pages
137–150. Springer, 1999.
[16] Juan Luis Esteban and Jacobo Torán. A combinatorial characterization of treelike resolution
space. Inf. Process. Lett., 87(6):295–300, 2003.
[17] Yuval Filmus, Pavel Hrubeš, and Massimo Lauria. Semantic versus syntactic cutting planes.
In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium on Theoretical Aspects ofComputer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs,
pages 35:1–35:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
[18] Noah Fleming, Mika Göö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 - LeibnizZentrum für Informatik, 2021.
[19] Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are
hard for cutting planes. In 58th IEEE Annual Symposium on Foundations of Computer Science,
FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109–120, 2017.
[20] Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds
from resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los
Angeles, CA, USA, June 25-29, 2018, pages 902–911. ACM, 2018.
[21] Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM
J. Comput., 47(5):1778–1806, 2018.
[22] Pavel Hrubeš and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In 58th
IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA,
October 15-17, 2017, pages 121–131, 2017.
[23] Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. unpublished.
[24] Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. In Electron. Colloquium Comput. Complex, page 111, 2020.
[25] Theodoros Papamakarios and Alexander A. Razborov. Space characterizations of complexity
measures and size-space trade-offs in propositional proof systems. Electron. Colloquium Comput.
Complex., 28:74, 2021.
22

[26] Wolfgang J. Paul, Robert Endre Tarjan, and James R. Celoni. Space bounds for a game on graphs.
Math. Syst. Theory, 10:239–251, 1977.
[27] Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations.
J. Symb. Log., 62(3):981–998, 1997.
[28] Pavel Pudlák. Proofs as games. Am. Math. Mon., 107(6):541–550, 2000.
[29] Ran Raz and Avi Wigderson. Monotone circuits for matching require linear depth. J. ACM,
39(3):736–744, 1992.
[30] Alexander A. Razborov. Lower bounds on monotone complexity of the logical permanent. Mathematical Notes of the Academy of Sciences of the USSR, 37(6):485–493, 1985.
[31] Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM,
63(2):16:1–16:14, 2016.
[32] Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Math. Oper. Res.,
42(4):1106–1134, 2017.
[33] Alexander A. Razborov. On space and depth in resolution. Comput. Complex., 27(3):511–559,
2018.
[34] Thomas Rothvoß and Laura Sanita. 0/1 polytopes with quadratic chvátal rank. In International
Conference on Integer Programming and Combinatorial Optimization, pages 349–361. Springer,
2013.
[35] Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM J. Comput., 33(5):1171–1200, 2004.

23