On Semi-Algebraic Proofs and Algorithms
Noah Fleming†

Mika Göös

Stefan Grosser

UCSD
Memorial University

EPFL

McGill University

Robert Robere†
McGill University

January 19, 2022
Abstract
We give a new characterization of the Sherali-Adams proof system, showing that there is adegree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there isan ε > 0 and a degree-d conical junta J such that violC (x) − ε = J, where violC (x) counts
the number of falsified clauses of C on an input x. Using this result we show that the linear
separation complexity, a complexity measure recently studied by Hrubeš (and independently
by de Oliveira Oliveira and Pudlák under the name of weak monotone linear programming
gates), monotone feasibly interpolates Sherali-Adams proofs.
We then investigate separation results for violC (x) − ε. In particular, we give a family of
unsatisfiable CNF formulas C which have polynomial-size and small-width resolution proofs,
but for which any representation of violC (x) − 1 by a conical junta requires degree Ω(n); thisresolves an open question of Filmus, Mahajan, Sood, and Vinyals. Since Sherali-Adams cansimulate resolution, this separates the non-negative degree of violC (x) − 1 and violC (x) − ε
for arbitrarily small ε > 0. Finally, by applying lifting theorems, we translate this lower boundinto new separation results between extension complexity and monotone circuit complexity.

†

Research supported by NSERC.

1

Introduction

The Sherali-Adams hierarchy is a well-studied method in optimization that provides an automatic way
to convert a linear program with “weak” approximation guarantees into a linear program with “strong”
approximation guarantees. Each “level” of the Sherali-Adams hierarchy is defined by systematicallyadding new variables and inequalities to the original linear program — “lifting” it to a higher dimensional space — and then “projecting” it back down to a polytope contained within the original linearn
program. The Sherali-Adams hierarchy at level r results in a linear program with roughly ≤r
constraints and variables, and it is known that at level n the hierarchy converges to the integral hull of thestarting polytope. Owing to its strength and its generality, much work has been spent on understanding
the strength of the Sherali-Adams hierarchy and its subsystems when applied to NP-Hard optimization
problems [1, 6, 15, 19, 38, 44, 46, 47, 50, 57], as well as its strength when it is treated as a refutation
system in propositional proof complexity [2, 5, 7, 18, 21, 34, 36].
A powerful generalization of the Sherali-Adams hierarchy is the notion of an extended formulation,
which was originally formulated by Yannakakis [59] and extended by Braun et al. [9] to nested pairsof polytopes. Given a pair of polytopes P ⊆ Q ⊆ Rn , an extended formulation of the pair (P, Q) is
a polytope K ⊆ Rm with m ≥ n along with a projection π such that P ⊆ π(K) ⊆ Q. Indeed, theSherali-Adams hierarchy gives many examples of extended formulations: if we are given some linear
program Q ⊆ [0, 1]n which gives a “weak” approximation guarantee to any point in the integral hullint(Q) := conv {x ∈ Zn | x ∈ Q} ,then each level of the Sherali-Adams hierarchy produces an extended formulation (K, π) such thatint(Q) ⊆ π(K) ⊆ Q.
We regard this as giving a “tighter” relaxation to the integral hull, when compared to the starting
polytope Q (indeed, at n-th level of the hierarchy it turns out that π(K) = int(Q)).
More generally, for some polytopes P ⊆ Rn with exponentially many facets, it turns out to be possible to find an extended formulation K ⊆ Rm such that π(K) = P but m = poly(n) and K has only
polynomially many facets [59] (this is certainly a boon if P = int(Q) for some combinatorial optimization problem encoded by Q!). Given a polytope pair P ⊆ Q we therefore let xc(P, Q) denote the size(= number of facets) of the smallest extended formulation for the pair P, Q. After a breakthrough result
by Fiorini et. al. [25], strong lower bounds have been shown for the extension complexity of polytopes
associated with many standard NP-Hard optimization problems [9–11, 14, 25, 31, 43, 55, 56, 59]. All ofthese lower bound results crucially rely on the close relationship between the number of facets in any
extended formulation and the non-negative rank of a certain related matrix [9, 59].
Theorem 1.1 (Factorization Theorem). Let P ⊆ Q ⊆ Rn be polyhedral sets, let v1 , . . . , vn be thevertices of P and let a1 · x ≤ b1 , . . . , am · x ≤ bm be linear inequalities in Rn describing the facetsof Q. The size of the smallest extended formulation of (P, Q) is rank+ (SP,Q ) ± 1 where SP,Q is then × m matrix defined by SP,Q (i, j) = bj − aj · vi .
Indeed, works of Chan et. al. [14] , Göös et. al. [33], and Kothari, Raghavendra, and Steurer [43]have shown that for certain NP-Hard optimization problems, lower bounds on the size of arbitrary
extended formulations follow immediately from lower bounds on the Sherali-Adams hierarchy. These
results join a long line of lifting theorems in communication, proof, and circuit complexity [16, 17,
22, 23, 26, 29, 30, 32, 35, 51, 53, 58] which systematically relate the complexity of computations in“complicated” computational models with complexity in “simple” computational models.
11.1

Sherali-Adams as Proofs and Extended Formulations as Circuits

In this work we further the study of the Sherali-Adams hierarchy and its relationship with extended
formulations, but approach it from a different point of view. In particular, we are interested in the “dualview” of Sherali-Adams as a propositional proof system (first considered in [18]), and in extended
formulations as a device for computing boolean functions. Before we formally state our results, let us
first describe these two perspectives.
A conical junta J is a non-negative linear combination of conjunctions over a set of {0, 1}-valued
variables. Given an unsatisfiable CNF formula C = C1 ∧ C2 ∧ · · · ∧ Cm , a Sherali-Adams refutation*of C is given by a list of m + 1 conical juntas J1 , . . . , Jm+1 such thatm
X

−C i Ji + Jm+1 = −1

i=1

where all operations are done in multilinear polynomial arithmetic (so, x2 = x) over R and C i is thenegation of the clause Ci . Indeed, if such a list of conical juntas exists then the original CNF formula
must indeed be unsatisfiable, as if x was a satisfying assignment then C i (x) = 0 for all Ci and theabove expression would reduce to −1 = Jm+1 (x) ≥ 0, a contradiction. In this way, Sherali-Adams isnaturally viewed as a proof system for refuting unsatisfiable formulas, and we can discuss complexity
measures of its proofs such as the degree (i.e. the maximum degree of any product C i Ji as a multilinear
polynomial) and its size† (the number of distinct monomials occurring in the proof after expanding all
products and before cancellations).
It is also quite natural to study extended formulations as non-uniform computation devices forboolean functions. The next definition was formally introduced by Hrubeš [40].
Definition 1.2. A separating polytope for f : {0, 1}n → {0, 1, ∗} is a polytope P ∈ Rn such thatconv f −1 (1) ⊆ P and P ∩ f −1 (0) = ∅. We say a polyhedron P ⊆ Rn is monotone if x ∈ P ⇒ y ∈ P
whenever x ≤ y, and if P ⊆ Rn we let P ∗ := {y ∈ Rn : ∃x ∈ P : x ≤ y} ⊇ P be the monotone
closure of P . A monotone separating polytope for f is a polytope P such that P ∗ is a separating
polytope for f .
Observe that if we have such a separating polytope K, then when given x ∈ {0, 1}n we can test
if f (x) = 1 simply by testing if x ∈ K. One natural way to construct such separating polytope is
as follows, and was introduced by Hrubeš [39] and studied independently by Göös, Jain and Watson[31]. Given a boolean function f : {0, 1}n → {0, 1} define the polytope Qf,1 by the |f −1 (0)| linear
inequalitiesnX∀y ∈ f −1 (0) :xi (1 − yi ) + (1 − xi )yi ≥ 1
i=1

P

where we note that i xi (1 − yi ) + (1 − xi )yi =: h(x, y) is exactly the hamming distance between
two {0, 1}-valued vectors x, y. It is easy to see that x ∈ Qf,1 for every x ∈ f −1 (1) since x must differ
from every y ∈ f −1 (0) on some coordinate; similarly, for any y ∈ f −1 (0) we have that y 6∈ Qf,1 as thehamming distance from y to itself is 0. It therefore follows that any extended formulation of the pair(conv f −1 (1), Qf,1 ) yields a separating polytope as we described above. One can further specialize* This encoding of Sherali-Adams is slightly different from the “usual” definition of Sherali-Adams as a refutation systemof linear inequalities or polynomial equations, but is easily seen to be equivalent (cf. Claim 3.32 in [27])†This measure is sometimes called the monomial size in other works on the Sherali-Adams hierarchy to differentiate fromthe bit-length of the encoding of the proof. As this is the natural notion of size for our purposes we simply call it size.

2

P


conv f −1 (1)f −1 (0)Figure 1: A monotone separating polytope.
this construction when the function f : {0, 1}n → {0, 1} is monotone (recall f is monotone if x ≤ y⇒f (x) ≤ f (y), where the first inequality is interpreted coordinate-wise). In this case, we can simplify
the description of Qf,1 and still obtain a separating polytope. Specifically, if f is monotone then define
the polytope Q+
f,1 by the linear inequalities∀y ∈ f −1 (0) :nXxi (1 − yi ) ≥ 1.

i=1

The fact that an extended formulation of (conv f −1 (1), Q+f,1 ) is a separating polytope (indeed, now
we can even have a monotone separating polytopes) for monotone f follows by a similar argument as
before, but uses the additional fact that for monotone functions, f (x) = 1 and f (y) = 0 if and only ifthere is a coordinate i such that xi = 1, yi = 0. We depict such a pair in Figure 1.
By using the Factorization Theorem (Theorem 1.1), we can relate the size of these extended formulations to the non-negative ranks of P
certain matrices. Namely, given f : {0, 1}n → {0, 1} define thef −1 (1) × f −1(0) matrix Sf (x, y) := ni=1 xi (1 − yi ) + (1 − xi )yi , and its “monotone” counterpart
P
Sf+ (x, y) := ni=1 xi (1 − yi ). Define the separation complexity quantities
sep1 (f ) := rank+ (Sf − 1),

msep1 (f ) := rank+ (Sf+ − 1)

where 1 represents the all-1s matrix of the appropriate complexity. By Theorem 1.1, these two quantities capture the size of the smallest extended formulations for the pairs (conv f −1 (1), Qf,1 ) and(conv f −1 (1), Q+f,1 ), respectively.
Now, it is natural to ask: are these interesting complexity measures of boolean computation?
Hrubeš [39] and Göös, Jain and Watson [31] showed that the answer is yes: both of these quantities
yield lower bounds on the formula complexity of computing f !
Theorem 1.3. For any boolean function f : {0, 1}n → {0, 1}, we have sep1 (f ) = O(n · F(f ))where F(f ) is the size of the smallest boolean formula computing f . Furthermore, if f is monotone,
then msep1 (f ) = O(n · mF(f )) where mF(f ) is the size of the smallest monotone boolean formulacomputing f .
3

f −1 (0)Qf,1conv f −1 (1)f −1 (0)conv f −1 (1)Qf,εFigure 2: The left depicts the polytope pair conv f −1 (1) and Qf,1 ; the right depicts conv f −1 (1) andQf,ε for some ε < 1. By setting ε < 1 it is potentially easier to project a relatively low-facet polytope
separating the 0s from the 1s of f .
Furthermore, observe the following. If our goal is just to separate the 1s of f from the 0s of f bymeans of a polytope we can weaken the inequalitiesnX

xi (1 − yi ) + (1 − xi )yi ≥ 1, ∀y ∈ f −1 (0).

i=1Since x ∈ f −1 (1) and y ∈ f −1 (0) are boolean strings, by integrality it suffices to have the inequalities∀y ∈ f −1 (0) :nXxi (1 − yi ) + (1 − xi )yi ≥ ε

i=1

for any ε > 0 (note we must have ε > 0, since if ε = 0 then y ∈ f −1 (0) will occur inside of thepolytope). With this in mind, define the quantities
sep(f ) := min rank+ (Sf − ε1),ε>0msep(f ) := min rank+ (Sf+ − ε1),
ε>0which generalize sep1 (f ) and msep1 (f ) in the natural way. These quantities were recently studied by
Hrubeš [40], where it was shown that they lower bound the size of boolean circuits computing f .
Theorem 1.4. For any boolean function f : {0, 1}n → {0, 1} we have sep(f ) = O(C(f ) + n),
where C(f ) is the size of the smallest boolean circuit computing f . Furthermore, if f is monotone,
then msep(f ) = O(mC(f ) + n), where mC(f ) is the size of the smallest monotone boolean circuit
computing f .
We also note that the quantity msep(f ) was independently studied by Pudlák and de Oliveira
Oliveira, where it was captured by a model of computation they called weak monotone linear programming gates [20].

4To summarize: the Sherali-Adams hierarchy can be interpreted both as a particular family of extended formulations in optimization, and also as a natural family of proof systems for refuting unsatisfiable formulas. If we consider extended formulations more generally, then it is natural to interpretthem as a computational devices whose complexities are related to standard boolean circuit and formulamodels. In this way, the known “lifting theorems” from Sherali-Adams proofs to extended formulations
fall naturally in line with other proof-to-circuit lifting theorems [22, 29, 53], as we will show next.

1.2

Our Results

Normal Form for Sherali-Adams. In this work, we systematically relate the complexity of SheraliAdams proofs and its fragments with the linear separation quantities sep1 (f ), msep1 (f ), sep(f ), andmsep(f ). Our first main result is the following novelP“normal form” for Sherali-Adams proofs. Given a
CNF formula F = C1 ∧C2 ∧· · ·∧Cm let violC (x) = m
i=1 C i (x) denote the number of falsified clauses
on an input x. Furthermore, if f : {0, 1}n → R≥0 is a non-negative real-valued boolean function thenlet deg+ (f ) denote the minimum degree of a conical junta J such that f = J .
Theorem 1.5. For any unsatisfiable CNF formula C, if there is a Sherali-Adams refutation of C with
degree d and size s, then there is an ε > 0 and a degree d, size s2d conical junta J such that
violC − ε = J .
Consequently, if SA(C) is the minimum degree of any Sherali-Adams refutation of C, then
SA(C) = min deg+ (violC − ε).
ε>0Several remarks on this theorem are in order. First, although we have stated this theorem for
CNF formulas, a similar result immediately follows for arbitrary boolean CSPs. This is because if
P : {0, 1}k → {0, 1} is an arbitrary boolean
CSP then we can represent P as a width-k unique DNF
P
of its 1-inputs. This means that ¬P = i Di for some conjunctions Di (specifically, conjunctions thatrecognize the 0s of P ). By substituting these sums for the predicates we can immediately deduce amore general theorem for refuting arbitrary boolean CSPs.
Second, if there is a conical junta J such that violC − ε = J then note that we immediately obtaina Sherali-Adams refutation by rearranging the expression:
m
X
i=1

−

Ci J
+
= −1.
ε
ε

Thus this truly is a normal form that preserves the degree and the size (although, the size is only
preserved up to a 2d factor).
Third, one should note the similarities between Theorem 1.5 and the definitions of sep(f ) andmsep(f ) — they are identical up to the substitution of “deg+ ” for “rank+ ” and “violC ” for “Sf /Sf+ ”.
Looking forward, this similarity turns out to be quite important for the rest of our results.
Finally, we remark that the fragment of Sherali-Adams corresponding to deg+ (violC − 1) has also
been studied in the literature as an object of interest. Göös, Jain and Watson studied it under thename of the “∃ − 1 Game”, in which they proved degree lower bounds for Tseitin formulas [31].
Filmus, Mahajan, Sood, and Vinyals studied a further restriction in which the coefficients are required
to be integers; they showed that this restriction was closely related to the complexity of MaxSAT
resolution [24].
5Feasible Interpolation for Sherali-Adams. Next, inspired by the normal-form theorem, we further
develop the connection between Sherali-Adams and separation complexity by way of monotone feasible interpolation.
The feasible interpolation method relates the complexity of proofs to the complexity of computational models. Suppose we are given an unsatisfiable CNF formula of the form A(x, z)∧B(y, z). Then,
under an assignment z 7→ α, at least one of the formulas A(x, α), B(y, α) is unsatisfiable. Thus, we
can associate with A ∧ B a partial function I : {0, 1}z → {0, 1}, known as an interpolant, satisfying(
0 if A(x, α) is satisfiable
I(α) =
1 if B(y, α) is satisfiable
In its original form, introduced at this level of generality in the classic work of Krajiček [45], we saythat a proof system P has feasible interpolation if we can extract a small computation of the interpolant
I in some computational model from any small P -proof of A ∧ B. Furthermore, if A ∧ B satisfies acertain monotonicity property, namely that all z-literals occur only negatively in A, then the interpolant
function I is monotone and we say that P has monotone feasible interpolation if we can extract froma P -proof of A ∧ B a computation in some monotone computational model. Instantiations of themethod of (monotone) feasible interpolation have led to a number of important lower bounds in proof
complexity. Razborov [52] showed that from proofs in certain fragments of bounded arithmetic one
could extract Boolean circuits and used this to establish conditional unprovability of P 6= NP in thesesystems. The first lower bounds for Cutting Planes were established by Pudlák [48], who showedthat proofs in this system gave rise to monotone real circuits; this built upon earlier work by Bonet,
Pitassi and Raz [8] who showed that low-weight Cutting Planes gave rise to monotone circuits. Pudlákshowed that span programs monotone feasibly interpolate Nullstellensatz [49], and de Oliveira Olivera
and Pudlák showed that proofs in the Lovász-Schijver system convert to monotone linear programming
circuits [20].
Recently, Hrubeš and Pudlák [41] and Fleming et al. [28] showed that the method of monotone
feasible interpolation could be generalized to work for arbitrary unsatisfiable CNF formulas, not only
for split formulas. They showed that from a small Cutting Planes proof of an unsatisfiable CNF formula
C one could extract small monotone circuit computing an associated monotone function, termed theunsatisfiability certificate by Hrubeš and Pudlák [41]. (Fleming et. al. used a conceptually different,
though ultimately equivalent, function [28]). If C is a clause and X is a subset of its variables we let
C X denote the subclause of C containing only literals over X.
Definition 1.6. Let C = C1 ∧ · · · ∧ Cm be an unsatisfiable CNF formula and let (X, Y ) be any partitionof its variables. The unsatisfiability certificate associated with C and (X, Y ) is the partial function(X,Y )certC: {0, 1}m → {0, 1, ∗} defined as(
0 if {CiX : Ci ∈ C, αi = 1} is satisfiable,(X,Y )
certC(α) =1 if {CiY : Ci ∈ C, αi = 0} is satisfiable,
When it is clear from context, we may suppress the partition (X, Y ) or the underlying CNF formula C.
Our second main result is the following monotone feasible interpolation theorem for Sherali-Adams
proofs‡ .
‡A similar feasible interpolation result can be proved for Sum-of-Squares proofs; we follow up on this in an upcoming
work.

6

Theorem 1.7. Let C = C1 ∧C2 ∧· · ·∧Cm be any unsatisfiable CNF formula. If there is a Sherali-Adams
proof of C with size s then for any partition (X, Y ) of the variables of C we have msep(certC ) = O(s2 ).
Several remarks on this theorem are in order. First, as was shown by Pudlák and Hrubeš [41] astandard interpolation theorem for split formulas follows from this interpolation (simply by “resolving
away” the z variables and taking the natural partition of variables). Second, prior to this result there wasno monotone feasible interpolation theorem known for Sherali-Adams. A recent work of Hakoniemi
gave the first feasible interpolation theorem for Sherali-Adams [37], but, his feasible interpolation result
only applied to the “standard” split formulas A(x, z) ∧ B(y, z) and it only gave a small non-monotone
Boolean circuit for the interpolant [37]. Finally, as we have remarked before, the model msep(f ) was
recently studied by de Oliveira Olivera and Pudlák under the name weak monotone linear programming
gates [20]. They also introduced a model that they called strong monotone linear programming gates,and showed that “circuits” created out of strong monotone linear programming gates can monotone
feasibly interpolate Lovász-Schrijver proofs. Pudlák and de Oliveira Olivera left as an open problem
whether or not strong monotone linear programming gates can be efficiently simulated by weak monotone linear programming gates. We believe our feasible interpolation result makes this question moreinteresting, in light of the lack of separations between Lovász-Schrijver and Sherali-Adams proofs —the only separation known is due to Atserias and Ochremiak [3] , who showed that degree-6 LovászSchrijver has polynomial-size refutations of Tseitin principles (and, furthermore, there are no good size
lower bounds on Lovász-Schrijver proofs at all!).
Separation Results. Finally, we prove new separation results between the proof and circuit models
described above. In particular, we are interested in the value of ε > 0 that is required in the definitionof msep(f ) := minε>0 rank+ (Sf+ − ε1) and in our new characterization of Sherali-Adams degreeminε>0 deg+ (violC − ε). For instance: is it possible that we never need to take ε < 1? Or, in otherwords, is it possible that msep(f ) = msep1 (f ), and that Sherali-Adams is already captured by theconical junta degree of violC − 1?
We give a negative answer to these questions. First, we show that if C is a pebbling formula, then+deg (violC − 1) must be large. (In fact, our lower bound already holds for deg+ (violP EBG − 0.99).)
Theorem 1.8. There is a constant δ > 0 such that for all sufficiently large m there is an in-degree-2
DAG G on m vertices such thatdeg+ (violP EBG − 1) = mδ ,where P EBG is the pebbling formula associated with G.
Pebbling formulas are well-known to be refutable in Resolution width O(1) and linear size ongraphs of constant in-degree, and thus our result separates deg+ (violC − 1) from Resolution, resolving an open problem asked by Filmus, Mahajan, Sood and Vinyals [24]. Since Sherali-Adams canefficiently simulate Resolution [18], it follows from combining the previous theorem and Theorem 1.5
that deg+ (violC − 1) can be much larger than deg+ (violC − ε) for arbitrarily small ε > 0 (although,we note that the standard simulation of Resolution by Sherali-Adams results in ε that is exponentiallysmall in the size of the proof!).
Next, by using known lifting theorems from conical junta degree to non-negative rank [33, 43], we
can lift the lower bound in the previous theorem to the following separation between msep1 (G ENn )and mC(G ENn ), where G ENn is the Generation function.
Theorem 1.9. The G ENn function is computable by polynomial-size monotone circuits, but, there is aδ
δ > 0 such that msep1 (G ENn ) = 2Ω(n ) .
7

mF(f )

mC(f )

msep1 (f ) = rank+ (Sf+ − 1)

msep(f ) = rank+ (Sf+ − ε1)

Circuit Classes

Feasible Interpolation
deg+ (violC − 1)

SA(C) = deg+ (violC − ε)Proof Systems
Res

Figure 3: Semialgebraic circuit classes and proof systems considered in this paper. Solid arrows represent simulation results, while dashed red arrows represent new separations.
Since msep(f ) ≤ mC(f ), this provides the analogous separation between msep1 (f ) and msep(f )(and, indeed, already between msep1 (f ) and monotone circuit size). Taken together, these results imply
that choosing smaller ε actually does increase the power of the corresponding proof systems and circuit
models.

1.3

Paper Outline

The rest of this paper is outlined as follows. In Section 2 we carefully outline all important proof
systems and non-uniform models of computation that we consider. In Section 3 we prove our new
characterization of Sherali-Adams proofs, as well as our feasible interpolation results. In Section 4 weprove our new separations between fragments of Sherali-Adams and between separation complexities.

2

Preliminaries

2.1

Proof Systems

We recall some preliminaries from proof complexity. A clause C is a disjunction of boolean literals;
the width of a clause, denoted w(C), is the number of literals in C. If C = C1 ∧ C2 ∧ · · · ∧ Cm is a
CNF formula then the width of C is the largest width of any clause in C.
Resolution Proofs. Fix an unsatisfiable CNF formula C over variables x1 , . . . , xn . A Resolution
refutation of C is a sequence of clauses D1 , . . . , Ds ending in the empty clause Ds = ∅ such that foreach i ∈ [s], either Di is in C or is derived from earlier clauses Dj , Dk with j, k < i using the resolutionruleC ∨ `, D ∨ ` ` C ∨ D
where the rule can only be applied if C and D do not contain literals of opposite sign. The size of theresolution proof is s, the number of clauses, and the width of the proof is the largest width of any clause8

in the proof. Let SRes (C) denote the minimum size of any resolution refutation of C, and let wRes (C)denote the smallest width of any resolution refutation of C.
Sherali-Adams and Conical Junta Degree. In this paper we will regularly be doing arithmetic withreal polynomials that represent boolean functions f : {0, 1}n → R. It is well known that each suchfunction can be represented (uniquely) by multilinear polynomials (that is, the largest degree of any
individual variable is 1). We will exclusively be operating using multilinear arithmetic with thesepolynomials — for example, we regard x2i and xi as representing the same boolean function. Formally,
we work modulo the ideal hx2i − xi ini=1 .
A d-conjunction J is a conjunction of d boolean literals. We will usually encode conjunctions aspolynomials over the reals, and so if S, T ⊆ [n] are subsets such that S ∩ T = ∅ then we let
Y Y
JS,T (x) :=xi(1 − xj )i∈Sj∈Tbe the conjunction that tests if all variables in S are 1 and all variables in T are 0. Similarly, if C is aand only if C(x) = 0 — that is, Cclause, we will let C denote the conjunction such that C(x)W = 1 if W
tests if the clause C is falsified. To spell it out, if C = j∈T xj ∨ i∈S xi then C = JS,T . Note thatthe empty conjunction J∅,∅ = 1.
P
A conical junta is any non-negative real combinations of conjunctions J = i λi Ji , where λi ≥ 0
is a real constant and Ji is a conjunction. The degree of a conical junta is the maximum degree ofany conjunction in the conical junta representation, and the size of a conical junta is the number ofmonomials obtained after expanding all juntas but before cancellation. If f : {0, 1}n → R≥0 is a nonnegative real boolean function, then the conical junta degree of f , denoted deg+ (f ), is the minimum
integer d such that we can write
X
f=
λi Ji
i

where λi ≥ 0 is a non-negative real constant and Ji is a ≤ d-conjunction for each i. Note that, unlike
polynomial degree, the representation of f as a conical junta is not necessarily unique.
A Sherali-Adams refutation of an unsatisfiable CNF formula C = C1 ∧ · · · ∧ Cm is given by asequence of conical juntas J1 , J2 , . . . , Jm , Jm+1 such thatm
X

−C i Ji + Jm+1 = −1.

i=1The degree of the proof is the maximum degree of any of the polynomials −C i pi , J before cancellation. The size of the proof is the number of distinct monomials that occurs in the proof (after expanding
all polynomials and before cancellation). Let SA(C) denote the minimum degree of any Sherali-Adams
refutation of C. We note that CNF formulas are often encoded as linear inequalities rather than juntas;
this is equivalent to the above definition up to increasing the degree by an additive factor of w(C) (seee.g., [27, Claim 3.32]). If C = C1 ∧ C2 ∧ · · · ∧ Cm is a CNF formula then define violC : {0, 1}n → R≥0bymX
Ci (x).
violC (x) :=i=1

That is, violC (x) counts the number of falsified clauses of C on input x. It follows that C is unsatisfiable
if and only if violC (x) ≥ 1 for all x ∈ {0, 1}n — indeed, if and only if violC (x) ≥ ε for any ε > 0.
Thus, a conical junta representation of violC − ε for any ε > 0 constitutes a proof that C is unsatisfiable.
9In fact, conical junta representations of violC − ε correspond naturally to fragments of SheraliAdams proofs. This is easy to see: suppose that violC − ε = J where J is a conical junta. Explicitly,
this means thatm
X
−C j + J = −ε
j=1which, dividing by ε, yields

m
X
j=1

1
J
− Cj += −1.
εεConversely, suppose that we have a Sherali-Adams refutation of C of the formmX

−αj C j + J = −1

j=1

where 0 ≤ αj ≤ 1/ε for all j. Since C j is a conjunction and 1/ε ≥ αj , this means that
m
X
j=1

m

X
1
− Cj + J +
ε



j=1


1
− αj C j = −1εis also a Sherali-Adams refutation of C. Multiplying through by ε yields the following:
Lemma 2.1. Let C = C1 ∧ C2 ∧ · · · ∧ Cm be an unsatisfiable CNF formula. If there is a Sherali-Adams
refutation of the formmX
−αj C j + J = −1
j=1

where J is a conical junta of degree d and size s and with 0 ≤ αj ≤ 1/ε for each αj , then there is adegree-max {d, w(C)} conical junta J 0 such that violC − ε = J 0 .
Conversely, if violC − ε = J 0 for some degree-d, size s conical junta J 0 , then there is a SheraliAdams proof of the above form with αj ≤ 1/ε and where J = J 0 .
As we will show in Section 3.1, it turns out that this fragment of Sherali-Adams is actually complete,in the sense that any Sherali-Adams proof can be put into this form without changing the degree andwithout (badly) changing the size.

2.2

Circuit Complexity and Extended Formulations.

Boolean Circuit Complexity. A partial boolean function is a function f : {0, 1}n → {0, 1, ∗} (the∗ represents that we “don’t care” what the function’s output is). Given two partial boolean functions
f, g we say that g extends f if for all x such that f (x) 6= ∗, g(x) = f (x). A (total) boolean function
f : {0, 1}n → {0, 1} is monotone if x ≤ y ⇒ f (x) ≤ f (y) (where the first inequality is taken
coordinate-wise); a partial boolean function f : {0, 1}n → {0, 1, ∗} is monotone if there is a total
monotone boolean function g extending f .
We assume familiarity with standard boolean circuit models in complexity theory — e.g. boolean
formulas, boolean circuits, etc. All circuits considered in this paper will be composed of AND (∧)
and OR (∨) gates, and will be De-Morgan in the sense that if any negations appear they appear at the
inputs of the circuit. A boolean circuit is monotone if it does not contain any negation gates. We say
10that a circuit C computes a partial function f : {0, 1}n → {0, 1, ∗} if f (x) = 1 ⇒ C(x) = 1 andf (x) = 0 ⇒ C(x) = 0 for all x ∈ {0, 1}n (in other words, the total function computed by C extendsf ). For any partial boolean f we let• C(f ) := the size of the smallest boolean circuit computing f ,• mC(f ) := the size of the smallest monotone boolean circuit computing f ,• F(f ) := the size of the smallest boolean formula computing f ,• mF(f ) := the size of the smallest monotone boolean formula computing f .
Non-negative Rank and Extended Formulations. Let B be a non-negative real matrix. The nonnegative rank of B, denoted rank+ (B), is the smallest integer r such that B can be written as the sumof r rank-1 non-negative matrices.
Non-negative rank is a very well-studied parameter in theoretical computer science, owing to its
close relationship with polytopes in convex optimization. We, however, will be particularly interested
in the connection between non-negative rank and circuit complexity.
Let 1m,n denote the m × n all-1s matrix (we may suppress the m, n when it is clear from context).
Let f : {0, 1}n → {0, 1, ∗} be a partial boolean function, let U = f −1 (1) and let V = f −1 (0). We let
Sf be the |U | × |V | matrix defined by, for each x ∈ U, y ∈ V ,Sf (x, y) =

n
X
i=1

Jxi 6= yi K

where JP K is the {0, 1}-indicator function for the predicate P . That is, the matrix Sf counts the numberof witnesses that x 6= y for each x ∈ f −1 (1), y ∈ f −1 (0). If the function f is furthermore monotone,
we define the matrix Sf+ by
n
X
Sf+ =
Jxi = 1 ∧ yi = 0K.
i=1

Observe that both Sf (x, y), Sf+ (x, y) ≥ 1 for all x ∈ U, y ∈ V . Because of this, we can say that for
any 0 < ε ≤ 1 the matrices Sf − ε1 and Sf+ − ε1 are both non-negative. With this in mind, we makethe following definitions (the second two, of course, only make sense for monotone f ):sep1 (f ) := rank+ (Sf − 1)
sep(f ) := min rank+ (Sf − ε1)
ε>0msep1 (f ) := rank+ (Sf+ − 1)
msep(f ) := min rank+ (Sf+ − ε1)
ε>0

We note the similarity between the definition of sep(f ) and deg+ (violC − ε) — the restriction of
Sherali-Adams — which was introduced in the previous section. Furthermore, as we have discussed indetail in Section 1, each of these parameters can be interpreted as the minimum size of any extended
formulation separating 0s of a function from 1s of a function, and they are closely related to circuit andformula size (cf. Theorem 1.3, Theorem 1.4).

113Upper Bounds

3.1

A New Characterization of Sherali-Adams Degree

In this section we provide our new characterization of Sherali-Adams degree, which is recorded next.
Theorem 1.5. For any unsatisfiable CNF formula C, if there is a Sherali-Adams refutation of C with
degree d and size s, then there is an ε > 0 and a degree d, size s2d conical junta J such that
violC − ε = J .
Consequently, if SA(C) is the minimum degree of any Sherali-Adams refutation of C, then
SA(C) = min deg+ (violC − ε).
ε>0Proof. Letm
X−C i Ji +X

λj Jj = −1ji=1

be a degree-d, size-s Sherali-Adams refutation of C, where each Ji are conical juntas. By expanding
each of the Ji into their monomials, we can re-write this proof astX−αk C ik mk +X

λj Jj = −1

(1)

j

k=1

for some t where αk ≥ 0 is a non-negative real constant and mk is a monomial for each k.
Now, fix some 1 ≤ u ≤ t. Assume w.l.o.g. that the variables occurring
Q in mu are x1 , x2 , . . . , x`
for some ` — explicitly, since mu is a monomial we therefore have mu = `i=1 xi = J[`],∅ . The main
claim we use is the following.
Claim. Let x1 , x2 , . . . , xn be any set of boolean variables. ThenX
JS,[n]\S = 1.
S⊆[n]ProofPof Claim. By induction
Pon n. If n = 0 then the only term
P in the sum is J∅,∅ , which is 1. If n > 0,then S⊆[n] JS,[n]\S = xn ( S⊆[n−1] JS,[n−1]\S )+(1−xn )( S⊆[n−1] JS,[n−1]\S ) = x1 +(1−x1 ) = 1
where we applied the induction hypothesis twice.
Define the conical junta
Ju :=

X

JS,[`]\S =S⊆[`],S6=[`]

X

JS,[`]\S − J[`],∅ .

S⊆[`]

By the Claim and the definition of Ju we have mu + Ju = J[`],∅ + Ju = 1. This means that
−αu mu C iu = −αu C iu J[`],∅ + αu C iu Ju − αu C iu Ju= −αu C iu + αu C iu Ju .

12

Since αu > 0 and C iu is a conjunction it follows that αu C iu Ju is a conical junta. By repeating thisconstruction for every polynomial −αk C ik mk it follows that we can rewrite the Sherali-Adams proof
from Equation 1 as


t
t
X
X
X
−αk C ik + 
λj Jj +
αk C ik Jk  = −1.
j

k=1

k=1

Replacing −αk C k mk by αk Cik Jk preserves the degree but increases the monomial size of the proof
by a 2d factor. By applying Lemma 2.1 it follows that there is a ε > 0 such that violC − ε = J forsome size at most s2d , degree-d conical junta J .

3.2

Feasible Interpolation for Sherali-Adams

In this section, we give a monotone interpolation theorem for Sherali-Adams in terms of the unsatisfiability certificate (cf. Definition 1.6). For our purposes, the important property of the unsatisfiability
certificate is the following connection it shares with violC .
Lemma 3.1. Let C be an unsatisfiable CNF formula on m clauses, let (X, Y ) be any partition of
the variables of C, and let cert be the corresponding unsatisfiability certificate. There are surjectionsµ : {0, 1}X → cert−1 (1) and ν : {0, 1}Y → cert−1 (0) such that+Scert(µ(x), ν(y)) = violC (xy)where xy denotes the concatenation of x, y.
Proof. We define µ and ν by their evaluations on assignments to the X and Y variables as follows.
For any x ∈ {0, 1}X define µx ∈ {0, 1}m by µxi = 1 − CiX (x) — that is, µix is 1 iff CiX (x) is
falsified. Similarly, for any y ∈ {0, 1}Y define ν y ∈ {0, 1}m by µyi = CiY (y) — so, νyi is 1 iff CiY (y)is satisfied. It follows by definition that cert(µx ) = 1 and cert(ν y ) = 0, and furthermore it is clearthat x 7→ µx and y 7→ ν y are surjective maps since every 1 and 0 assignment to cert must have some
witnessing assignments to the underlying variables. Finally, observe that if µxi = 1 and νiy = 0 thenCiX (x) = CiY (y) = 0, and thus the combined assignment xy violates the clause Ci . The converse also
clearly holds, proving the lemma.
By combining this fact with Theorem 1.5, we can immediately prove the following monotone
feasible interpolation theorem for Sherali-Adams proofs. This next theorem is slightly weaker (in that
we lose a 2d factor in the size) than the interpolation theorem stated in Section 1, but, has the benefit ofadmitting a completely transparent proof. We show how to remove the 2d factor in Appendix A.
Theorem 3.2. For any unsatisfiable CNF C and any partition of its variables (X, Y ), if there is aconical junta J of size s and an ε > 0 such that violC − ε = J thenrank+ (certC − ε) ≤ s.
Consequently, if there is a degree-d, size-s Sherali-Adams refutation of C then msep(certC ) ≤ s2d .
Proof. The “Consequently” statement of the theorem is just an application of Theorem 1.5, so we focus
on proving the non-negative
P rank upper bound for certC .
Write violC − ε =i λi Ji where each Ji is a conjunction. Under the partition of variables(X, Y ), we regard this as a {0, 1}X × {0, 1}Y matrix, where the (x, y)th entry of the matrix is exactly violC (xy) − ε. By Lemma 3.1 it follows immediately that rank+ (certC − ε) = rank+ (violC − ε),13since the existence of the two surjections implies that the matrix violC − ε is exactly the matrix certC − εwith some extra copies of rows and columns padded in. Thus if we show rank+ (violC − ε) ≤ s theproof of the theorem will be completed.
To show this, we use the expression of violC −ε as a conical junta. Observe that if Ji is a conjunction
over X and Y variables, then we can interpret any term zi or 1 − zi in the product Ji as a rank-1
2|X| × 2|Y | non-negative matrix (indeed, it is rank-1 since each term depends only on the x assignmentor the y assignment). If we let A ◦ B denote the Hadamard (i.e. entrywise) product of two matrices
A and B, it follows that the conjunction Ji is simply the Hadamard product of a number of rank1 non-negative matrices. Since rank+ (A ◦ B) ≤ rank+ (A) rank+ (B) — a fact easily verified bytaking non-negative rank decompositions — it follows that rank+ (Ji ) = 1. Therefore, if we can write
violC − ε = J where J is a non-negative combination of s conjunctions, it immediately follows by thesubadditivity of rank+ that rank+ (violC − ε) ≤ s, proving the theorem.

4Lower Bounds

In this section we prove our new separation between fragments of Sherali-Adams and Resolution andthen show how to lift this separation to a new separation between extension complexity (particularly,
msep1 ) and monotone circuit complexity. First, we show that the well-studied Pebbling formulas P EBG
require large conical junta degree to represent violP EBG − 1 (cf. Theorem 1.8). However, our eventual
goal is to apply a lifting theorem to get a strong lower bound on msep1 (f ) := rank+ (Sf+ − 1) fromthe lower bound on deg+ (violP EBG − 1) for some specially tailored monotone boolean function f .
Unfortunately, the known lifting theorems from conical junta degree to non-negative rank [33, 43] only
apply to approximate conical junta degree, which complicates the lower bound slightly.
Definition 4.1 (Approximate conical junta degree). For a non-negative function f : {0, 1}n → R≥0 weg
define its -approximate conical junta degree deg+
 (f ), as the minimum degree of a conical junta J
such that J (x) ∈ f (x) ±  for all inputs x.
For convenience, instead of proving lower bounds on the conical junta degree of P EBG directly,
we will instead work with the slightly more flexible Iteration problem I TERn (this is also sometimes
known as the Housesitting Principle) [4, 12]. An easy reduction from I TERn to P EBG will then yield
the degree lower bound for Pebbling formulas.

4.1

Conical Junta Lower Bound for Iteration

We study the Iteration problem I TERn on an n-by-n grid. An input to this problem consists of n2 input
variables xv , one for each grid node v ∈ [n] × [n]. The variables take values from an alphabet ofsize O(n). Namely, for each v ∈ [n − 1] × [n], we have xv ∈ [n] ∪ {⊥}. If xv ∈ [n], we say v is active,
and it points to the xv -th node on the next row. If xv = ⊥, we say v is disabled. For each node on the
final row v ∈ {n} × [n] there is a boolean variable xv ∈ {>, ⊥} where xv = > means xv is active andxv = ⊥ means v is disabled. The goal is to output one of the following types of solution.
(i) the distinguished source node (1, 1) is disabled (x1,1 = ⊥), or(ii) an active node that points to a disabled node (xi,j = k ∈ [n] and xi+1,k = ⊥), or(iii) an active node on the final row (xn,j = >).
For larger-than-boolean alphabets, we generalise the definition of a conjunction J naturally to bea partial assignment of pointers to nodes; for example, J = [x1,1 = 3; x2,3 = ⊥; x4,1 = 6] is a
14

1

2

3

4

1

3

⊥

4

⊥

2

⊥

⊥

2

3

3

⊥

4

2

⊥

4

⊥

>

⊥

>

Figure 4: An example outcome of the random variable X2 on I TER4 .
conjunction of degree 3. We prove strong lower bounds against the conical junta degree of violI TERn −1;
indeed, we are even able to prove lower bounds against the conical junta degree of violI TERn − 0.99,
which will turn out to be crucial for later results.
g
Theorem 4.2. deg+
1/20 (violI TERn − 1) ≥ Ω(n).
Proof. We define three random inputs X1 , X2 , X3 that admit 1, 2, or 3 solutions, all of type (iii). The
inputs are constructed from given data (vij ), j ∈ [2], i ∈ [n], that specifies for each row i ∈ [n], two(or three in the case of X3 ) nodes vi1 , vi2 ∈ {i} × [n]. The resulting input, call it X(vij ), is obtained byjactivating all the nodes vij , pointing vij to vi+1
, and disabling all other nodes.
X1 = “two random paths merging at the last row.” We choose vij for j ∈ [2], i ∈ [n] uniformly at
random subject to v11 = (1, 1), vi1 6= vi2 for i ∈ [n − 1], vn1 = vn2 . Then X1 = X(vij ).
X2 = “two random disjoint paths.” We choose vij for j ∈ [2], i ∈ [n] uniformly at random subject
to v11 = (1, 1), vi1 6= vi2 for i ∈ [n]. Then X2 = X(vij ).
X3 = “three random disjoint paths.” We choose vij for j ∈ [3], i ∈ [n] uniformly at random subject
0
to v11 = (1, 1), vij 6= vij for j 6= j 0 , i ∈ [n]. Then X3 = X(vij ).
PSuppose for the sake of contradiction that J = i λi Ji is a degree-o(n) conical junta that for every
input x outputs J (x) ∈ violI TERn (x) − 1 ±  where  := 1/20. We may assume that each conjunction
J in J is such that if it reads an active node v on row n − 1 (meaning that the conjunction contains[xn−1,j = k] for some k and v is node (n − 1, j)) then it also reads the boolean variable associatedwith node (n, xv ) on the last row. (Indeed, we may always replace J containing [xn−1,j = k] with theequivalent conic combination J · [xn,k = >] + J · [xn,k = ⊥].) We call a conjunction J paired if it
reads at least two active nodes on the last row, that is, J witnesses at least two solutions of type (iii).
Claim 4.3. If J is not paired, then E[J(X2 )] ≤ 2 · E[J(X1 )].
Claim 4.4. If J is paired, then E[J(X3 )] ≥ (3 − o(1)) · E[J(X2 )].

15

We provePthe claims shortly after we first complete the proof of the theorem assuming them. We
write J =i λi Ji = Jnot + Jpair where Jpair consists of conjunctions that are paired and Jnot
consists of those that are not. We calculate
1 −  ≤ E[J (X2 )](J approximates viol − 1)

= E[Jnot (X2 )] + E[Jpair (X2 )]≤ 2E[Jnot (X1 )] + E[Jpair (X2 )](Claim 4.3 and linearity of E)≤ 2 + E[Jpair (X2 )](J approximates viol − 1)

≤ 2 + E[Jpair (X3 )]/(3 − o(1))(Claim 4.4 and linearity of E)≤ 2 + (2 + )/(3 − o(1))(J approximates viol − 1)

< 1 − .

( < 1/10)

This is the desired contradiction that concludes the proof (modulo the Claims).
Proof of Claim 4.3. The claim says that Pr[J(X1 ) = 1] ≥ Pr[J(X2 ) = 1]/2 for a non-paired J.
Consider any fixed setting of the vij such that X(vij ) is in the support of X2 and such that J acceptsb
X(vij ). Since J is not paired, it does not read the nodes {vn−1, vnb } for some b ∈ [2], and hence if wepick b ∈ [2] uniformly at random, Prb [J((vij )i∈[n−1] , vnb , vnb ) = 1] ≥ 1/2. Moreover, if (vij )i∈[n] is
distributed as in the process for X2 , then ((vij )i∈[n−1] , vnb , vnb ) (for random b ∈ [2]) is distributed as in
the process for X1 . Hence J’s acceptance probability can decrease by at most a factor of 1/2.
Proof of Claim 4.4. The claim says that Pr[J(X3 ) = 1] ≥ (3 − o(1)) Pr[J(X2 ) = 1] for a paired J.
Since J reads at most o(n) nodes, there is some middle row i∗ ∈ [n/3, 2n/3] from which J reads nonodes. Split any input x into three parts so that x = (xT , xM , xB ) where xT is the pointer assignment
for nodes in topmost i∗ − 1 rows, xM is for nodes in row i∗ , and xB is for nodes in the remaining
bottommost rows. Write also J(x) = J T (xT ) · J B (xB ). Note that for both i = 2, 3, the variables XiT
and XiB are independent and thusPr[J(Xi ) = 1] = Pr[J T (XiT ) = 1 ∧ J B (XiB ) = 1] = Pr[J T (XiT ) = 1] · Pr[J B (XiB ) = 1].

(2)

We will prove the following estimates, which, when plugged into (2), would complete the proof:
Pr[J T (X3T ) = 1] ≥ (1 − o(1)) Pr[J T (X2T ) = 1],
B

B

B

B

Pr[J (X3 ) = 1] ≥ (3 − o(1)) Pr[J (X2 ) = 1].

(3)
(4)

Let us prove (3). Consider generating a sample from X3T as follows: (i) sample xT ∼ X2T , and (ii)
add to xT a random third path which is disjoint from the existing two. We argue that if the sample xT in
step (i) is accepted by J T , then the conjunction continues to accept after step (ii) with high probability.
Indeed, conditioned on the first step being accepting for J T , we note that the probability that any one
node is picked to lie on the third path is at most 1/(n − 2) and hence (by a union bound) the probability
that some node read by J T lies on the third path is at most deg(J)/(n − 2) = o(n)/(n − 2) = o(1).
Hence J T continues to accept with probability 1 − o(1), which proves (3).
Let us finally prove (4). Note how X2B (resp. X3B ) is distributed: it consists of two (three) uniformly
random disjoint paths down the grid. Consider the following bipartite graph (L ∪ R, E) where• Left vertices L are outcomes of X2B (pairs of disjoint paths).
• Right vertices R are outcomes of X3B (triples of disjoint paths).
16• There is an edge (l, r) ∈ E iff the two paths of l are a subset of the three paths of r.
Note that this graph is biregular with right degree dR := 3 and the left degree dL := 3|R|/|L|. Denoteby L0 ⊆ L (resp. R0 ⊆ R) the set of l ∈ L (resp. r ∈ R) accepted by J B . Let E(L0 , R0 ) := L0 × R0 ∩ E
denote the set of edges between L0 and R0 . Note that if r ∈ R0 , then at most one of r’s neighbours
is in L0 ; this is because J B is paired and hence it requires a prescribed pair of the three paths in
r to be present. Consequently |E(L0 , R0 )| ≤ |R0 |. On the other hand, if l ∈ L0 , then 1 − o(1)fraction of its neighbours are in R0 ; this is because of the same argument as in the preceding paragraph(condition on X2B = l ∈ L0 in step (i) and choose a random neighbour of l in step (ii)). Hence|E(L0 , R0 )| ≥ (1 − o(1))dL |L0 |. We now put these observations together to prove (4):
Pr[J B (X3B ) = 1] = |R0 |/|R|≥ |E(L0 , R0 )|/|R|≥ (1 − o(1))dL |L0 |/|R|= (3 − o(1))|L0 |/|L|= (3 − o(1)) Pr[J B (X2B ) = 1].

4.2

Lower bound for Pebbling

The Pebbling problem P EBG is defined relative to a DAG G = (V, E, v ∗ ) where v ∗ is a distinguishedsource node (in-degree 0) and where every node has out-degree at most 2 (but in-degree may be unbounded). The input to P EBG is y ∈ {0, 1}E , that is, an boolean assignment to the edges of G. Suchan assignment y naturally defines a subgraph Gy of G consisting of all the edges e such that ye = 1,
which we call the active edges. The goal is to output one of the following types of solution.
(i) the distinguished source node is a sink (out-degree 0) in Gy .
(ii) a node v ∈ V that is a proper sink in Gy , meaning v has in-degree ≥ 1 and out-degree 0.
Note that the presence of any solution can be certified by reading at most 3 bits, and hence P EBG
corresponds to the canonical search problem of an unsatisfiable 3-CNF formula. Moreover, if G has medges then this 3-CNF formula has at most m + 1 clauses, as every possible violation in P EBG is either
the violation of the first type, or can be identified with an incoming edge to a node. It follows that for
all z ∈ {0, 1}mviolP EBG (z) − 1 ≤ m,(5)
which we have recorded for later use.
We prove the following theorem, which is a strengthening of Theorem 1.8.
Ω(1) .
g
Theorem 4.5. There is a DAG G with m edges such that deg+
1/20 (violP EBG − 1) ≥ m

Proof. We describe a simple reduction from I TERn to P EBG where G has O(n3 ) edges. The goal of the
reduction is to show that any degree-d conical junta approximating violP EBG − 1 can be translated intoa degree-d conical junta approximating violI TERn − 1. Hence the theorem follows from Theorem 4.2.
The DAG G = (V, E, v ∗ ) is defined as follows. First, V includes all nodes in the grid [n] × [n]underlying I TERn . We naturally set v ∗ := (1, 1). Observe that naively connecting each grid node to all
its possible n successors on the subsequent row would result in a DAG of unbounded out-degree. To
circumvent this, we instead include in G for every node v = (i, j) ∈ [n − 1] × [n], a log n-depth binary
tree Tv with n leaves `v1 , . . . , `vn . We identify the root of Tv with v and we identify each leaf `vk with the17grid node (i + 1, k) ∈ [n] × [n]. Finally, we include in V an extra bottom row of nodes {n + 1} × [n].
For every grid node (n, j) on the n-th row, we include the single edge ev := ((n, j), (n + 1, j)). This
completes the description of G.
Given an input x to I TERn we define an input y = y(x) to P EBG as follows. Consider a nodev ∈ [n − 1] × [n]. If xv = k ∈ [n] we activate all edges on the unique root-to-`vk path in Tv and disable
the other edges in Tv . If xv = ⊥ we disable all edges in Tv . Finally, for a node v = (n, j) on the lastrow, we activate its associated edge ev iff xv = >.
Note that y = y(x) faithfully “models” the input x in the sense that the solutions of x appear associated with the same nodes as solutions in y. In particular, violI TERn (x) = violP EBG (y). Moreover, eachvariable ye of P EBG is a function of a single variable of I TERn . Thus every degree-d conjunction J(y)can be translated into a degree-d conjunction J 0 (x) such that J 0 (x) = J(y(x)). Applying this translation to the conjunctions in a conical junta, we conclude that if there is a conical junta approximating
violP EBG − 1, there is one for approximating violI TERn − 1 of the same degree.

4.3

Separating Extended Formulations from Monotone Circuits

As we have seen in Section 2, if f : {0, 1}n → {0, 1, ∗} is a partial monotone boolean function thenmsep(f ) := min rank+ (Sf+ − ε1) ≤ mC(f ),ε>0andmsep1 (f ) := rank+ (Sf+ − 1) ≤ mF(f ),where mC(f ) (mF(f )) is the size of the smallest monotone circuit (formula, resp.) computing f . It isnatural to wonder if it is necessary to chose ε < 1 in order to simulate monotone circuits — in otherwords, whether or not msep1 (f ) is already upper bounded by mC(f ). In this section, we show that the
separation proven in Section 4.2 implies that such a bound is not possible. In particular, we prove thefollowing theorem:
Theorem 1.9. The G ENn function is computable by polynomial-size monotone circuits, but, there is aδ
δ > 0 such that msep1 (G ENn ) = 2Ω(n ) .
Let us begin by defining the G ENn function, which was originally introduced by Raz and McKenzie [51] and has now been the subject of a number of works in circuit complexity [13,22,23,34,51,54].
Definition 4.6. Let n be a positive integer. A set of triples T ⊆ [n]3 is said to generate k ∈ [n] if k = 1
or if there is a triple (i, j, k) ∈ T such that T generates both i and j.
The G ENn function is a monotone boolean function defined as follows. As input, the function
3
receives a list of triples T ⊆ [n]3 encoded as a binary string of length {0, 1}n . It then outputs 1 if andonly if n can be generated from T .
It is well known that G ENn has polynomial-size monotone circuits [51], so, we focus on proving
the lower bound in Theorem 1.9. To do this we apply the following lifting theorem from conical junta
degree to non-negative rank due to Kothari, Meka, and Raghavendra [43] (we note that applying thelifting theorem from Göös et. al. would also yield an essentially identical result [33]). In order to state
the theorem we introduce the important notion of a pattern matrix:
Definition 4.7. Let f : {0, 1}n → R be a boolean function, and let g : X × Y → {0, 1} be any
function. Define the pattern matrix f ◦ g n : X n × Y n → R for any x ∈ X n , y ∈ Y n by(f ◦ g n )(x, y) := f (g(x1 , y1 ), g(x2 , y2 ), . . . , g(xn , yn )).
18

We note that even though we have defined it as a function, we think of f ◦ g n as a X n × Y n matrix inthe natural way.
The next theorem is a slight modification of Theorem 1.7 in [43], and follows immediately fromthe proof of [43].
Theorem 4.8. Let f : {0, 1}n → R≥0 be any boolean function with E[f ] = 1, and suppose thatdeg+ (f +1/100n) ≥ 9 deg(f ). For any b ≥ 100 log n there is a gadget function g : {0, 1}b ×{0, 1}b →{0, 1} such that+rank+ (f ◦ g n ) = 2Ω(b deg (f +1/100n)) .
We combine this theorem with our lower bound for P EBG from the previous section (Theorem 4.5)
and an embedding argument to prove the Theorem 1.9.
δTheorem 4.9. There is a constant δ > 0 such that for all sufficiently large n, msep1 (G ENn ) ≥ 2Ω(n ) .
Proof. Let G be the DAG with m edges guaranteeing the approximate conical junta degree lower boundfrom Theorem 4.5, and let g be the gadget function guaranteed by Theorem 4.8. We begin by showingthatδ
rank+ ((violP EBG − 1) ◦ g m ) = 2Ω(m )for some universal constant δ > 0. Once we have this, we show that the pattern matrix (violP EBG − 1) ◦+associated with G ENn (cf. Section 2);
g m can be embedded as a submatrix of the slack matrix SU,V
since non-negative rank is monotone decreasing with respect to taking submatrices this immediatelyδimplies msep1 (G ENn ) ≥ 2Ω(n ) , proving the theorem.
Let f = violP EBG −1, with the goal of applying the previous lifting theorem, and note f : {0, 1}m →R≥0 and furthermore that f (x) ≤ m by Equation 5. It follows that Ef ≤ m, and thus there is someε ≤ 1/100 such thatdeg+ (f /Ef + 1/100m) = deg+ (violP EBG − 1 + Ef /100m)= deg+ (violP EBG − (1 − ε))
δ
g
≥d
eg+
ε (violP EBG − 1) ≥ m
where we have used the fact that deg+ is invariant under multiplying by positive constants, and also
Theorem 4.5. Finally, since violP EBG can be represented as a sum of violations of a 3-CNF formula itfollows that deg(f ) = 3. We can therefore apply Theorem 4.8 and conclude thatδ

rank+ ((violP EBG − 1) ◦ g m ) = 2Ω(m ) .
So, in the remainder of the proof we show, for any DAG G with m edges, (violP EBG − 1) ◦ g m
can be embedded as a submatrix of the slack matrix SG+ENn associated with the G ENn function forsome n = poly(m). This is the same embedding argument that has been used in many works relating“lifted” P EBG to G ENn [22, 34, 51, 54]; for this reason, we only sketch the argument for the sake ofcompleteness. Recall from Section 2 the definition of Sf+ : if f : {0, 1, ∗}n → {0, 1} is a partial
monotone boolean function and U = f −1 (1), V = f −1 (0), then Sf+ is the |U | × |V | matrix defined by
Sf+ (x, y) =nXJxi = 1 ∧ yi = 0Ki=119

for all x ∈ U, y ∈ V . To construct our embedding we create two mappings µ : {0, 1}mb → G EN−1n (1)+m )(x, y).
and ρ : {0, 1}mb → G EN−1
(0)
such
that
S
(µ(x),
ρ(y))
=
(viol
◦
g
P EBG
n
G ENn
Let G be any DAG with m edges, and assume without loss of generality that G has a single distinguished source node s∗ with a single outgoing edge, and sink nodes u1 , . . . , ut . We define an auxiliarygraph Gaux as follows. The nodes of the auxiliary graph Gaux are the edges of G. Then, if (u, v), (v, w)
are edges of G that share a node v, we add a directed edge ((v, w), (u, v)) to Gaux (note the reversein the edge direction). Note the sink node of Gaux corresponds to the unique edge leaving the source
node of s∗ , and the source nodes of Gaux correspond to the edges that enter sinks of G.
Letting N = 2b , for each node in Gaux we create N points in the resulting G EN instance, andwe index each such point as ex for each x ∈ {0, 1}b . We also create a designated start node 1 and adesignated target node n.
Now we describe the functions µ, ρ in the embedding.
mb• Definition of µ : {0, 1}mb → G EN−1
and write x = x1 x2 · · · xm wheren (1). Let x ∈ {0, 1}b12m
xi ∈ {0, 1} . Order the edges e , e , . . . , e , and we regard e1 as the unique edge leaving thedistinguished source node. We regard each xi ∈ {0, 1}b as selecting the point eixi from theresulting G EN instance; we then plant a copy of Gaux inside the G EN instance on these points.
That is, whenever a node u = ei in Gaux has two incoming edges from v = ej , w = ek , weplant the triple (eixi , ejxj , ekxk ); when u has only a single incoming edge from v we plant the triple(ejxj , ejxj , eixi ). Finally, for each of source nodes u = ei of Gaux we add the triple (1, 1, eixi ).
It is easy to see that the result is in G EN−1 (1), since we have explicitly planted the graph Gaux
connecting the source node 1 to the target node n.
mb• Definition of ρ : {0, 1}mb → G EN−1
we similarly write y = y1 y2 · · · ymn (0). Given y ∈ {0, 1}
and add triples to the instance as follows. For any constraint of P EBG enforcing that a node v
in G is not a proper sink (for example, by preventing the case where ei = (u, v) is in G and
ej = (v, w1 ), ek = (v, w2 ) are not in G), and for any xi , xj , xk ∈ {0, 1}b , we add the triple(ejxj , ekxk , eixi ) to the instance iff the constraint is satisfied by the assignment ei = g(xi , yi ), ej =g(xj , yj ), ek = g(xk , yk ). We apply a similar construction for each of the constraints corresponding to the source node of s∗ having an outgoing edge and set all other triples to 0. This is a0-instance of G ENn since if it was a 1-instance it must contain an embedding of Gaux (as in theconstruction of µ above), but this would imply that the corresponding assignment x embedding
Gaux would satisfy every constraint of P EBG , which is a contradiction.

Finally, to see that SG+ENn (µ(x), µ(y)) = violP EBG (g m (x, y)) observe that, by construction, each triplein µ(x) which does not occur in µ(y) corresponds exactly to a unique violated constraint of P EBG .

AMonotone Feasible Interpolation for Sherali-Adams

In this appendix we prove a refinement of Theorem 3.2, showing that Sherali-Adams is interpolated
by non-negative span programs, a model introduced by de Oliveira Oliveira and Publák [20] as anextension of the classic span program of Karchmer and Wigderson [42].
Non-negative Span Programs. A non-negative span program (over the reals) is defined by a matrix
M ∈ Rk×t , a labelling ρ ∈ {1, zi , ¬zi }k of the rows, and a “target” vector b ∈ Rt . The program ismonotone if no row is labelled by ¬zi . The non-negative span program accepts an input z ∈ {0, 1}n if20

b is a conic combination of the rows of M labelled by 1 under z. That is, letting M ρ(z) be the matrix
obtained from M by replacing each column c ∈ [k] for which ρj (z) = 0 by the all-0 row, the nonnegative span program accepts iff there is non-negative vector y ∈ Rk such that y > M ρ(z) = b. A span
program computes a function f : {0, 1}n → {0, 1} if
f (z) = 1 ⇐⇒ ∃y ∈ Rk≥0 , y > M ρ(z) = b.
The size of a non-negative span program is the size of the matrix M .
It is known that non-negative span programs are simulated by msep. Therefore, the followinginterpolation theorem improves upon Theorem 3.2 in two ways: it provides a tighter connection of
Sherali-Adams proofs to a computational model, and it removes the pesky blow-up of 2d .
Theorem A.1. Let C be any unsatisfiable CNF formula and (X, Y ) be any partition of its variables. If
there is a Sherali-Adams refutation of C of size s then there is a O(s2 )-size non-negative span program(X,Y )
computing certC.
We begin with some definitions that will be used throughout this section. A set of polynomials P
is unsatisfiable (modulo the ideal hx2i = xi ini=1 ) if there is no x ∈ {0, 1}n such that p(x) ≥ 0 for
all p ∈ P . For this section it will be convenient to define Sherali-Adams refutations for more generalunsatisfiable sets of polynomials, rather than only CNF formulas. We state this generalization next, ina manner that will be convenient for this section.
A Sherali-Adams refutation of an unsatisfiable set of polynomials P on variables x1 , . . . , xn isgiven by a set of polynomials R such that
• R contains only polynomials of the form pJ, or J, for p ∈ P and J a non-negataive junta.
• The constant −1 is in the cone generated by taking non-negative linear combinations of thepolynomials in R.
The size of a Sherali-Adams derivation is the number of distinct monomials occurring in the (monomial
expansion of) the polynomials in R.
We will work with a slight generalization of interpolant functions for polynomials. For an unsatisfiable set of polynomials A(x, z) ∪ B(y, z) let(
0 if A(x, α) is satisfiable,
IA∪B (α) =1 if B(y, α) is satisfiable.
be the associated interpolant function.
The proof of Theorem A.1 will proceed as follows. First, we will reduce the task of constructing acomputation of an unsatisfiability certificate certC from a refutation of a CNF formula C to the task of
constructing an interpolant IAC ∧BC from a refutation of an associated split formula AC ∧ BC . Following
this, we show how to extract a small non-negative span program computing the monotone interpolant.
We will do this in two steps. First, we will show that a feasible disjunction property holds for SheraliAdams: from any refutation of an unsatisfiable system of polynomials A(x, z) ∧ B(y, z) and a {0, 1}assignment α to the z-variables, we can extract a refutation of A(x, α) or B(y, α) of roughly the same
size. Second, we will use this feasible disjunction property to construct a monotone non-negative span
program which has the same size as the Sherali-Adams refutation and searches for a refutation ofA(x, α).
21Reduction to Interpolant Formulas. Given any unsatisfiable CNF formula C we will describe atransformation of C into a monotone split formula due to Hrubeš and Pudlák [41]. Then, we will argue
that any computation of the interpolant IC of the split formula associated with C is also a computationof certC . Recall that we say that a split (CNF) formula A(x, z)∧B(y, z) is monotone if every z-variable
in A occurs negatively.
From a CNF formula C = C1 ∧ . . . ∧ Cm and a partition (X, Y ) of its variables, we will define themonotone CNF formula AC (X, Z) ∧ BC (Y, Z) as follows. Introduce m new variables z1 , . . . , zm anddefineX
AC (x, z) := (C1X ∨ ¬z1 ) ∧ . . . ∧ (Cm∨ ¬zm )Y
BC (y, z) := (C1Y ∨ z1 ) ∧ . . . ∧ (Cm∨ zm )(X,Y )Let ICbe the interpolant associated with the split formula for AC ∧ BC :(0 if {CiX : αi = 1} is satisfiable,(X,Y )IC(α) =1 if {CiY : αi = 0} is satisfiable.
(X,Y )(X,Y )

Observe that IC
is exactly certC. Finally, we record the following observation, which relates
the complexity of C and AC (x, z) ∧ BC (y, z).
Observation A.2. There is a Sherali-Adams derivation of C from AC (x, z) ∧ BC (y, z) of size |C|.
Thus, a lower bound on the size of refutations of the split formula would imply a lower bound on
the size of refutations of C.
Feasible Disjunction. We will show that from a Sherali-Adams refutation R of an unsatisfiable setof polynomials A(x, z) ∪ B(y, z) and assignment α 7→ z we can extract a refutation of either A(x, α)or B(y, α) of the same size. In fact, we will first argue that simply restricting the polynomials in
R(x, y, z) to either the x-variables or the y-variables will constitute a refutation of either A(x, α) or
B(y, α). Let RA (x, z) be the set of polynomials obtained by projecting R onto the (x, y)-variables.
That is, RA is formed by first removing any polynomial involving an axiom from B (i.e., polynomialsof the form p(y, z)J(x, y, z) for p ∈ B) and discarding the y-juntas from the remaining polynomials(i.e., p(x, z)J(x, z)J 0 (y) is replaced by p(x, z)J(x, z) for p ∈ A. Let RB (y, z) be defined analogously.
Lemma A.3. Let α be any {0, 1}-assignment to the variables z. If there is a Sherali-Adams refutation
R of an unsatisfiable set of polynomials A(x, z) ∪ B(y, z) of size s then there is a refutation of A(x, α)or B(y, α) using only the polynomials in RA (x, α) or RB (y, α) respectively.
The proof of this lemma is similar to a main lemma from [37]. It will be convenient to recall thefollowing notion of a pseudo-expectation for a set of polynomials R ⊆ R[x].
Definition A.4. Let R be a set of polynomials. A pseudo-expectation for R is a linear function Ẽ :R[x] → R satisfying
1. Ẽ[1] = 1,
2. Ẽ[p] ≥ 0 for every p ∈ R.

22

It is easy to see that −1 is a conic combination of the polynomials in R if and only if there is no
pseudo-expectation for R.
Claim. R is a Sherali-Adams refutation if and only if there is no pseudo-expectation for R.
Proof of Claim. Suppose for contradiction that R is a Sherali-Adams refutation and that there exists a
pseudo-expectation Ẽ for R. By the first assumption, there exists λ1 , . . . , λ|R| ∈ R≥0 such thatX
λi pi = −1.
pi ∈RApplying Ẽ to both sides of this equation yields a contradiction.
For the other direction, define the following sets
T1 := {p ∈ R[x] : p is a conic combination of polynomials R},
T2 := {−1}.
Since these sets are disjoint and convex, the hyperplane separation theorem yields a linear function
L : R[x] → R such that L[p] ≥ 0 for every p ∈ T1 and L[−1] < 0. By linearity of L, L[1] > 0. DefineẼ as follows: for any polynomial p ∈ R[x] letẼ[p] := L[p]/L[1]and observe that the desired properties hold.
We are now ready to prove Lemma A.3.
Proof of Lemma A.3. Let R(x, y, z) be a Sherali-Adams refutation of A(x, z) ∪ B(y, z) and henceR(x, y, α) is a refutation of A(x, α) ∪ B(y, α). Suppose that neither RA (x, α) nor Ry (y, α) is a
refutation; that is, −1 cannot be formed as a conic combination of the polynomials RA or RB . By theprevious claim there exists pseudo-expectations Ẽx and Ẽy for RA (x, α) and RB (y, α) respectively.
Define a linear function Ẽ : R[x, y] → R as follows: for every monomial m(x)m0 (y) letẼ[m(x)m0 (y)] := Ẽx [m(x)] · Ẽy [m0 (y)],and extend Ẽ linearly. We claim that Ẽ is a pseudo-expectation for R(x, y, α). Indeed, the following
holds by constructionẼ[p(x)J(x)J 0 (y)] = Ẽx [p(x)J(x)] · Ẽy [J(y)] ≥ 0,for every p(x)J(x)J 0 (y) ∈ R(x, y, α), and similarly for q(y)J(x)J 0 (y) ∈ R(x, y, α). Thus, Ẽ is a
pseudo-expectation for R(x, y, α), which by the previous claim is a contradiction.
Interpolation by Non-negative Span Programs. We now turn to showing that Sherali-Adams refutations of split formulas are interpolated by (monotone) non-negative span programs.
Recall that we say that a CNF formula A(x, z) ∧ B(y, z) on variables is monotone if only negative
z-literals appear in A. More generally, we say an unsatisfiable set of polynomials A(x, z) ∪ B(y, z) ismonotone if every p ∈ A(x, z) can be written as polynomialYp(x, z) :=zi p(x)i∈Ifor some (potentially empty) set of indices I and p ∈ R[x].
23Theorem A.5. Let A(x, z) ∪ B(y, z) be an unsatisfiable set of polynomials. If there is a Sherali-Adams
refutation of A(x, z) ∪ B(y, z) of size s then there is a non-negative span program M of size poly(s)such that M computes the interpolant IA∪B . Furthermore, if A(x, z) ∪ B(y, z) is monotone then so isM.
We will first prove our interpolation theorem for sets of polynomials A(x, z) ∪ B(y, z) satisfying
the following normal form from [49]. Afterwards, we will argue that this normal form assumption is
without loss of generality.
Definition A.6. A set of polynomials A(x, z) ∪ B(y, z) is in normal form if every polynomial either
does not contain a variable from z or is of the form zi p(x) + p0 (x) for a variable zi .
The high-level idea is that from a refutation R of A ∪ B we will construct a non-negative span
program which, on input α, searches for a refutation in RA (x, α). The columns of the non-negative
span program will be labelled by all monomials restricted to the x-variables in R and each row of the
non-negative span program will be a polynomial from RA (x, α). Therefore, there will exist a nonnegative linear combination of the rows equalling (−1, 0, . . . , 0), where the first column is corresponds
to the monomial 1, if and only if RA (x, α) is a Sherali-Adams refutation.
Lemma A.7. If there is a Sherali-Adams refutation of an (monotone) unsatisfiable set of polynomials
A(x, z) ∪ B(y, z) in normal form of size s then there is a (monotone) non-negative span program M
of size O(s2 ) computing the interpolant IA∪B .
Proof. Let R be a refutation of A(x, z) ∪ B(y, z). We will construct a non-negative span program(M, ρ, b) which, given an assignment α, searches for a refutation in RA (x, α). Denote by Sx the setof monomials in the variables x that occur in the polynomials R, including the constant 1. That is,m(x) ∈ Sx iff there exists a monomial m0 (y, z) and polynomial p ∈ RA such that mm0 occurs in the
expansion of p as a sum of monomials. The columns of the matrix M will index all monomials in Sx .
The rows of M will be all polynomials in RA (x, y), more formally the coefficients vectors of thosepolynomials. We will accomplish this as follows:• For each polynomial (zi p(x) + p0 (x))J(x)J 0 (z) in RA , if zi = 1 ; J 0 (z) = 0 create a row
containing the coefficient vector of the polynomial (p(x) + p0 (x))J(x) and label the row with zi .
As well, if zi = 0 ; J 0 (z) = 0 create a row containing the coefficient vector of p0 (x)J(x) andlabel it ¬zi .
• For each polynomial p(x)J(x)J 0 (y) ∈ RA which does not depend on a z-variable, create a row
containing the coefficient vector of p(x)J(x) and label it 1.
Let ρ be the labelling that results, and define b := (−1, 0, . . . , 0), where we have assumed that the firstcolumn of M corresponds to the monomial 1. Observe that the non-negative span program (M, ρ, b)
accepts if and only if −1 is a non-negative linear combination of the rows labelled 1 under an assignment α ∈ {0, 1}n . That is, the non-negative span program tests whether there is a Sherali-Adams
refutation of A(x, α) using the polynomials RA . Furthermore, if A is monotone, then we no longer
have any rows labelled by ¬zi and the non-negative span program is monotone.
It remains to argue that (M, ρ, b) computes IA∪B correctly. That is, if it accepts α ∈ {0, 1}n thenA(x, α) is unsatisfiable and if it rejects α then B(y, α) is unsatisfiable. This follows from Lemma A.3,
noting that the rows of M ρ(α) are exactly coefficient vectors of the polynomials in R(x, α). The nonnegative span program has at most |Sx | columns and |RA | rows, and is therefore of size of O(|R|2 ).
24

To prove Theorem A.5 it remains to show that the normal form assumption is without loss ofgenerality; for this, we will use the transformations of Pudlák and Sgall [49]. In particular, any set ofpolynomials A(x, z) can be transformed into normal form via the following process:1. Introduce |z| new variables w.
2. Replace each polynomial p(x, z) for p ∈ A by the polynomial p(x, w).
3. For each zi , introduce the constraint wi − zi = 0.
It is easy to see that the resulting formula is satisfiable iff the original formula is satisfiable. Next, weshow that Sherali-Adams can efficiently deduce the original formula from this normal form.
Claim. The constraints of A(x, z) can be deduced in Sherali-Adams in size poly(|A|) from the constraints which result from the aforementioned transformation.
Proof of Claim. Consider any monomial m(x, w) that is present in the monomial expansion of theconstraints resulting from the transformation; we will deduce m(x, z) as follows. Denote by m(x, w \wi ) the monomial obtained by discarding variable wi . Sequentially, for each variable wi in m(x, w, z),replace m(x, w) by m(x, w)+m(x, w\wi )(xi −wi ) if m occurs positively in A(x, z) and by m(x, w)+m(x, w \ wi )(wi − xi ) if m occurs negatively.
Unfortunately, for monotone sets of polynomials A(x, z) this transformation destroys the monotonicity. We will circumvent this by using an alternative transformation for monotone formulas:Q
1. For each monotone polynomial ki=1 zi p(x) in A, introduce new variables wi for i ∈ [k].
Q
2. Replace ki=1 zi p(x) by the following set of polynomial inequalities

z1 p(x) +kXwi = 0, z2 w2 = 0, . . . , zk wk = 0.

i∈2

It is not difficult to see that this transformation preserves satisfiability. One direction follows bysoundness and the observation that the constraints of the monotone normal form can be derived from theconstraints of the original
Q formula in Sherali-Adams. For the other direction, consider any satisfying
assignment (x, z) to ki=1 zi p(x) and note that either some zi = 0 or p(x) = 0. In the first case, set
wi = −p(x) and wj = 0 for j 6= i. In the second case, set wj = 0 for all j.
Claim. The constraints of A(x, z) can be deduced in Sherali-Adams from the constraints which result
from the transformation in size poly(|A|).
Q
Proof of Claim. We will prove that each polynomial ki=1 zi p(x) A(x, z) can be deduced in polynomial size from the constraints that result from its monotone transformation as follows: For each2 ≤ i ≤ k deduce z1 . . . zk wi = 0 and add it to z1 . . . zk (p(x) + w1 + . . . + wk ) = 0.
We can now prove Theorem A.5.
Proof of Theorem A.5. Let A(x, z) ∧ B(y, z) be a (monotone) unsatisfiable set of polynomials. By
the previous claims we can assume without loss of generality that these formulas are in normal form.
Applying Lemma A.7 completes the proof.
25

Finally, we are ready to prove the main theorem of this section.
Proof of Theorem A.1. Suppose that there is a Sherali-Adams refutation of C of size s. Then, by Observation A.2, there is a refutation of the associated split formula AC ∧ BC of size O(s). Applying
Theorem A.5 to AC ∪ BC , produces a monotone non-negative span program of size poly(s) computing(X,Y )(X,Y )
IC, which is equivalent to certF.

References[1] Sanjeev Arora, Béla Bollobás, László Lovász, and Iannis Tourlakis. Proving integrality gaps
without knowing the linear program. Theory Comput., 2(2):19–51, 2006.
[2] Albert Atserias and Elitza N. Maneva. Sherali-adams relaxations and indistinguishability in counting logics. In Shafi Goldwasser, editor, Innovations in Theoretical Computer Science 2012, Cambridge, MA, USA, January 8-10, 2012, pages 367–379. ACM, 2012.
[3] Albert Atserias and Joanna Ochremiak. Proof complexity meets algebra. ACM Trans. Comput.
Log., 20(1):1:1–1:46, 2019.
[4] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The
relative complexity of NP search problems. In Frank Thomson Leighton and Allan Borodin,
editors, Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, 29
May-1 June 1995, Las Vegas, Nevada, USA, pages 303–314. ACM, 1995.
[5] Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for lov[a-acute]sz–schrijver
systems and beyond follow from multiparty communication complexity. SIAM J. Comput.,
37(3):845–869, 2007.
[6] Siavosh Benabbas, Konstantinos Georgiou, Avner Magen, and Madhur Tulsiani. SDP gaps frompairwise independence. Theory Comput., 8(1):269–289, 2012.
[7] Christoph Berkholz. The relation between polynomial calculus, sherali-adams, and sum-ofsquares proofs. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical
Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 11:1–11:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
[8] Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs withsmall coefficients. J. Symb. Log., 62(3):708–728, 1997.
[9] Gábor Braun, Samuel Fiorini, Sebastian Pokutta, and David Steurer. Approximation limits oflinear programs (beyond hierarchies). Math. Oper. Res., 40(3):756–772, 2015.
[10] Gábor Braun and Sebastian Pokutta. Common information and unique disjointness. Algorithmica,
76(3):597–629, 2016.
[11] Mark Braverman and Ankur Moitra. An information complexity approach to extended formulations. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theoryof Computing Conference, STOC’13, Palo Alto, CA, USA, June 1-4, 2013, pages 161–170. ACM,
2013.

26

[12] Samuel R. Buss. Lower bounds on nullstellensatz proofs via designs. In Paul Beam and Samuel R.
Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop,
New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete
Mathematics and Theoretical Computer Science, pages 59–71. DIMACS/AMS, 1996.
[13] Siu Man Chan and Aaron Potechin. Tight bounds for monotone switching networks via fourier
analysis. Theory Comput., 10:389–419, 2014.
[14] Siu On Chan, James R. Lee, Prasad Raghavendra, and David Steurer. Approximate constraint
satisfaction requires large LP relaxations. J. ACM, 63(4):34:1–34:22, 2016.
[15] Moses Charikar, Konstantin Makarychev, and Yury Makarychev. Local global tradeoffs in metricembeddings. SIAM J. Comput., 39(6):2487–2512, 2010.
[16] Arkadev Chattopadhyay, Yuval Filmus, Sajin Koroth, Or Meir, and Toniann Pitassi. Query-tocommunication lifting using low-discrepancy gadgets. SIAM J. Comput., 50(1):171–210, 2021.
[17] Arkadev Chattopadhyay, Michal Koucký, Bruno Loff, and Sagnik Mukhopadhyay. Simulation
theorems via pseudorandom properties. CoRR, abs/1704.06807, 2017.
[18] Stefan S. Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes. Tight rank lower
bounds for the sherali-adams proof system. Theor. Comput. Sci., 410(21-23):2054–2063, 2009.
[19] Wenceslas Fernandez de la Vega and Claire Kenyon-Mathieu. Linear programming relaxations of
maxcut. In Nikhil Bansal, Kirk Pruhs, and Clifford Stein, editors, Proceedings of the Eighteenth
Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2007, New Orleans, Louisiana,
USA, January 7-9, 2007, pages 53–61. SIAM, 2007.
[20] Mateus de Oliveira Oliveira and Pavel Pudlák. Representations of monotone boolean functions
by linear programs. ACM Trans. Comput. Theory, 11(4):22:1–22:31, 2019.
[21] Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, andDmitry Sokolov. Automating algebraic proof systems is np-hard. In Samir Khuller and Virginia Vassilevska Williams, editors, STOC ’21: 53rd Annual ACM SIGACT Symposium on Theoryof Computing, Virtual Event, Italy, June 21-25, 2021, pages 209–222. ACM, 2021.
[22] 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.
[23] Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How limited interaction hinders
real communication (and what it means for proof and circuit complexity). In Irit Dinur, editor,
IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9-11 October
2016, Hyatt Regency, New Brunswick, New Jersey, USA, pages 295–304. IEEE Computer Society,2016.
[24] Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. Maxsat resolution and subcube
sums. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing- SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume12178 of Lecture Notes in Computer Science, pages 295–311. Springer, 2020.
27

[25] Samuel Fiorini, Serge Massar, Sebastian Pokutta, Hans Raj Tiwary, and Ronald de Wolf. Exponential lower bounds for polytopes in combinatorial optimization. J. ACM, 62(2):17:1–17:23,
2015.
[26] 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, volume 200 of LIPIcs, pages 6:1–6:30.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[27] Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm
design. Electron. Colloquium Comput. Complex., 26:106, 2019.
[28] 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.
[29] 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.
[30] Mika Goos. Communication Lower Bounds via Query Complexity. PhD thesis, University ofToronto (Canada), 2016.
[31] Mika Göös, Rahul Jain, and Thomas Watson. Extension complexity of independent set polytopes.
SIAM J. Comput., 47(1):241–269, 2018.
[32] Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is nphard. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia
Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 68–77. ACM, 2020.
[33] Mika Göös, Shachar Lovett, Raghu Meka, Thomas Watson, and David Zuckerman. Rectangles
are nonnegative juntas. SIAM J. Comput., 45(5):1835–1869, 2016.
[34] Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM
J. Comput., 47(5):1778–1806, 2018.
[35] Mika Göös, Toniann Pitassi, and Thomas Watson. Query-to-communication lifting for BPP.
SIAM J. Comput., 49(4), 2020.
[36] Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity.
Theor. Comput. Sci., 259(1-2):613–622, 2001.
[37] Tuomas Hakoniemi. Feasible interpolation for polynomial calculus and sums-of-squares. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany(Virtual Conference), volume 168 of LIPIcs, pages 63:1–63:14. Schloss Dagstuhl - LeibnizZentrum für Informatik, 2020.

28

[38] Samuel B. Hopkins, Tselil Schramm, and Luca Trevisan. Subexponential lps approximate maxcut. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham,
NC, USA, November 16-19, 2020, pages 943–953. IEEE, 2020.
[39] Pavel Hrubes. On the nonnegative rank of distance matrices. Inf. Process. Lett., 112(11):457–461,
2012.
[40] Pavel Hrubes. On -sensitive monotone computations. Comput. Complex., 29(2):6, 2020.
[41] Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Chris
Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017,
Berkeley, CA, USA, October 15-17, 2017, pages 121–131. IEEE Computer Society, 2017.
[42] Mauricio Karchmer and Avi Wigderson. On span programs. In Proceedings of the Eigth Annual
Structure in Complexity Theory Conference, San Diego, CA, USA, May 18-21, 1993, pages 102–111. IEEE Computer Society, 1993.
[43] Pravesh Kothari, Raghu Meka, and Prasad Raghavendra. Approximating rectangles by juntas andweakly-exponential lower bounds for LP relaxations of csps. CoRR, abs/1610.02704, 2016.
[44] Pravesh K. Kothari, Ryuhei Mori, Ryan O’Donnell, and David Witmer. Sum of squares lower
bounds for refuting any CSP. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors,
Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017,
Montreal, QC, Canada, June 19-23, 2017, pages 132–145. ACM, 2017.
[45] Jan Krajı́cek. Interpolation theorems, lower bounds for proof systems, and independence results
for bounded arithmetic. J. Symb. Log., 62(2):457–486, 1997.
[46] Claire Mathieu and Alistair Sinclair. Sherali-adams relaxations of the matching polytope. In
Michael Mitzenmacher, editor, Proceedings of the 41st Annual ACM Symposium on Theory ofComputing, STOC 2009, Bethesda, MD, USA, May 31 - June 2, 2009, pages 293–302. ACM,
2009.
[47] Ryan O’Donnell and Tselil Schramm. Sherali - adams strikes back. In Amir Shpilka, editor, 34th
Computational Complexity Conference, CCC 2019, July 18-20, 2019, New Brunswick, NJ, USA,volume 137 of LIPIcs, pages 8:1–8:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
[48] Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations.
J. Symb. Log., 62(3):981–998, 1997.
[49] Pavel Pudlák and Jirı́ Sgall. Algebraic models of computation and interpolation for algebraic
proof systems. In Paul Beam and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24,
1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science,
pages 279–295. DIMACS/AMS, 1996.
[50] Prasad Raghavendra and David Steurer. Integrality gaps for strong SDP relaxations of UNIQUEGAMES. In 50th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2009,
October 25-27, 2009, Atlanta, Georgia, USA, pages 575–585. IEEE Computer Society, 2009.

29

[51] Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Comb., 19(3):403–435,
1999.
[52] Alexander A Razborov. Unprovability of lower bounds on circuit size in certain fragments ofbounded arithmetic. Izvestiya: mathematics, 59(1):205, 1995.
[53] Robert Robere. Unified lower bounds for monotone computation. PhD thesis, University ofToronto (Canada), 2018.
[54] Robert Robere, Toniann Pitassi, Benjamin Rossman, and Stephen A. Cook. Exponential lower
bounds for monotone span programs. In Irit Dinur, editor, IEEE 57th Annual Symposium on
Foundations of Computer Science, FOCS 2016, pages 406–415. IEEE Computer Society, 2016.
[55] Thomas Rothvoß. Some 0/1 polytopes need exponential size extended formulations. Math. Program., 142(1-2):255–268, 2013.
[56] Thomas Rothvoss. The matching polytope has exponential extension complexity. J. ACM,
64(6):41:1–41:19, 2017.
[57] Grant Schoenebeck. Linear level lasserre lower bounds for certain k-csps. In 49th Annual IEEE
Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 593–602. IEEE Computer Society, 2008.
[58] Xiaodi Wu, Penghui Yao, and Henry S. Yuen. Raz-mckenzie simulation with the inner productgadget. Electron. Colloquium Comput. Complex., page 10, 2017.
[59] Mihalis Yannakakis. Expressing combinatorial optimization problems by linear programs. J.
Comput. Syst. Sci., 43(3):441–466, 1991.

30