TFNP Characterizations of Proof Systems and Monotone
Circuits
Sam Buss

Noah Fleming

Russell Impagliazzo

UCSD

Memorial University

UCSD

Abstract
Connections between proof complexity and circuit complexity have become major tools
for obtaining lower bounds in both areas. These connections, which take the form ofinterpolation theorems and lifting theorems, translate efficient proofs into small circuits
and vice versa, enabling tools from one area to be applied to the other.
Recently, the theory of TFNP has emerged as a unifying framework for these connections. For proof systems which admit such a connection there is a TFNP problem
which characterizes it: the class of problems which are black-box reducible to this TFNP
problem is equivalent to the set of tautologies which admit short proofs in this proof system. Such characterizations have resulted in proof complexity becoming one of the main
tools for analyzing black-box TFNP. Similarly, for certain models of monotone circuitry,
the class of functions that can be computed efficiently is equivalent to the total functions
that can be reduced to a certain TFNP problem via communication-efficient reduction.
Whenever a TFNP problem is characterized by both a proof system and a circuit model,
one immediately obtains an interpolation theorem. Similarly, the major lifting theorems
are between proof systems and circuit models which characterize the same TFNP problem. This suggests that TFNP could provide a roadmap for the development of further
interpolation theorems and lifting theorems.
In this paper we develop a systematic understanding of these connections by uncovering the exact conditions for such characterizations to occur. We show:– Every well-behaved proof system which can prove its own soundness (a reflection
principle) is characterized by a TFNP problem. Conversely, every TFNP problem
is characterized by a Cook-Reckhow proof system which proves its own soundness.
– Every well-behaved monotone circuit model which admits a universal family offunctions is characterized by a TFNP problem. Conversely, every TFNP problem
is characterized by a monotone circuit model with a universal family of functions.
As a proof of concept, we use this to uncover a characterization of Polynomial Calculus
and a dag-like variant of Sherali-Adams.

A preliminary version of this work appeared at the 14th Innovations in Theoretical Computer Science (ITCS).

1

Introduction

Recently, connections between proof complexity and monotone circuit complexity have been central toresolving long-standing open problems in a variety of areas. These connections take the form of:– Interpolation Theorems, which translate small proofs into efficient computations in an associatedmodel of monotone circuit [6, 17, 18, 21, 32, 37–39, 45, 47, 49].
– Query-to-Communication Lifting Theorems, which translate efficient monotone computations into
small proofs in an associated proof system [10, 15, 16, 23, 29–31, 36, 40, 43, 44, 48, 50].
Recently, the landscape of total functional NP (TFNP) has emerged as an organizing principle for connections between proof systems and models of monotone circuitry [13, 28] in the following sense. For manyof the proof systems which admit an interpolation theorem or lifting theorem there is a subclass of TFNP
which characterizes it: the set of theorems efficiently provable in this proof system is equivalent to thetotal functions contained within this class, in the black-box setting. This has resulted in proof complexity
becoming a major tool for proving black-box/oracle separations in TFNP. As well, the framework of TFNP
has provided a number of unique results for proof complexity, including complete tautologies for any proof
system admitting a TFNP-characterization, and intersection theorems showing that some proof systems are
the intersection several others.
An analogous phenomenon exists for circuit complexity. For many models of monotone computation,
the set of functions which can be computed efficiently is equivalent to the set of total search problems which
can be reduced to a complete problem for a corresponding TFNP subclass, via communication-efficient
reductions.
When a proof system and circuit model are characterized by the same TFNP subclass, then we immediately get an interpolation theorem! As well, the query-to-communication lifting theorems can be viewed
as constructing a query-efficient reduction to a particular TFNP problem out of a communication-efficient
reduction to that problem. This is exciting as it suggests that understanding when TFNP classes admit suchcharacterizations is a pathway for developing further connections between proof complexity and circuit
complexity.
In this paper we give exact conditions under which a proof system or monotone circuit model admits acharacterization by a TFNP subclass. For proof complexity, we show that every well-behaved1 proof system
which can prove its own soundness (a reflection principle) is characterized by a TFNP subclass — simply
the search problem associated with its reflection principle. This gives a recipe for constructing a TFNP
subclass which characterizes a given proof system, simply use the search problem for its reflection principle
as the complete problem! Conversely, we show that every TFNP class which has a complete problem gives
rise to a well-behaved proof system which proves its own soundness and which is closed under decision
tree reductions. Furthermore, this result is constructive: for every TFNP subclass with a complete problem,
we give a proof system which it characterizes. As an example, we provide a TFNP characterization of the
Polynomial Calculus, as well as several variants, answering a question from [27], and show that it can prove
its own soundness. For circuit complexity, we show that every well-behaved model of monotone circuitry
which admits a universal family of functions is characterized by a TFNP class. Conversely, every TFNP
class with a complete problem gives rise to a monotone circuit model with a universal problem.
1
We will say that a proof system of monotone circuit model is well-behaved if it satisfies some minor technical conditions
discussed in subsection 1.2.

1

1.1

Overview: Connections Proof Complexity, and Circuit Complexity, and TFNP

The connections between proof systems and monotone circuit models can be understood as relating thecomplexity of two families of total search problems, whose complexity characterizes proof and circuit complexity respectively.
– False Clause. S EARCHF for an unsatisfiable CNF formula F = C1 ∧ · · · ∧ Cm : given an assignmentx ∈ {0, 1}n output the index i ∈ [m] of a clause such that Ci (x) = 0.
– Monotone Karchmer-Wigderson. M KWf for a monotone boolean function f : given x, y ∈ {0, 1}nsuch that f (x) = 1 and f (y) = 0 output i ∈ [n] such that xi > yi .
The theory of TFNP considers the total search problems for which solutions can be efficiently verified, suchas S EARCH and M KW. There is believed to be no complete problem for TFNP [46], and therefore muchof the work on this subject has focused on identifying subclasses which do admit complete problems. This
has resulted in a rich landscape of classes which capture a wide variety of important problems in a rangeof areas including cryptography, economics, game theory, circuit complexity, and proof complexity. These
classes are typically defined as everything that can be efficiently reduced to a certain existence principle
on an exponential-size universe. For example, PPA is the class of search problems that can be reduced
to finding an unmatched vertex in a perfect matching on a graph with an odd (exponential) number ofvertices. These exponential size objects are given in a white-box fashion: they are represented succinctly asa polynomial-size circuit which can be queried to obtain each bit of the input.
The principal goal in the study of TFNP is to understand how these subclasses relate. However, aseparation between any pair of subclasses would imply P ̸= NP. Instead, a line of work has sought toprovide evidence of their relationships by proving black-box separations. As opposed to the white-box
setting, we are now limited to accessing the defining circuit via an oracle. We may query the oracle foreach bit of the input, but we may no longer observe its representing circuit (nor are we guaranteed that a
representing circuit exists for this instance).
Black-Box TFNP and Proof Complexity. Beginning with [3], proof complexity has become a major tool
for proving black-box TFNP separations. In fact, black-box TFNP — denoted TFNPdt — can be viewed
as the study of the false clause search problem. Every TFNPdt problem is equivalent to S EARCHF forsome unsatisfiable CNF formula F . Using this connection, Göös et al. [28] observed that many prominent
TFNPdt subclasses are characterized by associated proof systems in the sense that the unsatisfiable formulasthat are efficiently provable in that proof system are exactly the problems S EARCHF that are reducible to thethe complete problem for that TFNPdt subclass. This has led to the characterization of many well-studied
TFNPdt subclasses:– FPdt = TreeRes [42].
– PLSdt = Res [9].
– PPAdt = F2 -NS [28].
– PPAdt
q = Fq -NS for any prime q [34]
– PPADdt = unary-NS [27].

– PPADSdt = unary-SA [27].
– EOPLdt = RevResT [27].
– SOPLdt = RevRes [27].
– CPLSdt = Res(polylog) [12]Via these characterizations, separations between these proof systems translate into separations between
their corresponding TFNPdt subclasses. This has resulted in a complete picture of how the prominent
TFNPdt subclasses relate [2, 7, 19, 27, 28].
This relationship has led to a number of striking results for proof complexity as well. These include:2

– Complete Problems: Any proof system P which is characterized by a TFNPdt subclass has a complete formula F , in the following sense: if a proof system can efficiently prove F (and can simulate
decision-tree reductions) then that proof system can efficiently simulate P. This complete tautology
F states that a complete problem for this subclass is total. Previously, complete problems were known
only for strong proof systems which could prove their own reflection principle.
– Intersection Theorems: Proof systems which can efficiently prove a formula iff that formula has shortproofs in several other proof systems [27, 33, 41].
– Coefficient Separations: Separations between the complexity of certain algebraic proof system when
their coefficients are represented in unary versus binary [27].
Despite all of this, there are still many important TFNPdt subclasses — such as PPPdt — which haveevaded characterization by a proof system, and there are many important proof systems for which no corresponding TFNPdt problem is known.
Communication TFNP and Monotone Circuit Complexity. Karchmer and Wigderson [35] showed thatthe monotone formula complexity of any monotone function f is equal to the communication complexityof M KWf . Building on this, Razborov [49] considered reductions between black-box TFNP classes where
one measures the amount of communication needed to perform the reduction (for some suitable partitionof the input), denoted TFNPcc , and showed that PLScc -complete problems characterize monotone circuit
complexity. There is good reason for this: analogously to how TFNPdt is the study of the false clausesearch problem, TFNPcc can be viewed as the study of the monotone Karchmer-Wigderson game. Indeed,
every R ∈ TFNPcc is equivalent to M KWf (over the same partition of the variables) for some associatedmonotone function f [22, 28].
Following these results, a number of TFNPcc sub-classes have been characterized by models of monotone circuits [18, 28]. However, there remain many important circuit models for which no TFNPcc characterization is known.
A Theory of Interpolation and Lifting Theorems. As we have just discussed, certain proof systems andmonotone circuit models are characterized by dt and cc TFNP subclasses. Göös et al. [28] observed thatin all known examples of TFNP sub-class which admit both a characterization by a proof system and amonotone circuit, there exists both an interpolation theorems and query-to-communication lifting theorem
between that proof system and monotone circuit. This is to be expected, as a key component of bothinterpolation and query-to-communication lifting theorems proceeds by relating S EARCHF to M KWf for
associated pairs (F, f ). In fact, it is not difficult to see that whenever a TFNP class admits a characterization
by both a proof system and a monotone circuit model then there is an interpolation theorem between them— this follows immediately by the observation that communication protocols can simulate decision trees!
Thus, the landscape of TFNP, together with characterizations of TFNP subclasses by proofs and circuits,
appears to provide a roadmap for potential interpolation and query-to-communication lifting theorems.

1.2

Our Results

Our first main result is an exact characterization of when a proof system admits a characterization by a
TFNPdt class. We show that this occurs for any proof system P which meets the following two criteria:i) Proves its own soundness. P can prove that P -proofs are sound. That is, P has small proofs of areflection principle about itself, encoded in an efficiently-verifiable manner.
3ii) Closure under decision-tree reductions. Whenever there is a small P -proof of a formula H, andS EARCHF efficiently reduces to S EARCHH , then there is also a small P -proof of F .
Conversely, we show that every syntactic TFNPdt subclass (meaning that it has a complete problem) has a
proof system which characterizes it. Furthermore, this proof system satisfies conditions (i) and (ii).
Theorem 1 (Informal). The following hold:– For any syntactic TFNPdt subclass C there is a proof system P satisfying (i) and (ii), such that
C characterizes P : P has short proofs of F iff S EARCHF is efficiently reducible to a C-complete
problem.
– For any proof system P which satisfies (i) and (ii) there is a TFNPdt subclass which characterizes P .
It follows that the false-clause search problem for the reflection principle provides a somewhat a somewhat systematic way of generating a TFNPdt problem which characterizes that proof system. As an example, we introduce a new TFNP subclass, IND-PPA, which characterizes the F2 -Polynomial Calculus proof
system. This class contains problems which can be solved by inductive parity arguments. Furthermore, weshow that the F2 -Polynomial Calculus can prove its own soundness.
Theorem 2 (Informal). IND-PPAdt characterizes F2 -PC. As well, F2 -PC has small proofs of an efficiently
verifiable reflection principle about itself.
As a bonus, we show that the method we use to discover IND-PPA can also be used to discover TFNPdt
subclasses which characterize the dynamic versions of all static proof systems for which we currently have
TFNP characterizations. In subsection 3.4, we provide TFNPdt subclasses for the Fq -Polynomial Calculus,
the unary Polynomial Calculus, and unary dag-like Sherali-Adams. Finally, we observe that these characterizations hold the PCR systems as well. Indeed, from the perspective of TFNP, there is no difference
between the standard and dual-variable encodings of CNF formulas (Observation 14).
Our second main result is an exact characterization of the conditions under which models of monotone
circuitry admit characterization by a TFNPcc subclass. We formalize the concept of a monotone circuit
model as a monotone partial function complexity measure (mpc) — a mapping of partial monotone functions
to non-negative integers. We show that a TFNPcc subclass is characterized by a mpc iff the mpc meets thefollowing criteria:i) Closure under low-depth reductions: Whenever f is a partial function and h is computable by adepth-d monotone Boolean circuit then mpc(f ◦ h) is only polynomially larger in 2d and mpc(f ).
ii) Admits a universal family: A family of functions Fm such that whenever mpc(g) ≤ m for a monotone
partial function g, there is a string zg so that F (x ◦ zg ) solves g(x).
Theorem 3 (Informal). Let mpc be a complexity measure. There is C ⊆ TFNPcc such that C cc characterizes
mpc iff mpc satisfies (i) and (ii).
Finally, we investigate whether this characterization can be extended from partial function complexity
measures to total function measures. Since complexity measures on total functions induce measures onpartial functions, this allows us to give a general condition under which a complexity measure on total
functions has a TFNPcc characterization (Theorem 27) by applying Theorem 3.

4

A Note on the Provability of Reflection Principles. Theorem 1 establishes that the property of P having
short proofs of a reflection principle about itself is closely related to having a TFNPdt characterization of P .
The reflection principle for propositional proof systems has already been studied in prior work. In particular,
Cook [11] showed that extended Frege (eF) has short proofs its consistency statements, and Buss [8] showedthat Frege (F) has short proofs of its consistency statements. From their results, it follows readily that bothproof systems, extended Frege and Frege, have short (polynomial size) proofs of their reflection principles.
It is also well-known that the extended Frege and Frege proof systems can be characterized as very strong
TFNPdt classes characterizable in terms of second-order theories of bounded arithmetic, see [5]. Analogous
results were obtained for even stronger propositional proof systems by [25]. On the other hand, Garlik [24]showed that resolution requires exponential length for refutations of (a particular “leveled” version of) its
reflection principle, and Atserias-Müller [1] gave exponential lower bounds on resolution refutations of a
relativized reflection principle.
Theorem 1 requires that the proof system P has short proofs of a reflection principle about itself. There
are two main differences between our encodings of the reflection principle and previous ones which haveappeared in the literature. The first is that our reflection principles are parameterized by a complexity parameter c (see Section 2) rather than the typical size parameter. The complexity parameter measures boththe logarithm of the size and width/degree of the proof simultaneously. The second is that the reflection
principle must be efficiently verifiable, meaning that an error in the purported proof in the can always beverified by examining in a small number of bits. Thus for example, our results show that polylog(n)-width
Resolution can prove its own reflection principle, which we show explicitly in Appendix A. As well, thismeans that the bound of Garlik [24] does not contradict our results.

2

Proof Complexity and Black-Box TFNP

We begin by defining black-box TFNP. A total search problem is a sequence of relations Rn ⊆ {0, 1}n ×
On , one for each n ∈ N, which is total — for each x ∈ {0, 1}n there is i ∈ On such that (x, i) ∈ Rn .
A total search problem is in TFNPdt if its solutions are verifiable: for each n sufficiently large and everyi ∈ On there is a polylog(n)-depth decision tree Vi such that
Vi (x) = 1 ⇐⇒ (x, i) ∈ Rn .
Note that if R ∈ TFNPdt , then log |On | ≤ polylog(n) as we must be able efficiently output a solution.
Henceforth, for readability, we will suppress the subscript n.
A decision tree reduction from Q ∈ {0, 1}n × OQ to R ⊆ {0, 1}s × OR is a set of decision trees
Ti : {0, 1}n → {0, 1} for i ∈ [s] and Tjo : {0, 1}n → OQ for j ∈ O such that for any x ∈ {0, 1}n ,((T1 (x), . . . , Ts (x), j) ∈ R =⇒ (x, Tjo (x)) ∈ Q.
That is, the Ti ’s map inputs to from Q to R, and the Tjo ’s maps solutions to R back to solutions to Q. The
depth of the reduction is d, the maximum depth of any of the decision trees involved, and the size is s. The
complexity of the reduction is log s + d and the complexity of reducing Q to R is the minimum complexityof any decision tree reduction from Q to R. We say that Q reduces to R, denoted Q ≤dt R, if there is apolylog(n)-complexity reduction from Q to R for all sufficiently large n. We say that Q =dt R if Q ≤dt R
and R ≤dt Q.
The intimate connection between black-box TFNP and proof complexity is summarized by the following claim from [27, 28]. Recall that the width of a CNF formula is the maximum number of literals in any
clause of the formula.
5

Claim 4. If R ∈ TFNPdt then there is an unsatisfiable polylog(n)-width CNF F such that R =dt S EARCHF .
Proof. Let R ⊆ {0, 1}n × O be a search problem in TFNPdt . We build a CNF formula F asserting that R
is not total.
As R ∈ TFNPdt , there are decision trees Vi for each i ∈ O such that Vi (x) = 1 iff (x, i) ∈ R. For each
Vi , we build a CNF formula saying that i is not a solution to R. Say that a root-to-leaf path in Vi is a 1-path
if its leaf is labelled 1. If we follow a 1-path of Vi on input x then this path verifies that (x, i) ∈ R. Thinkingof each path in this decision tree as a conjunction of the literals which appear along it, we define the CNF
^
Ci :=
¬p
1-path p∈Vi

whichV
states that no input x ∈ {0, 1}n outputs solution i. We state that R is not total with the CNF formula
F := i∈O Ci . As R ∈ TFNPdt the depth of each Vi , and hence the width of F is at most polylog(n).
To reduce R to S EARCHF , let Ti (x) := xi and Tjo (x) := i if clause Cj of F is one of the clauses of
Ci . Conversely, we can reduce S EARCHF to R by letting Ti (x) := xi and setting Tio to be the decision tree
which queries Vi and outputs the index of the clause ¬p for the root-to-leaf path p followed in Vi .
The upshot is that black-box TFNP is exactly the study of the false clause search problem! Therefore,
without loss of generality, we focus on the search problems S EARCHF associated with R ∈ TFNPdt insteadof R itself. Using this connection, Göös et al. [28] observed that many important proof systems are characterized by an associated TFNPdt class in the sense that the CNF formulas F that are efficiently provablein that proof system are exactly the search problems S EARCHF that are efficiently reducible to this TFNPdt
class.
TFNP Characterizations. The known characterizations of proof systems by TFNPdt problems are interms of a somewhat non-standard, but very natural, complexity parameter. For a proof system P and
unsatisfiable CNF formula F let the complexity required by P to prove F be
P (F ) := min{width(Π) + log size(Π) : Π is a P -proof of F },where width denotes an associated width measure of the proof system. For Nullstellensatz and SheraliAdams, this width measure is the maximum degree of any polynomial in their proofs, while for Resolution,
width is the maximum number of variables in any clause in a proof. While nonstandard, this complexity
parameter is very natural. Indeed, all of the query-to-communication lifting theorems referenced in the
introduction lift lower bounds on a complexity parameter for some proof system to lower bounds on somemonotone circuit model.
We say that a TFNPdt subclass C characterizes a proof system P ifno
C dt = S EARCHF : P (F ) = polylog(n) .
That is, the false-clause search problems (and hence by Claim 4, the problems in C) are exactly the polylog(n)width CNF formulas provable in P . This is reflexive and so we also say that P characterizes C.
In this section we give necessary and sufficient conditions for such a characterization to occur. The first
condition is that the proof system proves (an efficiently verifiable variant of) its reflection principle.

6

2.1

What is a Reflection Principle?

The first condition of Theorem 1 is that the proof system must be able to prove its own soundness. A
reflection principle Ref P for a proof system P states that P -proofs are sound; it says that if Π is a P -proofof a CNF formula H then H must be unsatisfiable. This is formalized with variables encoding a CNF H,
a proof Π, and a truth assignment α to H. The formula (falsely) asserts that Π is a P -proof of H and αsatisfies H,
Proof(H, Π) ∧ Sat(H, α).
We say that a reflection principle is efficiently verifiable if it is encoded as a low-width CNF formula. In
this case, solutions to the false clause search problem for the reflection principle (also known as the wrong
proof problem [4, 26]) can be efficiently verified.
For a proof system P there are many ways to encode its proofs, with the choice of the encoding potentially affecting the complexity of proving the associated reflection principle. Rather than worrying about
the particular encoding, we will instead define one reflection principle for each efficiently verifiable way of
encoding P -proofs, which we call a verification procedure. Recall that the complexity c of a proof is always
an upper bound on the width of the CNF being proven. For this reason, and to simplify notation, we willbound the width of the CNF H by c.
Verification Procedure. A verification procedure V for a proof system P is a mapping of tuples (n, m, c)
to CNF formulas that generically encodes complexity-c (or O(c)) P -proofs of n-variate CNF formulas withm clauses of width at most c. Specifically, the CNF formula Vn,m,c has two sets of variables H, Π, suchthat:
– An assignment to the variables H := {Ci,j : i ∈ [m], j ∈ [c]} specifies a CNF formula with mclauses over n variables, where Ci,j ∈ [2n] is the index of the j th literal of the ith clause of H; if
Ci,j ≤ n then it specifies a positive literal, and otherwise it specifies a negative literal. Note that we
can always specify clauses of smaller width by repeating the same literal, and specify a formula withfew clauses by repeating the same clause multiple times.
– An assignment to the variables Π specifies a (purported) P -proof of H, such that any purported errorin Π can be verified by looking at the assignment to at most poly-logarithmically many variables ofVn,m,c .
– The CNF formula Vn,m,c has 2Θ(c) many variables.
As the complexity parameter c bounds the logarithm of the size of the proof, and the number of variables is
exponential in Θ(c) by the third condition, the second condition ensures that Vn,m,c has width poly(c) andcan be verified by looking at poly(c)-many variables. The third condition can be relaxed, and larger numbersof variables can be tolerated at the cost of worse bounds in Theorem 10. We give a concrete example of averification procedure for the Polynomial Calculus proof system in Section 3.
For concreteness, we have fixed a particular encoding of H in order to avoid pathological codings; e.g.,ones in which a SAT oracle is used to decide whether the formula is satisfiable. Since we allow arbitrarycodings of proofs, this will be robust under different encodings of CNFs as long as they are polynomial-time
computable from ours.
We can now define a reflection principle for any proof system based on a verification procedure.

7

Reflection Principle. Let P be a proof system and V be a verification procedure for P -proofs. The reflection principle Ref P,V associated with (P, V ) is the unsatisfiable formula
Proof nH ,mH ,c (H, Π) ∧ SatnH ,mH ,c (H, α),where H is a CNF formula over nH variables with mH clauses of width at most c. The j th literal (if any)of the ith clause of H is specified by a vector Ci,j of log 2nH -many Boolean variables, and– Proof nH ,mH ,c (H, Π) := VnH ,mH ,c (H, Π).
– SatnH ,mH ,(d,nF ) (H, α) is the formula stating that α is a satisfying assignment for H:∀i ∈ [mH ], ∃j ∈ [c][[Ci,j = xk ]] ∧ αk
∨ [[Ci,j = ¬xk ]] ∧ ¬αk ,where [[p = ℓ]] is the indicator function of p being equal to ℓ.
Sat can be encoded as a CNF formula of width O(c log nH ) and size mH exp(O(c log nH )). To see this,construct the following decision tree Ti for each i ∈ [mH ]: for each j ∈ [c], query the 2nH -ary variables
Ci,j to determine the literal ℓk or for Ci,j and then query the value of αk ∈ {0, 1}. Label this leaf with 1
if αk agrees with the literal specified by Ci,j and 0 otherwise. Using this, we build the width-O(c log nH )formula^^Sat :=¬p.
i∈[mH ] 1-path p∈Ti
For simplicity of notation, we will drop the subscripts P, V from Ref when the proof system and verification procedure is clear. One technicality is that TFNPdt problems have one instance for each numberof variables n; to ensure that this is the case for Ref we could use a pairing function on the multiple sets
of variables for Ref, however we are going to ignore this detail. Each reflection principle gives rise to a
TFNPdt problem. Indeed, by construction Ref is verifiable by observing polylog(n) many bits, where n is
the total number of variables.

2.2

Conditions for a TFNP Characterization

The first necessary condition for a proof system to admit a characterization by a TFNPdt problem willbe that the proof system must efficiently prove a reflection principle about itself. The second necessary
condition is that the proof system must be closed under substitutions of decision trees for variables, as
TFNPdt subclasses are closed under such reductions.
Closure under Decision Tree Reductions. A proof system P is closed under decision tree reductions
if whenever there is a P -proof of complexity c of an unsatisfiable formula F , and S EARCHH reduces to
S EARCHF by depth-d decision trees, then there is a P -proof of H of complexity poly(cd).
In all of the proof systems which are known to admit characterization by a TFNPdt problem, closure
under decision tree reductions takes the form of directly substituting (an appropriate encoding of) decision
trees into the proofs. For example, if S EARCHH reduces to S EARCHF and we have a Resolution proof of F ,then we can obtain a Resolution proof of H by replacing each variable in the proof of F by the (CNF formula
corresponding to the negation of the accepting paths of) corresponding decision tree from the reduction. If
8these are depth d decision trees, and the Resolution proof has width w and size s, then after substitution we
have a Resolution proof of width at most dw and size at most s exp(dw). Hence, the proof width and size
remain poly-logarithmic and quasi-polynomial, respectively, if d, w, log s = polylog(n).
We are now ready to prove Theorem 1, which we state formally as follows.
Theorem 5. The following hold:i) For any syntactic TFNPdt subclass C there is a proof system P such that C characterizes P . Furthermore, P is closed under decision tree reductions and there is a reflection principle Ref P for P suchthat P (Ref P ) ≤ polylog(n).
ii) For any proof system P which is closed under decision tree reductions and for which there is areflection principle Ref P of which P has polylog(n)-complexity proofs, there is a TFNPdt subclass C
which characterizes P .
In fact, we prove a tighter characterization over the following two subsections, from which Theorem 5
will follow. Part (i) is proven in Theorem 7, with the “furthermore” part proven in Theorem 9, and part (ii)is proven in Theorem 10.

2.3

A Proof System for any TFNP Problem

We show how to construct, from any TFNPdt subclass with a complete problem R, a proof system whichcharacterizes it. The key insight is that one can view decision tree reductions to R as proofs — indeed, thecorrectness of a reduction can be verified efficiently! This efficient verifiability can then combined with thecharacterization of problems in TFNPdt by instances of the false-clause search problem in order to obtaina proof system for UNSAT. More concretely, let F = {Fn }n∈N be the unsatisfiable CNF formula suchthat S EARCHF is equivalent to R. A PF -proof Π will consist of an unsatisfiable CNF formula H consistsof a decision-tree reduction from S EARCHH to S EARCHF . In order to define this formally, we will use thefollowing notion of a reduction between CNF formulas.
Suppose that C is a clause over n variables and T = {Ti }i∈[n] is a sequence of depth-d decision trees,
where Ti : {0, 1}s → {0, 1}. We write C(T ) to denote the CNF formula obtained by substituting thedecision trees Ti for each i ∈ Vars(C) and rewriting the result as a CNF formula. Formally, C(T ) is formedby creating a decision tree T C that sequentially runs the trees Ti for each variable xi used in C. Say that apath p in T C is violating if corresponds to queried trees Ti outputting an assignment which falsifies C; thatis, p satisfies the constraint^^[[Ti (p) = 0]] ∧[[Ti (p) = 1]],i∈Vars− (C)i∈Vars+ (C)where Vars+ (C), Vars− (C) are the indices variables which occur positively and negatively in C. That is,C(T (p)) = 0 for every violating path. Label the leaves of the violating paths p ∈ T C by 0, and label theremaining leaves by 1. Then, C(T ) is the CNF formula^C(T ) :={¬p : p is a violating path of T C },where a path p is identified with the conjunction of the literals set true along the path, and ¬p is its negation.
C(T ) asserts that C is not falsified. Another way to see this is to say that a root-to-leaf path in Ti is a9t ∈ {0, 1}-path if it ends at a leaf labelled t. Then^_
C(T ) := ¬+i∈Vars (C)p ∧

0-path p∈Ti^
i∈Vars− (C)



_


p ,

1-path p∈Ti

stating that we do not follow path in the trees Ti for i ∈ Vars(C) which falsifies C.
Reductions Between CNF Formulas. Say that a CNF formula H on nH variables and mH clauses
reduces to an unsatisfiable F = C1 ∧ · · · ∧ Cm over n variables via depth-d decision trees if there is a
depth-d decision tree reduction T = {Ti }i∈n where Ti : {0, 1}nH → {0, 1}, and T o = {Tio }i∈[m] with
Tio : {0, 1}nH → [mH ] from S EARCHH to S EARCHF . We can interpret this syntactically as follows. Define
the reduced formula FH as the CNF formula
^ ^
FH :=
Ci (T ) ∨ ¬p,i∈[m] p∈Tio

where p ∈ Tio denotes that p ranges over all root-to-leaf paths of Tio . Since Ci (T ) is a CNF, FH is readily
written as a CNF by distributing ¬p into Ci (T ). Then, since (T, T o ) is a valid reduction, each clause of
Ci (T ) ∨ ¬p must either be tautological (contains a literal and its negation) or be a weakening of the clauseof H indexed by the label of the leaf reached by taking the path p in Tio .
Letting the width and size of a CNF formula be the maximum number of literals in any clause, and thenumber of clauses in the formula respectively, the following hold:– width(FH ) ≤ d · width(F ),– size(FH ) ≤ size(F ) · 2d·width(F ) .
In particular, if F is a quasi-polynomial size, polylog(n)-width CNF formula and d = polylog(n), then FH
has quasi-polynomial size and polylog(n)-width.
Observe that a depth-d decision tree reduction of S EARCHH to S EARCHF introduces a new false clausesearch problem S EARCHFH which is a refinement of S EARCHH . Clearly, if F is unsatisfiable, then so is FH
and consequently also H is unsatisfiable.
Canonical Proof System. Let S EARCHF ∈ TFNPdt . The canonical proof system PF for S EARCHF proves
an unsatisfiable CNF formula H on nH variables if H is reducible to an instance of F on some n variables.
A PF -proof Π consists of the decision trees T = {Ti }i∈[n] and T o = {Tio }i∈[m] of the reduction, along withthe reduced formula FH .
The size of Π is the number of bits needed to write down the proof Π = (T, T o , FH ), which is polynomially related to s(FH ), and the width is w(FH ), which is polynomially related to the maximum depth
among any of the decision trees in T, T o . The complexity of proving an unsatisfiable CNF formula H is thenthe minimum over all PF -proofs of H,
PF (H) := min{width(Π) + log size(Π) : Π is a PF -proof of H}.
This proof system is sound as any substitution of an unsatisfiable CNF formula is also unsatisfiable, and
it is complete as S EARCHH for any unsatisfiable CNF formula H can be solved by a decision tree of depth
n. The following claim shows that PF is polynomial-time verifiable.

10Claim 6. There is a polynomial-time Turing Machine M such that M (H, Π) = 1 if and only if Π is a
PF -proof of H.
Proof. Let (T, T o , FH ) be a PF -proof of an unsatisfiable CNF formula H. Our verifier M checks thefollowing conditions:– FH is the CNF formula obtained by the reduction (T, T o ) applied to F .
– Each clause of FH is either a weakening of a clause in H or tautological, meaning that it contains avariable and its negation.
As the number of clauses of FH is bounded above by the size of the proof, this can be done in polynomialtime in the size of the proof.
Finally, note that the canonical proof system PF is closed under decision tree reductions.
The next theorem states that PF has a short proof of H iff S EARCHH efficiently reduces to S EARCHF .
This is almost immediate from the definitions.
Theorem 7. If S EARCHF , S EARCHH ∈ TFNPdt then S EARCHH ≤dt S EARCHF iff PF (H) ≤ polylog(n).
This theorem establishes part of (i) in Theorem 7; the “furthermore” part is proven in the following
subsection. This theorem follows from the next lemma by setting c ≤ polylog(n).
Lemma 8. Let S EARCHF ∈ TFNPdt . For any unsatisfiable CNF formula H, there is a complexity creduction from S EARCHH to S EARCHF iff PF (H) ≤ c · polylog(n).
Proof. Suppose that there is a complexity c reduction from S EARCHH to S EARCHF . Letting T = {Ti }i∈[n]
and T o = {Tjo }j∈[m] be the decision trees in this reduction, construct the CNF formula FH as above. Notethat since S EARCHF ∈ TFNPdt , F contains at most quasipolynomially-many clauses and has width at
most polylog(n). Hence size(FH ) ≤ exp(c · polylog(n)) and width(FH ) = O(polylog(n)), and PF (H) =c · polylog(n).
It remains to verify that (FH , T, T o ) is a PF -proof of H. Fix any clause L of FH . L belongs to some
CNF formula Ci (T ) ∨ ¬p for some clause Ci of F and root-to-leaf p of Tio . If L is tautological, then we aredone. Otherwise we will argue that it is a weakening of a clause of H. Fix any assignment which falsifies L.
As L is a clause of Ci (T ) ∨ ¬p it has ¬p as a sub-clause, and so p(x) is satisfied. Thus, by the correctnessof the reduction from S EARCHH to S EARCHF , the Tio (x)th clause D of H must be falsified by T (x) (asTio (x) is a solution to S EARCHH ). Hence, we have that ¬L =⇒ ¬D and so D is a weakening of L.
For the converse direction, suppose that there is a proof (T, T o , FH ) of H in PF . We claim that (T, T o )constitutes a reduction from S EARCHH to S EARCHF . To see this, fix any input x to S EARCHH . As F isunsatisfiable, T (x) falsifies some clause Ci of F , and x follows some root-to-leaf path p in Tio . Hence, xfalsifies some clause L in the sub-formula Ci (T (x)) ∨ ¬p(x) of FH . As FH is a proof of H, and x follows
path p in Tio (x), L must be a weakening of clause Tio (p) = Tio (x) of H. Thus, the Tio (x)th clause of H isfalsifies on input x and we conclude that (x, Tio (x)) ∈ S EARCHH .
Finally, let c be the complexity of this proof. Then, each decision tree in (T, T o ) has depth at most c andthere are at most 2c of them. Hence, this is a complexity c reduction.

11

2.4

Canonical Proof Systems Prove their own Soundness

In this section we define a natural formulation of the reflection principle for any canonical proof system P
by defining a verification procedure for its proofs. Then, we show that P can prove this encoding of its
reflection principle.
To construct this verification procedure we must define a CNF formula which generically encodes any
complexity-c P -proof in the sense that all complexity-c proofs can be recovered from variable instantiationsof this formula. As proofs in a canonical proof system are decision tree reductions, the following notion of ageneric decision tree will be useful. One should think of a generic decision tree as a template for a decision
tree, such that any decision tree of depth d can be recovered from it by correctly instantiating its variables.
Generic Decision Tree. Let O be a set and z1 , . . . , zn be Boolean variables. A generic n-ary decision
tree T of depth d specifying a decision trees over the variables ⃗z with output in O is the following complete
binary tree.
– Non-leaves. For each non-leaf vertex v of T , the left outgoing edge is labelled 0 and the right outgoingedge is labelled 1. The vertex v is labelled by an n-ary variable xv .
– Leaves. Each leaf ℓ is labelled with an |O|-ary variable xℓ .
An assignment to the variables of a generic n-ary decision tree specifies a decision tree over the variables z1 , . . . , zn as follows. For each vertex v, the assignment to xv specifies the z-variable which should bequeried at vertex v. For example, if xv = i then v is labelled by zi . Similarly, for each leaf ℓ, the assignment
to xℓ specifies the element o ∈ O which is the outcome of the decision tree at this leaf. For any root-to-leaf
path p ∈ T , let Lits(p) be z-literals named by this root-to-leaf path.
A generic n-ary decision tree of depth d can be used to specify any decision tree T of depth at most d bynaming the index of the variable queried at each vertex v using the xv variables. If T not a complete binary
tree then in order to shorten a root-to-leaf path, we can name the same variable repeatedly along this path.
For example, if p is a root-to-leaf path in T of depth 1, involving only a single variable zi , then for for every
v in the sub-tree rooted at the leaf of p in T , we set xv = i.
A generic n-ary decision tree may be converted into a generic decision tree T over binary variables
by the following recursive process (see Figure 1): beginning at the root of T . Let v be the current nonleaf vertex. Replace each xv by (log n + 1)-many variables xv = [xv1 , . . . , xvlog n , sv ], where sv is a sign
bit indicating the polarity of variable xv . Replace v by a depth-log n + 1 complete binary tree Tv which
sequentially queries xv1 , . . . , xvlog n to obtain the value variable xv ∈ [n] and then the sign bit sv to determine
whether the variable indexed by xv should be positive or negative. If v had left and right children u and w
in T , then at each leaf of Tv where sv = 0 we recurse on the child u and at leaves where sv = 1 we recurseon v. At each leaf ℓ we replace xℓ by log |O|-many variables, replace ℓ with a binary tree querying thesevariables, and label each leaf with the outcome in O.
Verification Procedure for PF . Fix some S EARCHF ∈ TFNPdt . We define a verification procedure
V = VnH ,mH ,(d,nF ) for PF , which encodes a complexity c = poly(d, log nF ) PF -proof Π of a CNF formulaH on nH variables and mH clauses as follows. The proof Π is specified by nF -many depth-d genericdecision trees T1 , . . . , TnF which specify decision trees over the variables of H with output in {0, 1} andmF depth-d generic decision trees T1o , . . . , Tmo F which specify decision trees over the variables of H with
output in [mH ]. The variables of V will be
12

⃗xu
xu

su

0

1

xv
0
xℓ1

xw
1

0

xℓ2

xℓ3

1
xℓ4

⃗xv

⃗xw

sv

sw

⃗xℓ1

⃗xℓ2

⃗xℓ3

⃗xℓ4

Figure 1: A generic n-ary decision tree (left) and its corresponding generic decision tree (right).
– {Ci,j : i ∈ [mH ], j ∈ [c]}, where Ci,j ∈ [2nH ] (encoded by binary variables) names the j th literal in
the ith clause of H.
– xv for each vertex v of Ti , Tjo where xv names the variable of H being queried at vertex v or if v is aleaf, is either a boolean variable if v is from Ti or names a clauses of H if it belongs to Tjo .
The constraints of the CNF formula V will enforce that each clause of the reduced CNF formula FH is aweakening of a clause of H. In particular, the constraints will assert that for each clause Ci of F = FnF androot-to-leaf path p ∈ Tio , the clauses of Ci (T ) ∨ ¬p are a weakening of the Tio (p)th clause of H.
The CNF formula Ci (T ) is formed as before, except that we now query the variables of the genericdecision tree. In particular, we create a stacked decision tree T Ci formed by sequentially running the trees(j) (j)(j)
Ti for each i ∈ Vars(Ci ), querying the variables xv , sv , and xℓ of Ti . For any root-to-leaf path p in T Ci
(j)
let {xℓ }j∈[Vars(Ci )] be the leaf variables queried along p — these determine the assignment to clause Ci .
Say that a path p is violating if p satisfies
^
^
(j)
(j)
[[xℓ = 0]] ∧[[xℓ = 1]],j∈Vars+ (Ci )j∈Vars− (Ci )where Vars+ (Ci ), Vars− (Ci ) are the variables which occur positively and negatively in Ci . That is, p isviolating if it corresponds to an assignment which falsifies the clause Ci . Then the CNF formula^
Ci (T ) :=¬p̂
violating p̂∈T Ci

The constraints of V enforce that each clause ¬p̂ ∨ ¬p of^^
Ci (T ) ∨ ¬p =
p∈Tio

^

¬p̂ ∨ ¬p

violating p̂∈T Ci p∈Tio

is a weakening of the Tio (p)th -clause of H. Let LitsH (p) be the literals of H named along the a path pof one of these generic decision trees. As well, let Hk be the decision tree which sequentially queries thevariables Ck,j ∈ [2nH ] for each j ∈ [c]. Each root-to-leaf path p∗ in this decision tree determines the13variables which appear in the k th clause of H. Say that p∗ is bad for a pair of paths (p̂, p) ∈ Tio × T Ci if
LitsH (p∗ ) ̸⊆ LitsH (p̂ ∧ p), meaning that Ci (T ) ∨ ¬p are not a weakening of the k th clause of H.
The constraint corresponding to Ci (T ) ∨ ¬p̂ are^^^(¬p̂ ∨ ¬p ∨ ¬p∗ )Wi :=violating p̂∈T Ci p∈Tio p∗ ∈HTio (p) bad for (p,p̂)

stating that if we follow path p̂ of T Ci and path p of Tio then the clause Ci (T ) ∨ ¬p̂ of FH is a weakeningof the Tio (p)th clause of H. The CNF formula^
V (H, Π) :=
Wi ,
i∈mF

is satisfied only when Π is a valid PF -proof of H. As each generic decision tree has depth at mostd, F has width O(polylog(nF ), and H has width at most c, this is a CNF formula of width at mostpolylog(nF )(d log(nH ) + log mH ) + c log nH .
Canonical Reflection Principle. Let S EARCHF ∈ TFNPdt . We define its canonical reflection principle
Ref F to be the conjunction
Proof nH ,mH ,(d,nF ) (H, Π) ∧ SatnH ,mH ,(d,nF ) (H, α),where Sat is defined as in the definition of the reflection principle and Proof := VnPH ,mH ,(d,nF ) . In total, thisis a CNF formula of width d log nF + log mH + c log nH over n = mF 2d+1 + nF 2d log nH + cmH log 2nH
many variables. In particular, under any assignment to the variables, any clause of Ref F can be evaluatedby looking at the values of polylog(n) many variables, where n is number of variables of Ref.2 Thus,
S EARCHRef F ∈ TFNPdt .
The following theorem establishes the “furthermore” part of (i) of Theorem 7.
Theorem 9. For any S EARCHF ∈ TFNPdt , PF (Ref F ) = O(polylog(n)).
Proof. Fix an instance of S EARCHRef F . By Theorem 7, it suffices to show that S EARCHRef F is reducible toan instance of S EARCHF . Let the parameters of Ref F be (nH , mH , (d, nF )), where c = d + log nF , and let
Ti , Tjo be the generic decision trees of Ref F .
o specifying a reduction from S EARCH
We will define the decision trees T1 , . . . , TnF , T1o , . . . , Tm
Ref FF
to an instance of S EARCHF on nF variables. To do so, we will say that a decision tree T evaluates one ofthese generic decision tree T by the following recursive procedure, beginning at the root of T : Let v be thecurrent vertex. If v is not a leaf then query xv and let j ∈ [nH ] be the outcome. Then query αj for the valueof the j th variable of H. If αj = 0 then proceed to the left child of v in Ti and to the right child if αj = 1.
Otherwise, if v is a leaf query xv and output its value.
– Ti evaluates Ti and outputs the value in {0, 1} to should assign to the ith variable of F .
2

Note that in this definition of Ref, and in particular V , we have excluded the formula FH from the input, and let it be defined
implicitly from the decision trees and nF . We could instead explicitly include FH as part of the input. However, as F has widthc and each decision tree has depth at most c, FH is a CNF formula of size at most mH · 2dc . Hence, FH would be encoded
generically in Π with that many variables. This would only change the number of variables of Ref by a quasi-polynomial amount,and hence the complexity of verifying and reducing to Ref by a polylog(n) amount. Thus, these formulas are equivalent up topolylog-reductions.

14

– Tjo first sequentially evaluates Ti to obtain the value of the variable i ∈ Vars(Cj ), where Cj is the j thclause of F . If this truth assignment satisfies the Cj , then Tjo outputs something arbitrary. Otherwise,
if Cj is falsified, then Tjo evaluates Tjo to obtain the index k ∈ [mH ] of a clause of H. The assignment
discovered thus far must falsify some clause D of the formula FH . D should be a weakening k thclause of H. To check whether this is the case, Tjo queries the values of the variables Ck,ℓ for eachℓ ∈ [c] to determine the variables which belong to k th clause. If D is not a weakening of this clause,then we have found a falsified clause of Ref, which we output. Otherwise, if D is a weakening of thek th clause, then as D is falsified, so is the k th clause of H. Hence, we must have discovered a falsified
clause of SAT, which we output.
Each Ti has depth O(d log nH ) and each Tjo has depth O(w(F ) · d log nH + log mH + c log nH ), which areboth poly-logarithmic in the number of variables of Ref F .

2.5

TFNP Problems for Proof systems which Prove their own Soundness

In this section we identify the following two conditions as being necessary for a proof system to be characterized by a TFNPdt problem:
1. Closed under decision-tree reductions, and
2. Admits short proofs of a reflection principle about itself.
The first condition is required because sub-classes of TFNPdt are closed under decision tree reductions. For
the second condition, we will see that any verification procedure for this proof system will suffice.
Theorem 10. Let P be a proof system that is closed under decision tree reductions and that has polylog(n)complexity proofs of a reflection principle Ref about itself, then P is characterized by S EARCHRef .
We begin with a high-level sketch of the proof. If there is a reduction from some S EARCHH to
S EARCHRef then, as P is closed under decision tree reductions, there is a proof of roughly the same complexity. Conversely, if we have a P -proof Π of an unsatisfiable formula H then we can construct a reduction
from S EARCHH to S EARCHRef of similar complexity by hard-wiring the description of Π and H into Ref,leaving only the variables of H free. Hence solutions to this instance of S EARCHRef are falsified clauses of
H. The following lemma is a technical statement of Theorem 10.
Lemma 11. Let P be a proof system that is closed under decision tree reductions, and let V be a verification
procedure for P , and denote by Ref = Ref P,V . Then for any unsatisfiable CNF formula H,i) If there is a complexity c reduction from S EARCHH to S EARCHRef then P (H) = poly(c · P (Ref)).
ii) There is a complexity O(P (H)) reduction from S EARCHH to S EARCHRef .
Theorem 10 follows immediately from Lemma 11 assuming that P (Ref) = polylog(n). Indeed, (i)implies that if there is a polylog(n)-complexity reduction from S EARCHH to S EARCHRef then P (H) =polylog(n). Conversely, (ii) implies that if P (H) = polylog(n) then S EARCHH ≤dt S EARCHRef .
Proof of Lemma 11. Let H be any unsatisfiable CNF formula and suppose that there is a complexity creduction from S EARCHH to S EARCHRef . Then, as P is closed under decision tree reductions, there is a
P -proof of H with complexity P (H) = poly(c · P (Ref)).

15

For the other direction, let Π be a complexity P (H) proof of H in P . We construct a reduction T =o ) from S EARCH to S EARCH(T1 , . . . , Tn ), T o = (T1o , . . . , Tm
H
Ref as follows. Let nH , mH be the numberof variables and number of clauses of H respectively. The decision trees T will hardwire the input (H, Π)into the instance of Ref = Proof ∧ SAT with parameters nH , mH , P (H), using constant decision trees, andmap the input variables x1 , . . . , xnH of S EARCHH to the variables α1 , . . . , αnH of Ref. For each clause iof Proof we let Tio output the index of an arbitrary clause of H. For each clause ℓ of SAT, corresponding
to some clause i ∈ [mH ] of H, the tree Tℓo outputs i. This is a constant-depth decision tree reduction to an
instance of S EARCHRef on exp(c)-many variables. Hence the complexity of this reduction is O(P (H)).
It remains to argue that this reduction is correct. Let α ∈ {0, 1}nH be any assignment to S EARCHH . As
Π is a valid P -proof of H, all of the clauses of Proof(T (α)) are satisfied. The formula SAT(T (α)) assetsthat H is satisfied by α, and hence some clause of SAT must be falsified. By construction, if ℓ is a falsified
clause of SAT then it must be part of the constraints encoding that some clause i ∈ [nh ] of H is satisfied.
Hence clause i of H must be falsified, and Tℓo correctly outputs the index i of a falsified clause of H.

3

Characterizations of the Polynomial Calculus

As an instantiation of the generic connection between TFNPdt and proof complexity, we develop a total
search problem which characterizes the Polynomial Calculus. Using this, we show that the Polynomial
Calculus can prove its own reflection, establishing Theorem 2. We do this for every finite field, as well as
PC over the integers when coefficients are measured in unary. This answers an open question from [27].
The Polynomial Calculus (PC). The Polynomial Calculus proves that a system of polynomials {pi (x)}i∈[m]
has no common root over {0, 1}n . An unsatisfiable CNF formula F = C1 ∧ . . . ∧ Cm is encoded as a systemof polynomial by mapping each clause Ci to the conjunct C i . For example, (x1 ∨ ¬x2 ∨ x3 ) is represented
as (1 + x1 )x2 (1 + x3 ) = 0. We will operate exclusively with multilinear arithmetic; that is, x2i and xi are
represented by the same function; that is, we work over the ideal ⟨x2i = xi ⟩i∈[n] .
A PC derivation of a polynomial q from a set of polynomials {pi (x)}i∈[m] using the following two
inference rules:– Addition. From two previously derived polynomials p, q, deduce p + q.
– Multiplication by a Variable. From a previously derived polynomial p, deduce xi p for some i ∈ [n].
The size of a proof is the number of monomials (counted with multiplicity) in the proof, the length is thenumber of lines (applications of rules), and the degree is the maximum degree of any polynomial at any
step in the proof. A PC proof of a system of polynomials {pi (x)}i∈[m] is a derivation of the polynomial 1,
certifying that the set of polynomials has no roots over {0, 1}n . The complexity of proving an unsatisfiable
CNF formula F in PC ismin{size(Π) + log degree(Π) : Πis a PC proof of F }For any prime q, Fq -PC is obtained from PC by replacing addition by addition over Fq .
We begin by characterizing the F2 -PC. Our characterization will extend the characterization of F2 Nullstellensatz by PPA [28], the class of total search problems reducible to L EAF.

16

Leaf. An instance of L EAFn is given by a function N : [n] → [n] × [n]. We view N as defining a degree≤ 2 undirected graph, where an edge (u, v) is present in the graph iff u ∈ N (v) and v ∈ N (u). A vertexv ∈ [n] is a solution if:– Root Violations. If v = 1 and |N (1)| ≠ 1. That is, 1 is not a leaf of the graph.
– Leaf Violations. If v ̸= 1 and |N (v)| ≠ 2. That is, v is a leaf other than the designated leaf 1.
This problem is total by a parity argument: each vertex is matched with its two neighbours. As the 1-vertex
only one neighbour, there must be another vertex with only a single neighbour.
The IndPPA class is defined by its complete problem I ND L EAF. At a high level, an instance of I ND L EAF
is formed from an instance of L EAF by partitioning the vertices [n] into groups (for simplicity, in the actual
problem each pool actually gets a copy of [n]), which we call pools, P1 , . . . , PL , where we require that
P1 = {1}. These pools are arranged in a rooted dag, with P1 being the root, and we require that for every
Pi with children Pc , Pc′ , there is a matching between the vertices in Pi ∪ Pc ∪ Pc′ . If the edges of this dag
are fixed then this problem remains PPA-complete — essentially it is an instance of L EAF in which we haveconstrained where each vertex can be matched. However, if we allow the edges of this dag to be definedby variables, then we are able to simulate the ability of PC to dynamically simplify a polynomial after amultiplication step.
Inductive Leaf. An instance of the IndPPA-complete problem I ND L EAF for parameters L, N , is given byfunctions E : [L] → [L] × [L] and functions M (v) : [L] × [N ] → [L] × [N ] for each v ∈ [L]. We willinterpret E and M (v) as forming the following structure:– The dag E. We view [L] as the vertices of a rooted dag with the ≤ 2 outgoing edges of vertex v givenby E(v) = (u, w). If one (both) of (u, w) are equal to v then we will interpret v as having one (no)child. We will ensure that E forms a dag with root vertex 1 by making v a solution if it is not the casethat u, w ≥ v.
– The Pools. We call each vertex v ∈ [L] a pool and associate a subset Pv ⊆ [N ] with it; we call these
the nodes of pool V . To identify this subset, we will say that a node m ∈ [N ] does not appear in poolv if M (v) (v, m) = (v, m) and appears otherwise. That is,
Pv := {m ∈ [N ] : M (v) (v, m) ̸= (v, m)}.
– The Matching. For each pool v ∈ [L] with children E(v) = (u, w), we will have a matching between
the nodes Pv ∪ Pu ∪ Pw . This matching is given by the function M (v) , and we say that m ∈ Pi
and γ ∈ Pj are matched, for i, j ∈ {u, v, w}, if M (v) (i, m) = (j, γ) and M (v) (j, γ) = (i, m). The
structure of these matchings can be seen in Figure 2.
– The Root. The root pool 1 contains only the 1-node, P1 = {1}.
There are four types of solutions, which can be seen in Figure 3:– Dag Violations. A pool v ∈ [L] such that E(v) = (u, w) and either u < v or w < v.
– Root Violations. Any violation to P1 = {1}. That is,17i) (1, 1) is a solution if M (1) (1, 1) = (1, 1), andii) (1, m) is a solution if M (1) (1, m) ̸= (1, m).
– Matching Violations. A node that is incorrectly matched in the matching constraint for a pool v. Thatis, (v, u, m) is a solution if u ∈ E(v) ∪ {v}, and m ∈ Pu , and eitheri) m is matched to a node in a pool w ̸∈ E(v) ∪ {v}: M (v) (u, m) = (w, m′ ) for some m′ , orii) The node which m is matched to is not matched to m: M (v) (M (v) (u, m)) ̸= (u, m)– Consistency Violations. If u ∈ E(v) then node m of pool u occurs in the matching for v iff it occurs
in the matching for u. That is, (v, u, m) is a solution if E(v) = (u, z) for some z ∈ [L] and eitheri) node m of u is inactive in v but active in u: M (v) (u, m) = (u, m) but M (u) (u, m) ̸= (u, m)ii) node m of u is active in v but inactive in u: M (v) (u, m) ̸= (u, m) but M (u) (u, m) = (u, m)
Encodings. We think of the function E : [L] → [L]2 as being encoded as follows: for each v ∈ L, we an
2L-ary variable Ev naming u, w such that E(v) = {u, w}. These can be encoding binary by replacing Evby 2 log L-many variables coding Ev . These two encodings are equivalent up to polylog-depth decision tree
reductions: from polylog-depth decision trees T1 , . . . , T2 log L specifying the values of the variables of thebinary encoding we can construct a polylog-depth decision tree T specifying the value of Ev by stacking the(logarithmically-many) trees T1 , . . . , T2 log L . Conversely, given a polylog-depth decision tree T specifying
the value of Ev we can construct decision trees T1 , . . . , T2 log L , where Ti (x) outputs the ith bit of T (x).
For ease of notation we will work with these 2L-ary variables while implicitly working with these binary
variables. Similarly, we have 2 log L-many variables Ev naming u, w such that E(v) = {u, w}. Similarly,(v)
for each v, u ∈ [L] and m ∈ [N ], we have an LN -ary variable Mu,m naming M (v) (u, m), which can be
encoded with log L + log N -many variables.
Claim 12. I ND L EAF ∈ TFNPdt .
Proof. The totality of I ND L EAF follows from a parity argument. Suppose that there is an instance of
I ND L EAF that does not have a solution. Observe that for each leaf l ∈ [L] (with E(v) = (v, v)) wehave a matching M (l) on the nodes in Pl . Hence, |Pl | is even. We also have that |P1 | is odd. We claim that
if |Pv | is odd and E(v) = (u, w) then either |Pu | or |Pw | is odd. Indeed, the matching M (v) between thevertices of Pv ∪ Pu ∪ Pw , as well as the fact that we do not have any inconsistent appearances, ensures that
|Pv | + |Pu | + |Pw | ≡ 0 mod 2.
Beginning at 1, we walk down the dag maintaining that |Pv | is odd for the current vertex v, until wereach a leaf. This is a contradiction, as |Pv | is even for every leaf. Hence, there must be a solution to thisinstance of I ND L EAF. Finally, observe that any solution to I ND L EAF can be efficiently verified by a constantnumber of calls to E and M (m) .
The following theorem states that F2 -PC is characterized by I ND L EAF.
Theorem 13. Let F be any unsatisfiable CNF formula. There is a complexity c reduction from S EARCHF
to I ND L EAF iff F2 -PC(F ) = O(c).

18

1
3

M (3)
2

3

3

4

5

2

6
2

5
7

1

1
3

2

1
3

6

8

Figure 2: The structure of an I ND L EAF instance on L = 8 and N = 3. Left is the dag in which every
pink blob indicates a matching. Here we have, for example, E(2) = {4, 5} and E(7) = {7}. Right is an
example of a matching for M (3) , where P3 = {2, 3}, P5 = {2, 1}, and P6 = {1, 3} as the remaining nodes
self-loop, meaning that M (3) (3, 1) = (3, 1), M (5) (5, 3) = (5, 3), and M (6) (6, 2) = (6, 2), and hence thesenodes do not appear in their respective pools. The matching M (3) is indicated by the blue edges. Here,M (3) (3, 2) = (5, 2), M (3) (5, 2) = (3, 2), M (3) (5, 1) = (6, 3), M (6) (6, 3) = (5, 1), M (3) (3, 3) = (6, 1),
and M (6) (6, 1) = (3, 3).

Dual Variable Encodings. As a corollary, we observe that this theorem holds also for F2 -PCR. This is
the extension of F2 -PC to include variables xi for each variable xi . The benefit of these additional dual
variables
W is thatWit allows us to reduce the number of monomials
Q needed
Q to encode CNF formulas. A clause
C = i∈I xi ∨ j∈J xj is encoded as the polynomial DC = i∈I xi j∈J xj . The dual variable encodingof a CNF formula F = C1 ∧ . . . ∧ Cm is the system of polynomials
DF := {DCi : i ∈ [m]} ∪ {xi + xi = 1 : i ∈ [n]}.
The set of polynomials DF is unsatisfiable in the sense that there is no x ∈ {0, 1}2n such that for everyp ∈ DF , p(x) = 0.
For an unsatisfiable system of polynomials D = {p1 , . . . , pm } over n variables, the false polynomial
search problem S EARCHD ⊆ {0, 1}n × [m] is defined as(x, i) ∈ S EARCHD ⇐⇒ pi (x) ̸= 0.
We observe that for any proof system which admits a TFNPdt -characterization, using the dual variable
encoding or the regular encoding does not affect complexity. This is in contrast to measuring proofs by theirsize (number of bits), where we know that dual and regular encodings can be exponentially separated [14].
Observation 14. For any unsatisfiable CNF formula F over n variables, S EARCHF =dt S EARCHDF .
Proof. Let F = C1 ∧ . . . ∧ Cm . We define a reduction {Ti }i∈[2n] , {Tjo }j∈[m+n] from S EARCHF to
S EARCHDF as follows. For each i ≤ n let Ti (x) = xi and for each i > n let Ti (x) = 1 − xi . For
each i ∈ [m] let Tio (x) = i and for each i > m let Tjo be arbitrary. Observe that this reduction is correct:
19

4

2

(a) Dag violations.

1

1
i

1

1

(b) Root violations. Left: type (i). Right: type (ii).
i

i

k

j

j

(c) Matching violations. Left: type (i). Right: type (ii).

i

j

i

j

(d) Consistency violations. Left: type (i). Right: type (ii).

Figure 3: The solution types of I ND L EAF marked in red. A dashed blue line indicates that i points to j
(M (v) (v, i) = (u, j), while a solid blue line indicates that there is an edge between i and j (M (v) (v, i) =(u, j) and M (v) (u, j) = (v, i)).
20

for any x ∈ {0, 1}n , T (x) = (x, x) and hence we satisfy every xi + xi = 1. Hence the only falsified
polynomials of DF (x) are of the form DCi and DCi (x, x) ̸= 0 iff Ci (x) = 0.
For the converse direction, we define the reduction {Ti }i∈[n] , {Tjo }j∈[m] as follows. For each i ∈ [n], Ti
queries xi and xi . If xi + xi ̸= 1 then we output the constraint xi + xi ̸= 1 as a solution to S EARCHDF .
Otherwise, Ti (x, x) = xi . Finally, Tjo (x, x) = j.
We will now prove Theorem 13, which is broken into Lemma 16 and Lemma 15, and proven over thefollowing subsections.

3.1

PC Proofs Imply Reductions

We begin with the easier direction of Theorem 13.
Lemma 15. Let F be an unsatisfiable CNF formula. If there is a F2 -Polynomial Calculus proof of F withsize L and degree-d then there is a depth O(d)-reduction from S EARCHF to an instance of I ND L EAF on
O(L2 )-many variables.
An example of this construction is given in Figure 4.
Proof. Let Π be a F2 -PC proof of F and fix a topological ordering of the lines in Π with the first line being
the 1 polynomial. Let N be the number of distinct monomials that occur in Π and let L be the number oflines. The I ND L EAF instance that we construct will have pools [L] and nodes [N ].
Fix any assignment x ∈ {0, 1}n to F . The edges of the dag in the I ND L EAF instance will be in oneto-one correspondence with the inferences in Π, with one twist. Let v be a line in Π there are three cases
depending on how v was derived:– If v is an axiom, then the decision tree E(v)(x) = (v, v) always. That is, v becomes a leaf of the dag.
– If v was derived by addition from u, w in Π then E(v)(x) = (u, w) always.
– If v was derived from u by multiplication by a variable xi , then the decision tree E(v) queries xi andoutputs v if xi = 0 and otherwise it outputs u. That is, v becomes a leaf in the dag if xi = 0.
The intuition behind the multiplication case is that if xi = 0 then v becomes the 0-polynomial under thisassignment, as every monomial in v contains xi .
For every line v ∈ [L] of Π, there will be a one-to-one correspondence between the monomials in line vthat are non-zero under x and the nodes that appear in Pv , and hence we will abuse notation refer to nodes
as “monomials”. That is,
Pv = {m : m is a monomial in line v and m(x) ̸= 0}.

(1)

To ensure that this is the case, and that we maintain consistency (i.e., avoid matching violations of type(iii)), for every pool u ∈ [L] (including v) and every monomial m ∈ [N ] that does not occur in u, we will
fix M (v) (u, m) = (u, m) always. Otherwise, if the monomial m occurs in line u, then the decision tree
M (v) (u, m) will query the at most d-many bits of x which occur in m in order to check whether m(x) = 0.
If m(x) = 0 then M (v) (u, m) = (u, m). Otherwise, if m(x) ̸= 0, then we set the matching so that
M (v) (u, m) ̸= (u, m) as follows:

21

1

M (3)

x1 x2 + x1 x3

3
1

3

1

2

x1 + x1 x3

5

1

2
3

4

4

4
[[x1 = 1]]

x1 + x3

2

1
3

x1 x2 + x1

4

6

x

1

M (4)

3

4

Figure 4: An example part of an F2 -PC proof and the relevant part of the corresponding I ND L EAF instance.
Left: part of a F2 -PC proof. Middle: the dag of the I ND L EAF instance when x1 = 1. Right: the The
matching for pool 1 indicated in blue, and the matching for pool 2 indicated in red when x1 = 1.
– Addition: If v was obtained by addition from lines u and w then in the matching for v, we will match
each of the monomials m in v to the corresponding monomial in u or w that it came from. That is, we
set M (v) (v, m) = (u, m) and M (v) (u, m) = (v, m) if m came from u and otherwise, we set it to w.
Any monomial m that occurs in u (w) but not in v must have cancelled mod 2 during addition, and so
there must be a copy of m in w (u). Hence, the decision trees M (v) (u, m) = (w, m) and M (v) (w, m).
– Multiplication: If v is derived from u by multiplication by a variable xi , then every monomial in v
contains the variable xi . For each z ∈ {u, v} and each monomial m, M (v) (z, m) begins by querying
the variable xi . If xi = 0 then we set M (v) (z, m) = (z, m). Note that this does not cause any
consistency violations for u because if xi = 0 then E(v) = (v, v). Therefore, u is not a child of v,
and so M (v) (u, m) may be arbitrary.
Suppose that xi = 1. Observe that for every monomial xi m in v, exactly one of m or xi m occurs
in u — they cannot both occur, as they would have cancelled mod2 when multiplied by xi and so
xi m would not be in v. Let m′ be the one which occurs in v and match M (v) (v, xi m) = (u, m′ )and M (v) (u, m′ ) = (v, xi m). Finally, for any monomial m in u that was not matched in this way,
if xi is not in m then mxi must also be in u, by the same argument as above. Hence, we match
M (v) (u, m) = (u, mxi ) and M (v) (u, xi m) = (u, xi ). Similarly, if xi is in m then we match it to theoccurrence of m \ xi .
– Axioms: If v is an axiom in Π, then v = C for some clause C of F . Let m be some monomial in
C. The decision tree M (v) (v, m) queries the at most d-many variables in C to get some assignmentα ∈ {0, 1}Vars(C) . If C(α) = 1, and hence C(α) = 0, then either (1) m(α) = 0, or (2) there isanother monomial m′ in C such that m ↾ α = m′ ↾ α. In the first case, M (v) (v, m) = (v, m) and in
the second case M (v) (v, m) = (v, m′ ).

22

Otherwise, if C(α) = 1 then we have found a solution to S EARCHF . As C(α) = 1, there will be
an odd number of monomials m in C such that m ↾ α = 1 and the remaining monomials m′ inC will satisfy m′ ↾ α = 0. Hence, no matter how we set the matching there will be a matchingviolation, but for concreteness we pick some monomial m∗ such that m∗ is not in C, and we match
M (v) (v, m) = (v, m∗ ) for every monomial m in C such that m ↾ α = 1.
Any decision tree which has not been defined by this process can be set arbitrarily without causing a violation. This completes the description of the I ND L EAF instance. The correctness of this reduction will be
guaranteed by the following claim.
Claim. The only solutions are matching violations for pools corresponding clauses C of F falsified by x.
Before proving this claim, we complete the description of the reduction by describing the output decision
trees Tso for each solution s. By the claim, if s is not a matching violation for pool v corresponding to anaxiom of F , then Tso can be defined arbitrarily. Let s = (v, v, m) for v = C for some clause C of F andmonomial m in C. The decision tree Tso outputs the index of the clause C in F .
Proof of Claim. As the final line L of the proof contains only the 1-monomial, there will be no root violations. As we respect the topology of the proof there will also be no dag violations. Consistency violations
are avoided as the nodes in each pool are in one-to-one correspondence between the non-zero monomials in
the corresponding line in Π. Matching violations at non-leaf nodes are avoided because we match monomials to the corresponding monomial in the line that they came from in Π. Therefore, the only potential
solutions are matching violations at the leaves. By construction, the matchings corresponding to clauses C
of F that are satisfied under x are correct, and hence the only violations occur at pools corresponding tofalsified clauses of F .

3.2

Reductions Imply PC Proofs

Q
V
V
We Q
begin with some terminology. A conjunct i xi ∧ j ¬xj is represented as the polynomial i (1 −xi ) j xj . For conjuncts C, C ′ , we say that C ⊆ C ′ if every literal of C is contained in C ′ . For a decision
tree T with output in [k], we associate it with the sum of conjuncts
X[[T = k]] :=p,
k-path p∈Twhere a k-path is a root-to-leaf path p ending in a leaf labelled k, and p is associated with the product of theliterals occurring along the path p. For a conjunct C, say that C ⊆ [[T = k]] if C ⊆ p for all k-paths p ∈ T .
If Ti is the decision tree for some variable x of I ND L EAF, we write [[x = k]] := [[Ti = k]]. We will often
make use of the fact that summing over every root-to-leaf path in a decision tree gives the 1-polynomial:
X
X[[xi = j]] =p = 1.
p∈Tij∈[k]

Lemma 16. Let F be an unsatisfiable CNF formula. If S EARCHF is reducible to an instance of I ND L EAF
on n variables using decision trees of depth at most d then there is an O(d)-degree and size-n2 2O(d) F2 -PC
proof of F .

23

Proof. Suppose that F = C1 ∧ . . . ∧ Cm is an unsatisfiable CNF formula and S EARCHF reduces to
I ND L EAFn using decision trees {Ti }, {Tjo } of depth at most d. Let L be the number of pools and N
the number of nodes of the I ND L EAFn instance. For each pool v ∈ [L] consider the polynomialX
XX[[M (v) (v, m) = (u, γ)]],[[M (v) (v, m) ̸= (v, m)]] =Pv :=m∈[N ] (u,γ)̸=(v,m)

m∈[N ]

As we are working over F2 , the value of Pv (x) records whether the number of monomials in v, |Pv |, is evenor odd. To prove F using this reduction we will follow the proof of totality of I ND L EAF. Beginning fromL, we will derive that Pv = 0 for v = L, . . . , 1.
Claim 17. For each v ∈ [L], there is a degree O(d), size N L2O(d) F2 -PC derivation of the polynomial Pv
from F .
Using this claim, we derive that P1 = 0. This suffices in order to complete the proof, as the axioms of
I ND L EAF enforce that |P1 | is odd.
Claim 18. There is a degree O(d), size N 2O(d) F2 -PC derivation of the polynomial P1 − 1 from F .
Having derived the polynomials P1 and P1 −1, summing them over F2 gives 1, completing the proof.
We will now prove the outstanding claims, which will rely on the following Key Observation. Let β bea solution to I ND L EAF (either a dag, root, matching, or consistency violation), the indicator of the solution
β is the minimal conjunct Iβ such that Iβ (x) = 0 iff x ↾ Vars(β) = β.
Key Observation: If P is any conjunct such that there is a solution β with Iβ ⊆ P then P has a F2 -PC
derivation of degree O(d + deg(P )) and size O(|P |2d ) from the axioms of F .
Proof. Let Tβo be the output decision tree for the solution β. As Iβ ⊆ P , any assignment x which falsifies
P must witness the solution β. Let k the index of the clause of F output by Tβo (x). By the soundness of the
reduction, C k (x) = 0. Hence, whenever P · [[Tβo = k]] is falsified, C k must be falsified as well, and so wemust have C k ⊆ P · [[Tβo = k]]. Putting this together,P =X

P · [[Tβo = k]](Summing all the root-to-leaf paths in Tβo gives 1)

k∈[m]

=

X

C k = 0.

(C k are axioms of F )k∈[m]

As Tβo has depth at most d, it has at most 2d -many leaves and the bound on the degree and size follows.
Proof of Claim 18. It suffices to express
X
P1 − 1 :=X[[M (1) (1, m) = (u, γ)]] − 1m∈[N ] (u,γ)̸=(v,m)

as a low-degree polynomial in which every term involves one of the axioms C i of F . Consider any termof the form [[M (1) (1, m) = (u, γ)]] for u ̸= 1 or γ ̸= m, or [[M (1) (1, 1) = (1, 1)]]. Any assignment tothe variables of F which satisfies one of these terms is a root violation, and hence a (1, m) is a solution to24

I ND L EAF. Since summing over all root-to-leaf paths in the decision tree M (1) (1, 1) gives the 1 polynomial,
we have
X X[[M (1) (1, 1) = (u, γ)]] − 10=u∈[L] γ∈[N ]=X[[M (1) (1, 1) = (u, γ)]] + [[M (1) (1, 1) = (1, 1)]] − 1(u,γ)̸=(1,1)=

X[[M (1) (1, 1) = (u, γ)]] + 0 − 1(Key Observation)(u,γ)̸=(1,1)=

X[[M (1) (1, 1) = (u, γ)]] +

X

X

X

[[M (1) (1, m) = (u, γ)]] − 1(Key Observation)m̸=1 (u,γ)̸=(1,m)(u,γ)̸=(1,1)=

X[[M (1) (1, m) = (u, γ)]] − 1m∈[N ] (u,γ)̸=(1,m)= P1 − 1.
This polynomial is composed of a sum of O(N )-many pairs of decision trees (the second decision tree
coming being the output decision tree from the Key Observation), each of depth d and therefore at most
2d -many leaves. Hence, this is a proof of degree O(d) and size at most N 2O(d) .
Proof of Claim 17. We will give a size N 2O(d) and degree O(d) proof of the polynomial


X
Pv +
[[E(v) = (u, w)]] Pu + Pw

(2)

u,w>v

from the clauses of F , expressing that the matching for pool v does not contain any violations. Having
derived (2) for all v ≤ L the claim follows by induction on v = L, . . . , 1. For v = L, observe that (2)is simply PL as there are no u, w > L, and hence by (2) we have a small proof of our base case from theclauses of F . For v < L, suppose that we have derived Pu = 0 for all u > v. Multiplying them we obtainX[[E(v) = (u, w)]] Pu + Pw .
u,w>v

Adding this to (2) over F2 gives Pv .
It remains to give a small proof of (2) from the clauses of F . Consider any term [[E(v) = (u, w)]] whereat least one of u, w is greater than v. This is a dag-violation and so by the Key Observation we have a small
proof of this term from F . Using this,25

(2) = PvX[[E(v) = (u, w)]] Pu + Pw[[E(v) = (u, w)]] +

 X

= Pv

X



=0+

X

[[E(v) = (u, w)]] +u<v∨w<vp∈E(v) p = 1)[[E(v) = (u, w)]] Pv + Pu + Pw

u,w>v




[[E(v) = (u, w)]] Pv + Pu + Pw ,

X

P

u,w>v

u,w∈[L](As(Key Observation)

u,w≥v

=

X

[[E(v) = (u, w)]]=Pzz∈{u,v,w}u,w∈[L]X

X[[E(v) = (u, w)]]

X

X[[M (z) (z, m) ̸= (z, m)]],(3)z∈{u,v,w} m∈[N ]u,w∈[L]

where the last line follows by the definition of Pz .
In order to derive (3) from the axioms we will define the following polynomial which can be read as thesum of all of the indicators of valid matchings for pool v.
X
X
X
matchv :=[[E(v) = (u, w)]][[M (v) (v, m) ̸= (v, m)]] · matchvz,m .
u,w∈[L]m∈[N ] z∈{u,v,w}

We will define the polynomial matchvz,m shortly. However, for now we note that matchvz,m ≡ 1 as it will be
the sum of all root-to-leaf paths of in a sequence of decision trees. Then we can write
X
X
X
(3) =
[[E(v) = (u, w)]][[M (v) (v, m) ̸= (v, m)]] · matchvz,m = matchv .
u,w∈[L]m∈[N ] z∈{u,v,w}

Hence, it suffices to show that there is an efficient proof of matchv from the axioms of F .
Definematchvz,m :=X X
X[[M (v) (z, m) = (a, α)]]a∈[L] α∈[N ]X[[M (v) (a, α) = (z ∗ , m∗ )]]z ∗ ∈[L] m∗ ∈[N ]X X[[M (a) (a, α) = (b, β)]]b∈[L] β∈[N ]which records the possible matchings of node m in pool z in the matching for v. The first term asks for thenode (a, α) that the node m from pool z is matched to in the matching for z, the second term asks what thenode α from pool a is matched to, and the last term checks whether node α is active in pool a. Note thateach term is a sum over all of the paths in a decision tree, matchvz,m = 1.
To show that matchv has a proof from F , we will partition matchv into two multisets of conjuncts,
V which contains the conjuncts which witness violations, and C which correspond to correct matchings— those without violations. That is, C is the multiset of conjuncts witnessing (z ∗ , m∗ ) = (a, α) andM (a) (a, α) ̸= (a, α), and E are the remaining conjuncts in matchv . The conjuncts in V can be removed by
the Key Observation, while we argue that each conjunct in C occurs an even number of times in matchv , as26

(z, m) is matched to (a, α) iff (a, α) is matched to (z, m).
X
Xmatchv =
t+
t
t∈C

=

X

t∈V

t+0

(Key Observation)

t∈C

=

X

[[E(v) = (u, w)]]

u,w>v

X X

X

X

[[M (v) (v, m) ̸= (v, m)]]·m∈[N ] z∈{u,v,w}

2 · [[M (v) (z, m) = (a, α)]][[M (v) (a, α) = (z, m)]][[M (v) (a, α) ̸= (a, α)]]a∈[L] α∈[N ]=0.

(Working over F2 )To bound the size and degree, observe that each term of matchvz,m is the product of three decision trees
each of depth at most d, and hence has size at most 23d and depth 3d. The application of the key lemma
introduces an additional depth≤ d output decision tree. The polynomial matchv is formed from matchvz,mfor every m ∈ [N ] by multiplying it two decision trees of depth at most d. Hence, each matchv can bederived in size O(N 26d ) and degree 6d.

3.3

PC Proves its own Soundness

In this section we show that the F2 -Polynomial Calculus can prove a reflection principle about itself.
Theorem 19. There is a reflection principle Ref PC for the F2 -Polynomial Calculus such that PC(Ref PC ) ≤polylog(n).
We define Ref PC by giving a natural verification procedure for F2 -PC proofs. To do so, for simplicity it
will be convenient to combine the F2 -PC rules into a single inference rule: for any line v1 , v2 ,v1 , v2,
v1 x + v2 y
for any x, y ∈ {0, 1, x1 , . . . , xn }. It is easy to see that this will change the complexity of the proof by atmost 2.
A Verification Procedure for F2 -PC.
We define the reflection principle by giving a verification procedure V PC (H, Π) := VnPC
(H,
Π).
For
simplicity of exposition, we will have break the complexity of
H ,mH ,ccthe proof into three parameters, N = 2 which denotes the number of monomials, L = 2c which denotes thenumber of lines, and d = c which denotes the degree of the proof.3 As before, nH and mH are the numberof variables and clauses of the CNF formula H.
Variables: V PC describes the proof Π with the following variables. Each line v ∈ [L] is given by a length(v)N vector mon(v) ∈ ([nH + 1]d )N , where the mth entry monm ∈ [nH + 1]d names the at most d variables in
the mth monomial in the v th line. The (nH + 1)-st value is understood to indicate the constant 1. Not every
3

Note that we could have used a size parameter s, rather than N and L, counting the bit-complexity of the proof (roughly the
number of monomials and the number of lines). However, this would only change the complexity of the PC-proof in Theorem 19
by log-factors, and it is notationally simpler to work with parameters N and L.

27

(v)

line contains N monomials and so for each m ∈ [N ] we include a variable am ∈ {0, 1} which indicates
whether the ith monomial is active — that is, whether it occurs in line v.
The lines L − mH + 1, . . . , L are reserved to describe the clauses of H. Every other line v ≤ L − mH(v) (v)
has a pair of predecessor pointers p1 , p2 ∈ [v − 1], naming the two previous lines from which v was(v) (v)
derived, and a pair of variable pointers v1 , v2 ∈ [nH + 2] naming the respective variables multiplying
previous lines in the derivation of v; the values nH + 1 and nH + 2 indicate the constants 1 and 0. Together,(v) (v)(v) (v)these variables state that the line v was derived as p1 v1 + p2 v2 .
To ensure that each inference in the proof is correct, for each line v ≤ L − mH there is a matching(v)(v)
between the active monomials in v, p1 , and p2 . The matching for line v is given by 3N -many variables
match(v) (δ, m) ∈ {0, 1, 2} × [N ] for δ ∈ {0, 1, 2} and m ∈ [N ], where δ ∈ {0, 1, 2} indicates whether mis belongs to v (0), the left child (1) of v, or the right child (2), and match(v) (δ, m) names the monomial thatc’s copy of m is matched to.
Constraints: The constraints of V PC are the following:– Final Line. There are constraints saying that the only monomial in line 1 is the 1-monomial. That is,(1)(1)
mon1 = 1, and for all m ̸= 1, am = 0.
– Axioms. For i ∈ [mH ] and v = L − i, we have constraints stating that the v th line is exactly theith clause of H. In particular, let k be the number of positive literals in Ci of H (of which there
are at most d), then we have constraints saying that exactly the first 2k monomials are active; that is,(v)(v)
a1 , . . . , a2k = 1. As well, we have constraints saying that the mth monomial of v is exactly themth monomial in the monomial-expansion of C i . To see that each of these can be expressed by a(v)
(v)
small CNF formula, observe that this constraints on the value of ai and monm can be defined by adecision tree querying the variables Ci,j for j ∈ [d] of Sat.
(v)

(v)

– Inferences. For each line v ≤ L − mH we have constraints saying that p1 , p2 ≥ v, and a set of(v) (v)
constraints saying that v was correctly derived from p1 , p2 . In particular, that the active monomials(v) (v)(v) (v)of v are exactly the monomials in p1 v1 + p2 v2 after cancelling mod2. More concretely, we(v) (v)have constraints stating that if an active monomial m from one of v, p1 , p2 is matched to another(v) (v)monomial m′ then m′ has to be matched back to m and the variables in m have to agree over v1 , v2 .
(v)
(v)
That is, if m is a monomial from v and m′ is a monomial from p1 then m = v1 m′ . We also
have constraints forcing that active monomials are only matched to active monomials, and no active
monomial is matched to itself.
The reflection principle for F2 -PC will be Ref PC (H, Π) := Sat(H, Π)∧V PC (H, Π). As every constraint
mentions O(d log nH )-many variables, this can be encoded as a CNF formula of width O(d log nH ).
Proof of Theorem 19. By Theorem 13, it suffices to construct a reduction from S EARCHRef PC to I ND L EAF.
Let nH , mH , (d, N, L) be the parameters of Ref PC . We construct an instance of I ND L EAF with L pools andN nodes. The high-level idea is simple: Ref PC is already almost an instance of I ND L EAF, with only a few
major differences:– V PC does not specify a matching for the axioms of H.
– Ref PC contains the additional Sat formula.
28

(v)

– Each node m ∈ [N ] no longer corresponds to a monomial, but rather has a set of variables monm ,naming which monomial it is.
Hence, given an assignment (H, Π) to S EARCHRef PC we construct the decision trees of the reduction as
follows:(v)(v)– Edges. For any v ∈ [L − mH ], the decision tree E(v) queries the variables for p1 , p2 and outputs(v) (v)
E(v) = (p1 , p2 ). For L − mH + 1 ≤ v ≤ L, define E(v) := (v + mH , v + mH ). Finally for
L + 1 ≤ L + mH let E(v) := (v, v).
– Non-Leaf Matchings. For every v ≤ L − mH and u ≥ [L] and m ∈ [N ], the decision tree M (v) (u, m)(v) (v)(u)queries p1 , p2 to determine the two children u1 , u2 of v, and am to determine if m is active. If(u)either u ̸∈ {u1 , u2 } or am = 0 then M (v) (u, m) = (u, m). Otherwise, decision tree asks for thevalue of match(v) (u, m) = (c′ , m′ ) ∈ {0, 1, 2} × [N ] and match(v) (uc′ , m′ ) = (c∗ , m∗ ), where(u ′ )(u)(v)
u0 := v, and also for the variables in these monomials monm and monm′c , and vc for the variable
used to derive m from m′ . If either we discover that (u, m) is matched to itself (m′ = m anduc′ = u) or if the variables in m do not agree with the variables of the monomial it was derived from(u ′ )(u)(v)(monm ̸= vc monm′c ) then we introduce a matching violation by sending M (v) (u, m) = (w, m)
for some w ̸∈ {u1 , u2 }. Otherwise, we set M (v) (u, m) = (uc′ , m′ ).
– Leaf Matchings. For any i ∈ [mH ], v = L − i + 1, and m ∈ [N ], the decision tree M (v) (v, m) queries
the variables Ci,j for j ∈ [d]. Let k be the number of positive literals in Ci , and note that C i has(v)
2k -many monomials. If am = 0 and m > k then set M (v) (v, m) = (v, m). Otherwise, if m > 2k(v)(v)
and am = 1 or if m ≤ 2k but am = 0 then we pick some w ̸= v and set M (v) (v, m) = (w, m),(v)
forming a matching solution. If neither of these hold, then query monm to determine the variables in
the mth monomial. If these disagree with the variables in Ci , then we violate an axiom constraint of
Ref PC and we set M (v) (v, m) = (w, m) for some w ̸= v in order to cause a solution. Finally, querythe bits of the assignment α to Sat that are mentioned by Ci . If we discover that Ci (α) = 0, thenagain we cause a solution by setting M (v) (v, m) = (w, m) for some w ̸= v. Otherwise, if Ci (α) = 1(v)
then either monm ↾ α = 0, in which case we set M (v) (v, m) = (v, m), and otherwise, as C i ↾ α = 0,(v)
there must exist another monomial in C i ↾ α which is equal to monm ↾ α; let this be the tth monomialof C i . The decision tree outputs M (v) (v, m) = (v, t).
It remains to define the output decision tree Tso for each solution s to I ND L EAF.
– Dag Violations. Let there be a dag violation at v. Then, as the edges of the I ND L EAF are exactly those(v) (v)in the inference structure of the Ref PC instance, there must one of p1 , p2 which outputs a value less(v) (v)than v, and hence violates one of the inference constraints of V PC . Hence, Tvo queries p1 , p2 andoutputs the index of that falsified constraint.
(1)

(1)

o
– Root Violations. If (1, m) is a root violation, then the decision tree T(1,m)
queries am , monm andoutputs the violated final line constraint.
o– Matching Violations. If (v, u, m) is a matching violation, the decision tree T(v,u,m)queries the same

variables as the decision tree M (v) (u, m) and outputs the appropriate violated inference constraint
if v is not an axiom, or if v is an axiom then it outputs the appropriate violated axiom constraint or
constraint of Sat.
29

– Consistency Violations. There will be no consistency violations in the reduction as it is defined, andso we let Tso be arbitrary for each potential consistency violation s.
This completes the reduction.

3.4

Characterizing Dynamic Variants of Static Systems

We end this section by discussing how one can define induction variants of TFNP problems (such as L EAF)
which characterize static proof systems (such as Nullstellensatz), in order to characterize their dynamic
variants. Consider some TFNP class which characterizes a static proof system and let R be a complete
problem for this class. We build a problem I ND R to characterizes the dynamic variant of this proof system
as follows: there are L pools, which correspond to the lines of the proof, and a dag structured defined byedge variables E (m) for each m ∈ [L], which define the children ml , mr ≥ m of m. Each pool has a set ofvertices, and we have an instance of the problem R defined over these vertices, where, as before, we restrict
the vertices in each pool m to only interact with vertices in neighbouring pools. The crucial part is that theedges of this dag (and hence how vertices in different pools interact) is determined by variables, rather thanbeing fixed a-priori.
Using this template, we develop characterizations of the Fq -Polynomial Calculus, the unary Polynomial
Calculus, and unary dag-like Sherali-Adams.
Polynomial Calculus over Finite Fields.
Kamath [34] showed that a Fq -variant of PPA, where one uses q-matchings, rather than matchings, characterizes Fq -Nullstellensatz. It is straightforward to generalize I ND L EAF to characterize Fq -PC. The
I ND L EAFq problem will be defined as I ND L EAF, except one now matches q-tuples, rather than pairs. Morespecifically, in the matching for each pool v ∈ [L], each active node m is either matched in a q-tuple with,or is matched in a 2-tuple, with the restriction that if m is matched in a 2-tuple with another node m′ thenm must belong to pool v and m′ must belong to one of the children u of v. The meaning of the two edges isthat the monomial m is being “carried forward” from line u to line v in the Fq -PC proof.
Unary Polynomial Calculus.
The unary Polynomial Calculus (uPC) proof system is the Polynomial Calculus system operating over the
integers, rather than a finite field. Unary refers to the fact that the size of a uPC proof is measured withcoefficients written in unary. That is, if αm occurs in some line in the proof, for α ∈ Z, then it contributes|α| towards the size.4
Göös et al. [27] characterized the unary Nullstellensatz proof system by PPAD, the class of total search
problems reducible to E ND - OF -L INE. We extend this to characterize uPC by IND-PPAD.
End-of-Line. An instance of E ND - OF -L INEn is given by predecessor and successor pointers p : [n] → [n]and s : [n] → [n]. We view the pointers as defining a degree≤ 2 graph on the vertices [n] where there is adirected edge (u, v) iff s(p(v)) = v and p(s(u)) = u. A vertex v is a solution if:– Root Violations. p(1) ̸= 1 or s(1) = 1.
4
Typically PC over Z is defined with a multiplication rule whereby one may derive, from previous lines p, q any line of the form
αp + βq for α, β ∈ Z. As we are measuring coefficients in unary, this operation may be simulated by repeated addition.

30

– Sink Violations. v ∈ V such that p(s(v)) ̸= v, meaning that v is a sink.
– Source Violations. v ̸= 1 such that s(p(v)) ̸= v, meaning that v is a source.
The IND-PPAD class, which characterizes uPC is defined by its complete problem I ND E ND - OF -L INE.
The major difference between this and I ND L EAF is that the matchings for each pool are now directed. The
direction of an edge will be indicated by the head-vertex being assigned “+” and the tail being assigned“−”; that is, if M (v) (u, m) = (u′ , m′ , +) and M (v) (u′ , m′ , −), then we interpret this as an arrow from u(the tail) to u′ (the head). We will enforce consistency between pools: if a node m of pool u is at the headof an edge in the matching for v then it must be at the tail of an edge in the matching for u.
The direction of the edges corresponds to the polarity of the monomials in the uPC proof: let m be anode belonging to some pool v. Then, the sign of the monomial corresponding to m in line v in the uPC
proof is determined by whether it appears at the head (positive) or tail (negative) of an edge in the matchingfor pool v. The consistency conditions ensure that the signs are maintained in each application of a uPC
rule.
Induction End-of-Line. An instance of I ND E ND - OF -L INE (I ND EOL) for parameters L, N is specified
by functions E : [L] → [L] × [L] and M (v) : [L] × [N ] → [L] × [N ] × {−, +} for each v ∈ [L]. We
interpret E and M (v) as defining the same structure as in I ND L EAF, with the following modification to thematching structure. In the following, ∗ denotes that the value is arbitrary.
– The Matching. For each pool v,
Pv := {m ∈ [N ] : M (v) (v, m) ̸= (v, m, ∗)}is the set of nodes which appear in v. Let E(v) = (u, w) be the children of v. We have a directed
matching between the nodes of Pv ∪ Pu ∪ Pw . This matching is given by the function M (v) , andwe say that m ∈ Pi and γ ∈ Pj are matched, for i, j ∈ {u, v, w}, if M (v) (i, m) = (j, γ, b) andM (v) (j, γ) = (i, m, b) for b ∈ {+, −} and b = {+, −} \ b. In this case, we say that (j, γ) is labelledb and (i, m) is labelled b, and we view this as a directed edge from the node labelled “−” to the nodelabelled “+”.
The solution-types are the same as I ND L EAF, with an additional type of consistency violation.
– Dag Violations. A pool v ∈ [L] such that E[v] = (u, w) and either u < v or w < v.
– Root Violations. Any violation to P1 = {1}.
i) (1, 1) is a solution if M (1) (1, 1) = (1, 1, ∗) or M (1) (1, 1) = (u, m, +) for some (u, m) ̸= (1, 1).
ii) (1, m) is a solution if M (1) (1, m) ̸= (1, m, ∗).
– Matching Violations. (v, u, m) is a solution if u ∈ E(v) ∪ {v}, and m ∈ Pu , and eitheri) m is matched to a node in a pool w ̸∈ E(v) ∪ {v}: M (v) (u, m) = (w, ∗, ∗).
ii) The node which m is matched to is not matched to m: M (v) (u, m) = (u′ , m′ , b) and M (v) (u′ , m′ ) ̸=(u, m, b), for some u′ ∈ E[v] ∪ {v}, m′ ∈ [N ], b ∈ {+, −}.
– Consistency Violations. A node m of pool u occurs in the matching for v iff it occurs in the matchingfor v, and its sign is consistent. That is, (v, u, m) is a solution if u ∈ E(v) and either
31

1

M (v)

4
3

1

2

2
3

1

2
3

4

4

x

1

M (u)

3

4

Figure 5: Two adjacent pools of an I ND EOL instance. The red arrows indicate the M (u) , while the blue
arrows indicated M (v) . There are no consistency violations present, as each node in Pu which is at the tailof an arrow in M (v) is at the head of one in M (u) , and vice-versa.
i) node m of u is inactive in v but active in u: M (v) (u, m) = (u, m, ∗) but M (u) (u, m) ̸= (u, m, ∗)ii) node m of u is active in v but inactive in u: M (v) (u, m) ̸= (u, m, ∗) but M (u) (u, m) =(u, m, ∗).
iii) node m changes polarity between pools: M (u) (u, m) ̸= (u, m, ∗) and M (v) (u, m) = (u′ , m′ , b)
and M (u) (u, m) = (u′′ , m′′ , b) for b ∈ {−, +}, u′ , u′′ ∈ [L], and m′ , m′′ ∈ [N ].
A portion of an instance of I ND EOL is depicted in Figure 5.
Theorem 20. Let F be any unsatisfiable CNF formula. There is a complexity c reduction from S EARCHF
to I ND L EAF iff F2 -PC(F ) = O(c).
We defer the proof of this theorem to the Appendix.
Unary DAG-Like Sherali-Adams.
The unary dag-like Sherali-Adams proof system generalizes both the uPC and (unary) Sherali-Adams proof
systems (see e.g., [20] for a definition). Briefly, Sherali-Adams
algebraic proof system which allows
V is an V
one toQ
introduce
additional
conjuncts.
Recallthataconjunctx∧i∈I ij∈J xj is encoded as the polynomial
Q
C := i∈I xi j∈J (1 − xj ).
Dag-Like Sherali-Adams. The unary dag-like Sherali-Adams (uDSA) proves the unsatisfiability of a
CNF formula F by deriving −1 from the polynomials {Ci = 0 : Ci ∈ F } using the addition and multiplication rules of uPC along with the following additional rule:– Conjunct Rule. From a previously derived polynomial p ≥ 0, deduce p + C for any conjunct C.

32

As before, we work over the ideal ⟨x2i − xi ⟩i∈[n] , multi-linearlizing implicitly.
We measure the degree of a uDSA proof by the maximum degree of any derived polynomial, and thesize of the proof is measured as the number of monomials (with multiplicity) that appear in the proof (thatis, we measure coefficients in unary).
Göös et al. [27] characterized unary Sherali-Adams by the class PPADS, whose complete problem is
S INK - OF -L INE. The S INK - OF -L INE problem is identical to E ND - OF -L INE, except that we no longer havesource violations. We extend this characterizing by defining the class IND-PPADS of everything reducible tothe complete problem I ND S INK - OF -L INE (I ND SOL). Like S INK - OF -L INE, I ND SOL restricts the solutionsof I ND EOL. In particular, I ND SOL will permit nodes which occur at the head of arrows to be incorrectly
matched. This corresponds to introducing conjuncts via the conjunct rule in a uDSA proof.
Induction Sink-of-Line. An instance of I ND SOL is identical to an instance of I ND EOL, with the matching and root violations replaced by the following:– Root Violations. Any violation to 1 being the only node in the first pool and occurring at the tail ofan arrow (1 is negative)i) (1, 1) is a solution if M (1) (1, 1) = (1, 1, ∗) or M (1) (1, 1) = (u, m, −) for any u ∈ [L], m ∈ [N ].
ii) (1, m) is a solution if M (1) (1, m) ̸= (1, m, ∗).
– Matching Violations. (v, u, m) is a solution if m ∈ Pu , and eitheri) u ∈ E(v) ∪ {v} and u is matched to a node in a pool which is not in E(v) ∪ {v}: M (v) (u, m) =(u′ , m′ , b) for u′ ̸∈ E(v) ∪ {v}.
ii) u ∈ E(v) and the node which m is matched to is not matched to m: M (v) (u, m) = (u′ , m′ , b)
and M (v) (u′ , m′ ) ̸= (u, m, b), for some u′ ∈ E[v] ∪ {v}, m′ ∈ [N ], b ∈ {+, −}.
iii) u = v and m appears at the tail of an arrow in M (v) and m is matched to a node which is
not matched back to it: that is, M (v) (v, m) = (w, m′ , +) ̸= (v, m, ∗) and M (v) (w, m′ ) ̸=(v, m, −).
The characterization of uDSA by I ND SOL follows by a very similar argument to the proof of Theorem 20,
combined with the characterization of Sherali-Adams by PPADS [27].
Theorem 21. Let F be any unsatisfiable CNF formula. There is a complexity c reduction from S EARCHF
to I ND SOL iff uDSA(F ) = O(c).

4Communication TFNP and Monotone Circuit Complexity

In addition to proof system characterizations of black-box TFNP subclasses, the communication versions of
TFNP subclasses have provided characterizations of monotone circuit models [28, 35, 49]. When combinedwith lifting techniques translating decision tree lower bounds to communication complexity lower bounds,
this has resulted in numerous new lower bounds for a variety of monotone circuit models. For example,
bounds on the F2 -Nullstellensatz proof system, which is characterized by black-box PPA were lifted tocommunication-PPA lower bounds, which characterizes F2 -monotone span programs [44]. Conversely, a
black-box and communication characterization of the same TFNP subclass automatically gives rise to a33

monotone interpolation theorem. In this section, we uncover the exact conditions under which a monotone
circuit model has a communication-TFNP characterization.
The first order of business is to define what is meant by a monotone circuit model. This is formalized by
the following notion of a monotone partial complexity measure.
Monotone Partial Function Complexity Measures. A monotone partial function complexity measure
mpc is a map from partial monotone functions to non-negative integers that is Monotone Under Solutions:whenever g solves f , mpc(g) ≥ mpc(f ).5
Typical such measures include the minimum monotone circuit, formula, or span program size of a total
function that solves f , but we won’t include a circuit model explicitly. As has been pointed out in the past,
there is a direct mapping from TFNP problems to partial monotone functions, and we utilize this mapping.
This will allow us to give an exact characterization of when a complexity measure on partial functions has a
TFNP characterization, proving Theorem 3.
Since complexity measures on total functions induce complexity measures on partial functions, thisalso gives a general condition under which a complexity measure on total monotone functions has a TFNP
characterization. Unfortunately, we don’t have a converse statement for total functions and it is conceivablethat measures that don’t meet our criteria also have TFNP characterizations. We explore this further insubsection 4.3.
It would be plausible to propose that some of the results in this section might have analogs for nonmonotone models of computation. However, the techniques we use seem not to hold for these models,
which might indicate why TFNP or other communication complexity characterizations of non-monotone
circuits are much more difficult to use to prove lower bounds.

4.1

Communication TFNPFor n bit strings x and x′ , we say that x′ dominates x, written x ≤ x′ , if xi ≤ x′i for every i ∈ [n]. A partial
Boolean function f on n bit strings is described by two disjoint sets of inputs, Nof which is the set of strings
that f rejects, and Yesf , the strings that it accepts. f is total if Nof ∪ Yesf = {0, 1}n . A partial Booleanfunction f is monotone if whenever x ∈ Nof and x′ ≤ x, then x′ ∈ Nof and whenever y ∈ Yesf and y ≤ y ′then y ′ ∈ Yesf . For partial functions f and g, we say f is solved by g if Nof ⊆ Nog and Yesf ⊆ Yesg . Thatis, g contains f as a sub-function.
′
Let h : {0, 1}n → {0, 1}n , and let f be a partial function on n′ -bit inputs. Then f ◦ h is the partial
function where Yesf ◦h = {x|h(x) ∈ Yesf } and Nof ◦h = {x|h(x) ∈ Nof }. If h is monotone in its input,
and f is monotone, then f ◦ h is monotone.
We are now ready to develop the connection between monotone complexity and a variant of TFNP whichuses communication-efficient reductions. Central to this connection is the Karchmer-Wigderson game.
Karchmer-Widgerson Game. Let f be a function. The Karchmer-Wigderson game for f , denoted KWf ,is the communication problem where one player has x ∈ Nof the other has y ∈ Yesf and the output isa position i so that xi ̸= yi . Similarly, for a monotone Boolean function f on n inputs, the monotone
Karchmer-Wigderson game for f , denoted M KWf , is a restriction of the Karchmer-Wigderson game to require that the output is a position i such that xi < yi .
5

Recall that a partial function g solves f if Nof ⊆ Nog and Yesf ⊆ Yesg .

34

Karchmer and Wigderson [35] showed that communication complexity of KWf (M KWf ) is an exact
characterization of the (monotone) circuit depth needed to compute f , or equivalently FPcc .
Communication TFNP. Consider relational communication problems defined by a predicate R ⊆ X ×
Y × [ℓ]. The corresponding communication problem has one player given x ∈ X, the other y ∈ Y , andthe goal being to output an index i so that R(x, y, i) holds. We say this problem is in t-bit communicationTFNP if for every x ∈ X, y ∈ Y , for some i, R(x, y, i); and given i, there is a t-bit communication
protocol V (x, y, i) to determine whether R(x, y, i) holds. We say that R ∈ TFNPcc if R is in polylog(n)bit communication TFNP.
We say that one communication problem R ⊆ Xm × Ym × [ℓ] mapping reduces to another R′ ⊆Xn′ × Yn′ × [ℓ′ ] with communication t if there are functions MX : X → X ′ , MY : Y → Y ′ and a t-bit
communication protocol S(x, y, i′ ) which outputs i so that
R′ (MX (x), MY (y), i′ ) =⇒ R(x, y, S(x, y, i′ )).
In particular this means that R requires at most t more bits of communication than R′ to solve. The complexity of this reduction is t + log n, and we say that this reduction is efficient, denoted by R ≤cc R′ , if
the complexity is O(polylog(m)). We say that two communication problems R, R′ are equivalent, denoted
R =cc R′ if R ≤cc R′ and R′ ≤cc R.
The following lemma says that TFNPcc is exactly the study of the monotone Karchmer-Wigderson
game.
Lemma 22. For any R ⊆ TFNPcc , there is a partial monotone function f such that R =cc M KWf .
Proof. Let R ⊆ X × Y × [ℓ] and let S(x, y, j) be a t-bit protocol that verifies that j ∈ [ℓ] is a valid solution
on input (x, y). We define a partial function f on N = 2t ℓ input bits. We think of each coordinate as
representing a solution j ∈ [ℓ] and a communication pattern for S(x, y, j). We then construct the accepting
and rejecting sets for f ; for each x ∈ X we construct an input α(x) ∈ {0, 1}N in NoF as follows: for eachj ∈ [ℓ] and t-bit communication pattern p ∈ {0, 1}t we set(
1 if there is a y ∈ Y such that S(x, y, j) evolves according to p and S(x, y, j) = 1,(x)α(j,p) =0 otherwise.
To construct YesF we build an input β (y) ∈ {0, 1}N in the same way, except we reverse 0 and 1:(
0 if there is a x ∈ X such that S(x, y, j) evolves according to p and S(x, y, j) = 1,(y)β(j,p) =1 otherwise.
We claim that M KWf is equivalent to R, using this construction as the map. Let j be a solution to
R on input (x, y). We simulate S(x, y, j) and output j together with the communication pattern p for the(x)(y)
simulation. This gives an index (j, p) such that α(j,p) = 1 > 0 = β(j,p) , which is a solution to M KWF on
input (α(x) , β (y) ). In the reverse direction, if we are given a bit (j, p) such that α(x) > β (y) , then we knowthat S(x, y, j) accepts, and we can return j.
We will also need the following notion which will allow us to pad a search problem.

35

Paddable. Say that the sequence Rn is paddable if there is a quasi-polynomial function p and a functiont(n) = polylog(n) so that Rn is t(n′ )-communication reducible to Rn′ for all n′ ≥ p(n).
The condition that the sequence Rn be paddable looks a bit artificial at first. However, if we drop it, we
would allow totally unrelated TFNP subclasses to be used in a characterization. For example, it would allow
for a class that is essentially PPA for infinitely many sizes and then suddenly switches to the pigeon-holeprinciple, and back again. Another example of a potential issue is that our class could contain all of TFNP
by slowly introducing TFNP problems into the sequence in a non-computable way. So we think natural
subclasses of TFNP with complete problems will have the paddable property.
In the remainder of this section we will prove Theorem 3, giving the exact conditions under which an
mpc characterizes a TFNPcc subclass.
Characterizes. We say that TFNPcc class C with a complete problem R = {Rn }n∈N characterizes a
mpc if for every partial monotone function f there is a complexity c reduction from M KWf to R iff
mpc(f ) = O(polylog(c)). As well, say that R characterizes a mpc if the class whose complete problem is R characterizes that mpc.
Before proving Theorem 3, we will first give conditions for a TFNPcc characterization which involvea stronger notion of a universal family of functions, which we will call complete families (Theorem 23).
Using this, we then weaken the requirement to admitting a universal family (Theorem 27). In between, we
explore sufficient conditions for TFNPcc -characterizations of total functions.

4.2

Complete Problems give TFNP Characterizations

Our first characterization of mpc measures with TFNPcc connections involves two properties:′i) Closed under reductions. Say that an mpc is closed under reductions if for any h : {0, 1}n → {0, 1}nthat is computable by monotone Boolean circuits of depth d, and any partial monotone function f onn′ bit inputs, mpc(f ◦ h) ≤ poly(n, n′ , mpc(f ), 2d ).
ii) Admits a complete family. A complete family for an mpc is a family Fm of partial functions on
N (m) ≤ quasipoly(m) bit inputs such that for every partial monotone function f with mpc(f ) ≤ m,there is a polylog(m)-depth monotone circuit computing a function h so that Fm ◦ h solves f , andmpc(Fm ) ≤ quasipoly(m).6
The following theorem states that these conditions suffice for a TFNPcc characterizations.
Theorem 23. Let mpc be a complexity measure. Then there is a paddable sequence of TFNPcc problems
Rn which characterizes mpc iff (i) and (ii) hold. Moreover, the sequence Rn can be made explicit (i.e.,
computably described) iff the sequence of complete functions for f can be made explicit.
A key component of the proof is the following lemma which says that reductions between monotone
Karchmer Wigderson games and monotone reductions between functions are identical. Note that while thisis intuitive and has a simple proof, the proof does not seem to extend to non-monotone complexity. Thismight be an important distinction between monotone and non-monotone circuit complexity.
6
Note that in the definition of admitting a complete family we are insisting that f reduce to Fm for an m only dependent on its
complexity, not its input size. Most natural notions of circuit complexity have circuit size be always at least the number of bits thefunction actually depends on, and the reduction can ignore the irrelevant bits, so this should not usually be a problem.

36Lemma 24. Let f and g be monotone partial Boolean functions. Then M KWf has a communication-t
mapping reduction to M KWg iff there is a function h computable by a depth-t monotone circuit so that g ◦ hsolves f .
Proof. As before, let Yesf , Nof and Yesg , Nog be the set of accepting and rejecting inputs of f and grespectively.
For the if direction, suppose that there is a function h computable by depth-t monotone circuits suchthat g ◦ h solves f . From this, we define a reduction from M KWf to M KWg as follows. Define the both of
the function MX and MY as h; it remains to define S. Since g ◦ h solves f , for every (x, y) ∈ Nof × Yesf ,we have (h(x), h(y)) ∈ Nog × Yesg . Thus, (h(x), h(y)) is a valid input to M KWg . A solution to M KWg
on this input is a bit position i such that h(x)i < h(y)i . Let hi be the partial function, defined on inputs in
Nof ∪ Yesf , which outputs the i-th bit of h. Since h is computable by depth-t monotone circuits, so is hi .
Thus, by the Karchmer-Wigderson transformation [35], there is a t-bit communication protocol Si (x, y) for
M KW hi . Following this protocol on any input (x, y) for which h(x)i < h(y)i will output a position j suchthat xj < yj , which is a solution to M KWf . Thus, we can define S as follows: on input (x, y, i) it runs
Si (x, y) and outputs the answer.
Conversely, suppose that we have a t-bit communication reduction MX , MY , S(x, y, i) from M KWf to
M KW g . From the protocol S, which maps solutions i to M KW g on input MX (x), MY (y) back to solutions
S(x, y, i) to M KWf on input (x, y), we construct a function h computable with depth-t monotone circuits
such that g ◦ h solves f . For each i, consider the monotone partial function Hi whose no-inputs are the x
for which there is an x ≤ x′ with x′ ∈ Nof and MX (x′ )i = 0, and whose yes-inputs are those y for which
there is y ≤ y ′ with y ′ ∈ Yesf and MX (y ′ )i = 1; we call such an input pair a dominating and dominatedpair for Hi .
By the definition of reduction, whenever x′ ∈ Nof , MX (x′ )i = 0, y ′ ∈ Yesf and MY (y ′ )i = 1, thecommunication protocol S(x′ , y ′ , i) returns a position j with x′j < yj′ . Given any input pair (x, y) to
M KW f where there is a dominating and dominated pair (x′ , y ′ ) for Hi as above, the parties can, without
communication, find x′ and y ′ respectively and then run the protocol S(x′ , y ′ , i) to obtain the index j.
By definition, xj ≤ x′j < yj′ ≤ yj , so this modified protocol solves the M KWHi game. Therefore, by
the Karchmer-Wigderson transformation [35], there is a depth-t monotone circuit computing a function hithat rejects all x ∈ Nof with MX (x)i = 0 and accepts all y ∈ Yf with MY (y)i = 1; it follows thathi (x) ≤ MX (x)i for all x ∈ Nof , and if y ∈ Yesf then MY (y)i ≤ hi (y). Letting h = (h1 , . . . , hn ),where n is the number of input bits to f , we have that for each x ∈ Nof , h(x) ≤ MX (x) ∈ Nog , so by
monotonicity of g, h(x) ∈ Nog . Similarly, if y ∈ Yesf , MX (y) ≤ h(y) and h(y) ∈ Yesg . Thus, g ◦ h solves
f and g is computable by depth-t monotone circuits.
We will now use the lemma to prove the theorem.
Proof of Theorem 23. Let mpc be a complexity measure with properties (i) and (ii) and let Fm be thecomplete family of partial monotone functions guaranteed by (ii). Let Rm := M KWFm be the monotone Karchmer-Wigderson game for Fm . Observe that as Fm is complete, it reduces to Fm′ for all m′ ≥mpc(Fm ) = quasipoly(m) via depth-polylog(m′ ) reductions. Thus by Lemma 24, Rn = M KWFm reduces
to Rm′ = M KWFm′ with communication-polylog(m′ ) for all such m′ , and so R is paddable.
We claim that there is a complexity-c reduction from M KWf to R iff mpc(f ) = polylog(c). Lettingm = mpc(f ), f reduces to Fm with a polylog(m)-depth monotone circuit, as Fm is complete. Henceby Lemma 24, there is a polylog(m)-complexity reduction from M KWf to M KWFm with polylog(m). It
follows by definition that Rcc (M KWf ) ≤ polylog(m) = polylog(mpc(f )). In the other direction, supposethat there is a complexity c reduction from M KWf to M KWF . Then there are n, t with t + log n = c so that37

M KW f is t-communication reducible to M KW Fn . By Lemma 24, Fn ◦ h solves f for some depth-t circuit

h. By monotonicity under solutions, and closure under reductions,mpc(f ) ≤ mpc(Fn ◦ h) ≤ poly(mpc(Fn ), 2t ) = poly(n, 2t ) = 2O(c) .
Next we prove the converse direction of the theorem. Let Rn be any paddable sequence of communication TFNP problems and define a monotone partial function complexity measure mpc by letting
mpc(f ) := 2cfor every monotone partial function f , where c is a the complexity of reducing M KWf to Rn . By construction, mpc is monotone under solutions. We will show that mpc has the properties (i) and (ii). First, assumeg ◦ h solves f and h is computable by depth-t monotone circuits. Then by Lemma 24, M KWf has a t-bit
reduction to M KWg . As well, M KWg has a t′ bit reduction to Rn where t′ + log n is the complexity of
reducing M KWg to R. Stringing these together, f has a t + t′ bit reduction to Rn , and so the complexity of
reducing M KWf to R is ≤ t + t′ + log n = t + c, and mpc(f ) ≤ 2t mpc(g). Therefore, mpc is closed under
reductions.
Finally, we give a complete family for mpc. Let FN be the sequence of partial monotone functions
given by Lemma 22 such that RN is equivalent to M KWFN . Note that by definition FN has at most N 2t
many input bits where t = polylog(n) is the number of bits that need to be communicated in order to verify
solutions to RN . As well, letting c be the complexity of reducing M KWFN to R, we have mpc(FN ) = 2c ≤2t = quasipoly(N ).
We will show that for each m, there is an N ′ = quasipoly(m) so that every partial function f withmpc(f ) ≤ m reduces to FN ′ via a polylog(m)-depth reduction. Fix some f with mpc(f ) ≤ m and let
c = log mpc(f ). Then by definition of mpc, M KWf reduces to some Rn in t bits of communication, wheret + log n = c; in particular, t is at most M and log n ≤ c. Then by paddability, we can reduce this to some
RN ′ where N ′ = quasipoly(n) ≤ quasipoly(c) is a fixed function of m, and the further communication is
at most polylog(c). Then by Lemma 24, f has a polylog(c)-depth circuit reduction to FN ′ as desired. Thus,
mpc is closed under reductions and admits a complete family.

4.3

A Partial Characterization for Complexity Measures on Total Functions

Analogous to measures on partial functions, let a monotone (total function) complexity measure mc map
total monotone functions to non-negative integers. From any mc we can extract a monotone complexity
measure mpc on partial functions by
mpc(F ) := min{mc(f ) : total f solving F }.
Observe that mpc will always satisfy monotonicity under solutions because if g solves f , the set of total
functions that solve g is a subset of those that solve f , so the min for g will be at least that for f .
Generalizing the definition for partial functions, say that a monotone complexity measure mc has acomplete family if there is a family of total monotone functions Fm such that for every total monotonefunction f on n bit inputs with mc(f ) ≤ m, there is a log m-depth monotone circuit computing a function
h so that Fm ◦ h solves f , and mc(Fm ) ≤ poly(m).
We will prove the following lemma, whose corollary gives sufficient conditions for a monotone complexity measure to give rise to a corresponding TFNPcc subclass.
Lemma 25. mpc is closed under reductions and has a complete (partial function) family if and only if mc
is closed under reductions and has a complete total function family.
38

An immediate consequence is the following.
Corollary 26. If a monotone complexity measure mc is closed under reductions and has a complete family, then it has a TFNPcc characterization by a sequence of paddable relations. If not, mc has no suchcharacterization.
This still leaves open the possibility that there is a characterization of the complexity measure that does
not extend to partial functions for some complexity measures without complete problems.
Proof of Lemma 25. To prove the lemma, we will first assume mc is closed under reductions, e.g., mc(f ◦h) ≤ poly(mc(f ), 2d ) when h is computable in depth d. Let F be a partial function, and let f be a total
function of minimal complexity solving F . Then f ◦ h solves F ◦ h, so mpc(F ◦ h) ≤ mc(f ◦ h) ≤poly(mc(f ), 2d ) = poly(mpc(F ), 2d ). Conversely, since mpc(f ) = mc(f ) for total functions, it follows
immediately that if mpc is closed under reductions, then so is mc.
If Fm is a family of complete partial functions for mpc, let fm be the corresponding minimal complexity
total functions solving Fm . Note that mc(fm ) = mpc(Fm ) = quasipoly(m). Let g be any total function
and let m = mpc(g) = mc(g). Then there is a function h computable by polylogm-depth monotone circuits
such that Fm ◦ h solves h. Furthermore, fm ◦ h solves Fm ◦ h, and so fm ◦ h solves g. However, the only
way for one total function to solve another is if they are equal, so fm ◦ h = g. It follows that fm is also
complete and, by assumption, is total.
Conversely, if fm is complete for mc, then let G be any partial function, let g be a minimal complexity
total function solving G, and let m = mpc(G) = mc(g). Then g = fm ◦ h for some function h computable
by polylogm-depth circuits, and so solves G. Thus, fm is also complete for mpc.

4.4

Universal Functions vs. Complete Functions

We can simplify the condition that there be complete functions in the class to having universal families offunctions, replacing (ii) in Theorem 27 by the following:ii† ) Admits a Universal Family. Let Fm be a sequence of partial monotone functions, and let mpc be acomplexity measure on such functions. We say Fm is universal for mpc if whenever mpc(g) ≤ m ,there is a fixed string zg so that F (x ◦ zg ) solves g(x), and mpc(Fm ) ≤ quasipoly(m).
Observe that such a universal family Fm can be viewed as complete under depth 0 reductions.
Theorem 27. Let mpc be a monotone partial function complexity measure satisfying (i) and (ii). Then mpc
admits a universal family if and only if it admits a complete family.
Using Lemma 25, we can derive an analogous statement to Corollary 26 for total functions as well.
Next, we state Theorem 3 formally, which follows immediately from Theorem 27 and Theorem 23.
Theorem 28. Let mpc be a complexity measure. Then there is a paddable sequence of TFNPcc problems
Rn which characterizes mpc iff (i) and (ii† ) hold. Moreover, the sequence Rn can be made explicit (i.e.,
computably described) iff the sequence of complete functions for f can be made explicit.
Proof of Theorem 27. If there is a universal family Fm for mpc then we can let Gm = Fm since Fm iscomplete under depth 0 reductions.
Conversely, say that a monotone partial complexity measure mpc admits a complete family under d(m)depth reductions if there exists a family Gm of functions such that mpc(Gm ) ≤ 2d(m) and for every partial
39monotone function f with mpc(f ) ≤ m, there is a depth-d(m) monotone circuit computing a function hso that Gm ◦ h solves f . Suppose that Gm (x) is complete under depth d(m) reductions, where the input
size |x| = M ≤ poly(m). We want to construct a partial function Fm which can code any composition
g(x) = Gm (h(x)) for any g with mpc(g) ≤ m and for any h computable by monotone circuits of depth
at most d(m). We will actually end up coding a more powerful set of reductions, because we cannot code
exactly this family and be monotone. Observe that h has at most m input bits, M output bits, and at most
2d(m) gates total. Thus, we can embed h into a depth-2d(m) alternating unbounded fan-in ∧-∨ circuit withm inputs, M outputs, and 2d(m) M gates at each intermediate level. We can represent the connectivity of theembedding by having one bit for each pair of gates, including inputs and outputs, saying whether the earlier
gate is an input to the later one.
So, we let Fm be a partial monotone function with m + (m + (2d(m) − 2)M 2d(m) + M )2 inputs. The
first m inputs to Fm code the input x to g, and the other bits, denoted Bi,j , code the connectivity relation forthe circuit computing h. The gates at even levels will be ∨-gates, and those at odd levels ∧-gates. Because
we need the circuit evaluation problem to be monotone, we cannot enforce that each gate has exactly two
incoming wires, so we allow the gates to be arbitrary fan-in instead. If j is a gate on an even levels, for each
earlier gate i including input positions, we let Bi,j be 1 if i is an input to j and 0 otherwise. For odd levels,
we reverse the roles of 0 and 1.
To compute Fm , we work our way up the circuit computing a bit Hi for each gate i. W
For i in the firstlevel, Hi is the i-th input
bit
(the
i-th
bit
of
x.
For
other
levels,
we
use
the
rule
H
=
(Hi ∧ Bi,j ) atjVeven levels, and Hj = (Hi ∨ Bi,j ) at odd levels, where the scope of i is all gates at earlier levels. Aftercomputing the values Hj for the gates at the top level, we apply Gm to the result.
By construction, Fm reduces to Gm via a depth 4d(m) monotone circuit with fan-in M 2d(m) ∧’s and∨’s, which can also be computed by a depth 4d(m)(d(m)+log M ) depth fan-in two monotone circuit. Thus,by composition with reductions, mpc(Fm ) is quasi-polynomial in m. Also, for any g with mpc(g) ≤ m,g can be solved by F ◦ h where h can be computed by monotone depth-d circuits. The input zg includes
the values Bi,j according to the connectivity for h; unused bits in zg can be set to 0. By construction,
Fm (x ◦ zg ) = Gm (h(x)) which solves g.

Future Directions
The TFNP connection, mapping proof systems to circuit lower bounds via lifting, has been extremely
successful. Our results show that this TFNP connection is generic , and characterize the conditions underwhich it can be made. However, there are many gaps left in making these lower bounds systematic rather
than ad hoc, and extending them to new models of computation and proof systems.
In particular,
1. We have a generic relationship between proof systems and decision tree TFNP problems, and ageneric relationship between monotone circuit complexity problems and circuit lower bounds. Can
we complete the chain by proving a generic lifting theorem, and show that for each TFNP problem,
lower bounds for the corresponding proof systems and complexity measures are equivalent?
2. Our characterization of proof systems that correspond to TFNP problems involves proving their own
soundness. Can we use this to show a version of Gödel’s second incompleteness theorem, that some
proof systems cannot prove their own soundness because they do not have a tight TFNP connection?
3. TFNP has a direct connection to monotone complexity via the monotone KW games. Can we similarly characterize the class of communication problems corresponding to non-monotone KW games?
404. We showed that reductions between the monotone KW games were equivalent to small depth monotone reductions between the corresponding functions. Does this extend to non-monotone games andnon-monotone reductions? If not, can we give an example of functions with reductions between the
KW games and no reductions between the corresponding functions? (Since this is interesting evenfor sub-logarithmic bit reductions, this could possibly be shown unconditionally without proving new
formula lower bounds.)
5. Our characterization of the Polynomial calculus looks superficially similar to PLSPPA : PLS provides
the dag-like structure, while each inference is a matching (a PPA instance). Can one prove a separation
between F2 -PC and PLSPPA ? If so, what is the proof system corresponding to PLSPPA ?
Acknowledgements
Noah Fleming was supported by NSERC. Russell Impagliazzo was supported by NSF CCF 2212135 andthe Simons Foundation. The authors thank Robert Robere and William Pires for comments on an earlier
version of this paper.

References[1] Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the Association for
Computing Machinery, 67(5):31:1–31:17, 2020.
[2] 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.
[3] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relativecomplexity of NP search problems. J. Comput. Syst. Sci., 57(1):3–19, 1998.
[4] Arnold Beckmann and Sam Buss. The NP search problems of frege and extended frege proofs. ACM
Trans. Comput. Log., 18(2):11:1–11:19, 2017.
[5] Arnold Beckmann and Samuel R. Buss. The NP search problems of Frege and extended Frege proofs.
ACM Transactions on Computational Logic, 18(2):Article 11, 2017.
[6] Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small
coefficients. J. Symb. Log., 62(3):708–728, 1997.
[7] Josh Buresh-Oppenheim and Tsuyoshi Morioka. Relativized NP search problems and propositional
proof systems. In 19th Annual IEEE Conference on Computational Complexity (CCC 2004), 21-24
June 2004, Amherst, MA, USA, pages 54–67. IEEE Computer Society, 2004.
[8] Samuel R. Buss. The Boolean formula value problem is in ALOGTIME. In Proceedings of the 19-th
Annual ACM Symposium on Theory of Computing, pages 123–131, May 1987.
[9] Samuel R. Buss, Leszek Aleksander Kolodziejczyk, and Neil Thapen. Fragments of approximate
counting. J. Symb. Log., 79(2):496–525, 2014.
[10] 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.
41

[11] Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of theSeventh Annual ACM Symposium on Theory of Computing, pages 83–97. Association for Computing
Machinery, 1975.
[12] Ben Davis and Robert Robere. Colourful TFNP and propositional proofs. In Amnon Ta-Shma, editor,
38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264
of LIPIcs, pages 36:1–36:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
[13] Susanna F. de Rezende, Mika Göös, and Robert Robere. Guest column: Proofs, circuits, and communication. SIGACT News, 53(1):59–82, 2022.
[14] Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The power of negative reasoning. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021,
July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 40:1–
40:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[15] 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 Sandy Irani, editor,
61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA,
November 16-19, 2020, pages 24–30. IEEE, 2020.
[16] Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How limited interaction hinders realcommunication (and what it means for proof and circuit complexity). Electron. Colloquium Comput.
Complex., page 6, 2021.
[17] Noah Fleming. The Proof Complexity of Integer Programming. PhD thesis, University of Toronto,
Canada, 2021.
[18] Noah Fleming, Mika Göös, Stefan Grosser, and Robert Robere. On semi-algebraic proofs and algorithms. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference,
ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 69:1–
69:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[19] Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere. Black-box PPP is not turingclosed. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual
ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024,
pages 1405–1414. ACM, 2024.
[20] Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm
design. Found. Trends Theor. Comput. Sci., 14(1-2):1–221, 2019.
[21] Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are
hard for cutting planes. J. ACM, 69(3):19:1–19:32, 2022.
[22] Anna Gál. A characterization of span program size and improved lower bounds for monotone span
programs. Comput. Complex., 10(4):277–296, 2001.
[23] Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds fromresolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA,
June 25-29, 2018, pages 902–911. ACM, 2018.
42

[24] Michal Garlik. Resolution lower bounds for refutation statements. In Proc. 4 Intl. Symp. on Mathematical Foundations of Computer Science (MFCS), pages 37:1–37:13, 2019.
[25] Paul Goldberg and Christos Papadimitriou. Towards a unified complexity theory of total functions.
Journal of Computer and System Sciences, 94:167–192, 2018.
[26] Paul W. Goldberg and Christos H. Papadimitriou. Towards a unified complexity theory of total functions. Electron. Colloquium Comput. Complex., page 56, 2017.
[27] Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere,
and Ran Tao. Separations in proof complexity and TFNP. CoRR, abs/2205.02168, 2022.
[28] Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity
and TFNP. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference,
ITCS 2019, January 10-12, 2019, San Diego, California, USA, volume 124 of LIPIcs, pages 38:1–
38:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
[29] Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. 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.
[30] Mika Göös, Shachar Lovett, Raghu Meka, Thomas Watson, and David Zuckerman. Rectangles arenonnegative juntas. SIAM J. Comput., 45(5):1835–1869, 2016.
[31] Mika Göös, Toniann Pitassi, and Thomas Watson. Deterministic communication vs. partition number.
SIAM J. Comput., 47(6):2435–2450, 2018.
[32] 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.
[33] Pavel Hubácek, Erfan Khaniki, and Neil Thapen. TFNP intersections through the lens of feasible
disjunction. In Venkatesan Guruswami, editor, 15th Innovations in Theoretical Computer Science
Conference, ITCS 2024, January 30 to February 2, 2024, Berkeley, CA, USA, volume 287 of LIPIcs,
pages 63:1–63:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
[34] Pritish Kamath. Some hardness escalation results in computational complexity theory. PhD thesis,
Massachusetts Institute of Technology, 2019.
[35] Mauricio Karchmer and Avi Wigderson. Monotone circuits for connectivity require super-logarithmic
depth. SIAM J. Discret. Math., 3(2):255–265, 1990.
[36] Pravesh K. Kothari, Raghu Meka, and Prasad Raghavendra. Approximating rectangles by juntas andweakly-exponential lower bounds for LP relaxations of CSPs. In Hamed Hatami, Pierre McKenzie,
and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory ofComputing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 590–603. ACM, 2017.
[37] Jan Krajı́cek. Interpolation theorems, lower bounds for proof systems, and independence results forbounded arithmetic. J. Symb. Log., 62(2):457–486, 1997.
43

[38] Jan Krajı́cek. Interpolation by a game. Math. Log. Q., 44:450–458, 1998.
[39] Jan Krajı́cek. Randomized feasible interpolation and monotone circuits with a local oracle. J. Math.
Log., 18(2):1850012:1–1850012:27, 2018.
[40] James R. Lee, Prasad Raghavendra, and David Steurer. Lower bounds on the size of semidefinite
programming relaxations. In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the
Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA,
June 14-17, 2015, pages 567–576. ACM, 2015.
[41] Yuhao Li, William Pires, and Robert Robere. Intersection classes in TFNP and proof complexity. In
Venkatesan Guruswami, editor, 15th Innovations in Theoretical Computer Science Conference, ITCS
2024, January 30 to February 2, 2024, Berkeley, CA, USA, volume 287 of LIPIcs, pages 74:1–74:22.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
[42] László Lovász, Moni Naor, Ilan Newman, and Avi Wigderson. Search problems in the decision treemodel. SIAM J. Discret. Math., 8(1):119–132, 1995.
[43] Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS
2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 104:1–104:24.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[44] Toniann Pitassi and Robert Robere. Lifting nullstellensatz to monotone span programs over any field.
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 1207–1219. ACM, 2018.
[45] Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J.
Symb. Log., 62(3):981–998, 1997.
[46] Pavel Pudlák. On the complexity of finding falsifying assignments for herbrand disjunctions. Arch.
Math. Log., 54(7-8):769–783, 2015.
[47] Pavel Pudlák and Jirı́ Sgall. Algebraic models of computation and interpolation for algebraic proof
systems. In Paul Beame 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.
[48] Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Comb., 19(3):403–435,
1999.
[49] Alexander Razborov. Unprovability of lower bounds on circuit size in certain fragments of boundedarithmetic. Izvestiya Mathematics, 59(1):205–227, 1995.
[50] 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 ofComputer Science, FOCS 2016, 9-11 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA,pages 406–415. IEEE Computer Society, 2016.
44

A

Bounded-Width Resolution Proves its Reflection Principle

In this section we verify Theorem 10 by showing that resolution can indeed prove its own reflection principle,
when measuring this complexity parameter. This corresponds to showing that polylog(n)-width resolution
can prove its own reflection principle. A resolution proof of an unsatisfiable set of Clauses F is a derivationof the empty clause ⊥, which contains no literals, by the following inference rule:– Resolution rule. From C ∨ x and C ∨ x derive C.
The size of a resolution proof Π is the number of applications of the resolution rule, while the width is the
maximum number of literals in any clause in the proof. The complexity of proving F in resolution isRes(F ) := min log size(Π) + width(Π).
Π

Theorem 29. There is a reflection principle Ref Res for resolution such that Res(Ref Res ) ≤ polylog(n).
We define Ref Res by giving a natural verification procedure for resolution proofs.
(H, Π),A Verification Procedure for Resolution. The verification procedure V Res (H, Π) := VnRes
H ,mH ,ccencoding a proof of size s = 2 and width w = c, is defined by the following variables and constraints.
Variables: V Res describes the proof Π with the following variables. Each line ℓ ∈ [s] is given by a length-w(ℓ)
vector V (ℓ) where Vi ∈ [2nH + 1] indicates the ith literal in line ℓ. The values 1, . . . nH enumerate thepositive variables, while nH + 1, . . . 2nH enumerate the negative literals. Finally, the value 2nH + 1 denotes
the absence of this literal from ℓ.
The line 1 will correspond to the root of the proof (⊥) and the lines s − mH + 1, . . . , s + mH will(ℓ) (ℓ)correspond to the clauses of H. For each ℓ ∈ [s − mH ], we have two predecessor pointers p1 , p2 ∈ [s],naming the two lines from which ℓ was derived by the resolution rule.
Constraints: The constraints of V Res are the following:(1)– Final Line. There are constraints saying that the final line 1 contains no variables: Vifor all i ∈ [w].

= 2nH + 1

– Axioms. For each i ∈ [mH ] line ℓ = s − i + 1, we have constraints stating that the ℓth line is exactly(i)the ith clause of H. In particular, for each j ∈ [w], the variable Ci,j of the formula Sat equals Vj .
(ℓ)

(ℓ)

– Inferences. For each line ℓ ∈ [s − mH ] we have constraints saying that p1 , p2 > ℓ, and a set of(ℓ) (ℓ)constraints saying that ℓ must be correctly derived from p1 , p2 . In particular, we have constraints
(ℓ)

(ℓ)

stating that V (p1 ) and V (p2 ) contain complimentary literals and that V (ℓ) contains exactly the literals(ℓ)(ℓ)
of V (p1 ) and V (p2 ) after cancelling these complimentary literals. To see that this can be expressed as(ℓ) (ℓ)a not-too-large CNF formula, observe that for each value of p1 , p2 , these constraints can be defined
(ℓ)

(ℓ)

(ℓ)

(ℓ)

by a decision tree querying p1 , p2 , V (p1 ) , V (p2 ) , which involve t = O(log(s + mH ) + w log nH )many variables. Hence can be described by a CNF formula of width t and s2 2t -many clauses, whichis quasi-polynomial in the number of variables.
In order to prove Theorem 29 we will use the following characterization of resolution due to [9].
Fact 30. S EARCHF ∈ PLSdt iff Res(F ) = polylog(n).
A complete problem for the class PLS is I TER, which states that every dag has a sink.
45

Iteration. An instance of I TERn is given by a successor function s : [n] → [n]; we think of S as defining a
directed graph on the vertices [n], where there is an edge (u, v) if S(u) = v. A vertex v ∈ [n] is a solution if:– Source Violation. If v = 1 and S(1) = 1.
– Sink Violation. If S(v) ̸= v and S(S(v)) = S(v).
– Direction Violation. If S(v) < v.
Hence, it suffices to give a reduction from Ref Res to I TER.
Proof of Theorem 29. We give a reduction from Ref Res := V Res ∧ Sat to an instance of I TER on s-manynodes. Let n be the total number of variables of Ref Res and let (H, Π, α) be an assignment to Ref Res .
– Non-leaf Nodes. For each node ℓ ∈ [s − mH ], we define the successor S(ℓ) as follows: first, we
check whether the clause encoded by V (ℓ) is satisfied by the assignment α, querying the at-most-w
variables mentioned in V (ℓ) . If it is, then we set S(ℓ) = ℓ. Otherwise, we check whether the inference
(ℓ)

(ℓ)

(ℓ)

(ℓ)

constraints of ℓ are violated. This is done querying p1 , p2 and V (p1 ) , V (p2 ) . If an inference
constraint is violated then we set S(ℓ) = 1 to force a direction violation. Otherwise, by soundness(ℓ) (ℓ)of the resolution rule, one of p1 , p2 must be falsified. To determine which one, we query the bits
(ℓ)

(ℓ)

(ℓ)

of α corresponding to the literals specified by V (p1 ) , V (p2 ) . If p1 is falsified by α, then we set(ℓ)(ℓ)S(ℓ) = p1 , and otherwise we set S(ℓ) = p2 .
Observe that s(ℓ) can be defined by a polylog(n)-depth decision tree. Indeed, the number of variables
queried in this process is O(log s + w log nH ).
(1)– Root. To define S(1), we also check that for all i ∈ [w], Vi = 2nH + 1. If this is not the case, thenwe set S(1) = 1 to force a source violation. Otherwise, we define S(1) as in the non-leaf case.
– Axioms (Leaf Nodes). For i ∈ [mh ], we define S(s − i) by querying the variables of V (s−i) and thevariables Ci,j for all j ∈ [w] encoding clause i of H in Sat. If these name different literals, then we(s−i)
set S(s − i) = 1 to force a direction violation. Otherwise, S(s − i) = s − i. As both Vj
and Ci,j
are encoded using O(log nH )-many variables, this can be done with a polylog(n)-depth decision tree.
Observe that sink violations can only at the nodes v such that S(v) = s − i for some i ∈ [mH ].
It remains to define the output decision trees Tvo for each solution v ∈ [s]. These decision trees will
first query the decision tree for S(v) and S(S(v)). If we see a direction violation or a source violation, thenby definition of S, we must have observed that a Inference, Axiom, or Final Line constraint of Ref Res was
violated and Tvo outputs the index of that constraint. Otherwise, if we see a sink violation then S(v) = s − ifor some i ∈ [mH ]. At this point, we have queried the variables Ci := {Ci,j : j ∈ [w]} and the bits of αcorresponding to the variables in Ci . We claim that Ci (α) = 0. Indeed, as S(v) = s − i, the clause encodedby V (s−i) must have be falsified by α, and as we did not violate any Final Line constraints, we know that
V (s−i) = Ci , and hence Ci is falsified by α. Thus Tvo can output the index of the constraint of Sat statingthat clause i must be falsified by α.

B

Characterization of the Unary Polynomial Calculus

In this appendix we prove Theorem 20, which we break into the following two lemmas. Recall that thelength of a uPC proof is the number of lines (deductions) in the proof.
46

Lemma 31. Let F be an unsatisfiable CNF formula on n variables. If there is a uPC proof of F withsize-s, length-L, and degree-d then there is a depth-O(d) decision-tree reduction from SF to an instance of
I ND E ND - OF -L INE on O(sL) many variables.
Proof. Fix a uPC proof Π of F and fix a topological ordering on the lines of Π with the first line being the
1 polynomial. For each monomial m that appears in Π, let cm be the maximum P
a absolute value of any
coefficient of m in Π. Let the number of nodes of our I ND EOL instance be N := m cm and the numberof pools be L. That is, each pool will have one node for each possible occurrence of m in the correspondingline.
The proof is identical to the proof of Lemma 15, except that we need to specify the direction of eachmatching. Fix any assignment x ∈ {0, 1}n to F . The edges E : [L] → [L] × [L] will be defined exactly as
they were in the characterization of F2 -PC:
– If v is an axiom, then E(v)(x) = (v, v) always.
– If v was derived by addition from lines u, w in Π then E(v)(x) = (u, w) always.
– If v was derived from u by multiplication by a variable xi , then the decision tree E(v)(x) queries xi
and outputs v if xi = 0 and otherwise it outputs u. That is, v becomes a leaf if xi = 0.
For every line v ∈ [L] of Π, there will be a one-to-one correspondence between the monomials in v (thoughtof as a multi-set) that are non-zero under x and the nodes that appear in Pv , and hence we abuse notation
and refer to nodes as “monomials”. To ensure that this is the case, and to avoid consistency violations, forevery pool u ∈ [L] and every monomial m ∈ [N ] that does not occur in u, we fix M (v) (u, m) = (u, m, +).
Note that the + is arbitrary, it would have been equally valid to set it to−. If m occurs in line v, then query
the at most d-many variables of x that define m. If m(x) = 0 then we set M (v) (u, m) = (u, m, +) (whereagain + is arbitrary). Otherwise, if m(x) ̸= 0, then we set M (v) (u, m) as follows:– Addition: If v was derived by addition from lines u and w then if m is a b-monomial in v, for b ∈{−, +}, then m came from either u or w. Suppose that it was u, then we set M (v) (v, m) = (u, m, b)
where b = {+, −} \ b, and M (v) (u, m) = (v, m, b).
The remaining monomials m in u which have not yet had their matching defined must have cancelledwith a monomial in w of the opposite polarity during the addition. If m is a b-monomial for b ∈{−, +}, then we set M (v) (u, m) = (u, m, b) = (w, m, b).
– Multiplication: If v is derived from u by multiplication by variable xi , then the decision tree for each
M (v) (z, m) for z ∈ {v, u} and monomial m begins by querying xi . If xi = 0 then M (v) (z, m) =(z, m). Otherwise if xi = 1, then for every monomial xi m in v, there is some m′ equal to m or xi m inu which xi m comes from and we match M (v) (v, m) = (u, m′ , −) and M (v) (u, m′ ) = (v, mxi , +).
Finally, we must be able to pair-off the monomials in u that have yet to be matched into pairs (m, mxi )into pairs which cancel after multiplication by xi . That is, one monomial in the pair must be positive
and the other negative. Suppose that b ∈ {−, +} is the polarity of m. We match M (v) (u, m) =(u, mxi , b) and M (v) (u, mxi ) = (u, m, b).
– Axioms: If v is an axiom in Π, then v = C for some C ∈ F . For each monomial m ∈ C, M (v)queries the at-most-d bits of x corresponding to the variables in C to get an assignment α. If C(x) =C(α) = 1 then C(x) = 0 and we have found a solution to S EARCHF , so we match M (v) (v, m) insome way that creates a violation; for example M (v) (v, m) = (1, 1, +).
47

Otherwise, if C(x) = 0 then either m(α) = 0, and we have set M (v) (v, m) = (v, m, +), or wem(α) ̸= 0. If the latter is the case then as C(x) = 0, the monomials of C must cancel to 0. Hence,
there must be another monomial m′ in v such that m ↾ α = m′ ↾ α, and such that if m is a bmonomial, for b ∈ {−, +}, then m′ is a b-monomial. Hence, we set M (v) (v, m) = (v, m′ , b) andM (v) (v, m) = (v, m, b).
Finally, observe that the only violations occur at the pools corresponding to the axioms. Therefore, theoutput decision trees are defined identically to the proof of Lemma 15.
Lemma 32. Let F be an unsatisfiable CNF formula. If S EARCHF reduces to an instance of I ND EOL on nvariables using depth-d decision trees, then there is an degree-O(d) and size n2 2O(d) uPC proof of F .
Proof. Let F = C1 ∧ . . . ∧ Cm be an unsatisfiable CNF formula such that S EARCHF reduces to I ND L EAFn
using decision trees {Ti }, {Tjo } of depth at most d. Let L be the number of pools and N the number ofnodes of the I ND L EAFn instance. For each pool v ∈ [L] consider the polynomial
X
X
Pv : =[[M (v) (v, m) = (u, m′ , −)]] − [[M (v) (v, m) = (u, m, +)]]m∈[N ] (u,m′ )̸=(v,m)

which records the difference between the number of positive monomials and negative monomials in line v.
Using this reduction, we will prove F in uPC by deriving that Pv = 0 by induction from v = L, . . . 1.
Claim 33. For each v ∈ [L], there is a degree O(d), size N L2O(d) uPC proof of the polynomial Pv from F .
This suffices to complete the proof of the lemma, as once we have derived P1 , we can derive P1 − 1from the axioms of I ND EOL in order to complete the proof.
Claim 34. There is a degree O(d), size N 2O(d) uPC derivation of the polynomial P1 − 1 from F .
Having derive P1 and P1 − 1, we add them together to obtain 1, completing the proof.
We will now prove the outstanding claims, which rely on the following Key Observation. Let β be asolution to I ND EOL (either a dag, root, matching violation, or consistency), the indicator of the solution β
is the minimal conjunct Iβ such that Iβ (x) = 0 iff x ↾ Vars(β) = β.
Key Observation: If Q is any conjunct such that there is a solution β with Iβ ⊆ Q then Q has a uPC proofof degree O(d + deg(Q)) and size O(|Q|2d ) from the axioms of F .
Proof. Let Tβo be the output decision tree for the solution β. As Iβ ⊆ Q, any assignment x which falsifies
Q must witness the solution β. Let k the index of the clause of F output by Tβo (x). By the soundness of
the reduction, C k (x) = 0. Hence, whenever Q · [[Tβo = k]] is falsified, C k is falsified as well. Putting this
together,X
Q=
Q · [[Tβo = k]](Summing all the root-to-leaf paths in Tβo gives 1)
k∈[m]

=

X

C k = 0.

(C k is an axiom of F )k∈[m]

As Tβo has depth at most d, it has at most 2d -many leaves, and the bound on the degree and size follows.

48

Proof of Claim 34. It suffices to express
X
X[[M (1) (1, m) = (u, m′ , −)]] − [[M (1) (1, m) = (u, m′ , +)]] − 1
P1 − 1 :=m∈[N ] (u,m′ )̸=(1,m)

as a low-degree polynomial in which each term involves one of the axioms C i of F . Any assignment to thevariables of F which satisfies one of these terms is a root violation, and hence a solution to I ND EOL. Sincesumming over all root-to-leaf paths in the decision tree M (1) (1, 1) gives 1, we have
X X X[[M (1) (1, 1) = (u, m, b)]] − 10=u∈[L] m∈[N ] b∈{+,−}

=

X

X

=

X

[[M

[[M (1) (1, 1) = (1, 1, b)]] − 1b∈{+,−}(u,m)̸=(1,1) b∈{+,−}X

X[[M (1) (1, 1) = (u, m, b)]] +(1)(1, 1) = (u, m, b)]] + 0 − 1(Key Observation)(u,m)̸=(1,1) b∈{+,−}=X(u,m)̸=(1,1)=

X[[M (1) (1, 1) = (u, m, −)]] +X[[M (1) (1, 1) = (u, m, +)]] − 1(u,m)̸=(1,1)

[[M

(1)

(1, 1) = (u, m, −)]] − 1(Key Observation)(u,m)̸=(1,1)=

X[[M (1) (1, 1) = (u, m, −)]] −X

X[[M (1) (m′ , u) = (u, m, +)]] − 1

m′ ∈[N ] (u,m)̸=(1,m′ )(u,m)̸=(1,1)(Key Observation)=X

X[[M (1) (1, m) = (u, m′ , −)]] − [[M (1) (1, m) = (u, m′ , +)]] − 1 (Key Observation)m∈[N ] (u,m′ )̸=(1,m)= P1 − 1.
This polynomial is the sum over O(N )-many pairs of decision trees (from the Key Observation), each of
depth d and therefore at most 2d -many leaves. Hence, this is a proof of degree O(d) and size at most
N 2O(d) .
Proof of Claim 33. Extend the definition of Pu to the matching for v, asXX
Pu(v) :=[[M (v) (u, m) = (w, m′ , −)]] − [[M (v) (u, m) = (w, m, +)]]m∈[N ] (w,m′ )̸=(u,m)

To facilitate a proof by induction, we will show that for every v ∈ [L], the following two polynomials havea size N 2 2O(d) and degree 4d proof from the axioms of F :


X
Pv −
[[E(v) = (u, w)]] Pu(v) + Pw(v)
(4)
u,w>v

X



[[E(v) = (u, w)]] Pu(v) − Pu

(5)

u,w>v

(4) expresses the correctness of the matching, while the (5) expresses that consistency is maintained — thesigns of monomials in a pool u do not switch between matchings.
49

Supposing that we can derive these polynomials efficiently from F , we complete the proof of the claim
by proving that Pv induction on v = L, . . . , 1. For the base case, when v = L, (4) is simply PL as there
does not exist any u, w > L.
Now, suppose that we have derived Pu for all u > v. Multiplying these by E(v) and summing givesX[[E(v) = (u, w)]] Pu + Pw
u,w>v



(v)
(v)
[[E(v) = (u, w)]] Pu + Pw

X=(Adding (5))

u,w>v

=Pv .

(Adding (4))

As for every u, w ∈ [L], (4) and (5) have degree 4d and N 2O(d) -size proofs from F , the total degree of theproof is O(d) and the size is at most N L2O(d) . It remains to show that (4) and (5) have efficient proofs fromF.
Equation 4. This polynomial states that the monomials in u and w cancel to give the monomials in v. To
derive (4), we will use the matching M (v) . The intuition is that if a monomial m in this matching is correctly
matched, then it is matched to −m and so they are identically 0, and we can derive them as such. If m isincorrectly matched, then this is a matching violation, which the output decision tree maps to a clause of F ,and hence we can derive it from this clause.


 X

X
P
(4) = Pv[[E(v) = (u, w)]] −[[E(v) = (u, w)]] Pu(v) + Pw(v)(As p∈E(v) p = 1)u,w>vu,w∈[L]

= Pv



= Pv

 X

X

[[E(v) = (u, w)]] +u<v∨w<vX
X[[E(v) = (u, w)]] −[[E(v) = (u, w)]] Pu(v) + Pw(v) ]

u,w>v



X

[[E(v) = (u, w)]] −

u,w>v

=

X

u,w>v



[[E(v) = (u, w)]] Pu(v) + Pw(v)(Key Observation)

u,w>v



[[E(v) = (u, w)]] Pv − Pu(v) − Pw(v)

u,w>v

=

X

[[E(v) = (u, w)]]

u,w>v

X

bz Pz(v)(6)

z∈{u,v,w}

where bz = 1 if z = v and bz = −1 otherwise. It remains to deduce (6) from the axioms of F . To do so, we
use the matching M (v) . Define the polynomial


X
X
X
matchv :=[[E(v) = (u, w)]]bz[[M (v) (z, m) ̸= (z, m, ∗)]]· matchvz,m,− −matchvz,m,+ .
u,w>v

z∈{u,v,w}m∈[N ]

where, for γ ∈ {−, +},X X
Xmatchvz,m,γ :=[[M (v) (z, m) = (a, α, b)]]a∈[L] α∈[N ]X

X[[M (v) (a, α) = (z ∗ , m∗ , b∗ )]],z ∗ ∈[L] m∗ ∈[N ] b∗ ∈{−,+}

|

{z

≡1

}

where the final part is equal to 1 as it is the sum over all paths in the decision tree for M (v) (a, α), and so(6) = matchv . To show that matchv has a proof from F , we break it into two multisets of conjuncts, V
50which contains the conjuncts which witness violations, and C which correspond to the correct matchings— those without violations. The conjuncts in V can be removed by the Key Observation — they can bederived from the clauses of F — while the conjuncts in C are correctly paired, meaning that each positive
occurence is paired with a negative occurence, and hence they sum to 0.
X
Xmatchv =
t+
t
t∈C

=

X

t∈V

t+0

(Key Observation)

t∈C

=

X



X

[[E(v) = (u, w)]]

u,w>v

X

[[M (v) (z, m) ̸= (z, m, ∗)]]·z∈{u,v,w} m∈[N ]

X X 

[[M

(v)

(z, m) = (a, α, −)]][[M (v) (a, α) = (z, m, +)]]a∈[L] α∈[N ]

− [[M

(v)

(z, m) = (a, α, +)]][[M(v)(a, α) = (z, m, −)]]



=0.
Finally, observe that each matchvz,m,γ is the sum over two decision trees, each of depth at most d and hence
size at most 2d . matchv is formed from matchvz,m,γ by querying E(v) and taking a sum over all monomialsm ∈ [N ], and hence has degree at most 3d and size N 2O(d) . Finally, the application of the Key Observation
introduces one additional decision tree, and so the proof of (4) has size N 2 2O(d) and degree at most 4d.
Equation 5. This polynomial states that if u is a child of v then the monomials in Pu occur with the samepolarity in the matching M (v) . For z ∈ {u, v} and γ ∈ {−, +}, let z = {u, v} \ z, and define
X
X
X
(z)
pol(z)
:=
[[M
(u,
m)
=
(a,
α,
γ)]]
[[M (z) (u, m) = (w, β, b)]],γm∈[N ] a∈[L],α∈[N ]w∈[L],β∈[N ]b∈{−,+}

|

{z

≡1

}

where the final sum is equal to 1 as it is the sum over all paths in a decision tree. Therefore, we can write




X
X
(v)
(v)
(u)
(u)
(5) =
[[E(v) = (u, w)]] Pu(v) − Pu =[[E(v) = (u, w)]] pol− − pol+ − pol− + pol+
u,w>v

u,w>v

(7)

51

(z)

(z)

We break each polγ into a multi-set of conjuncts Vγ containing the conjuncts which witness violations(z)— these will all be consistency violations — and Cγ which do not witness violations. Then (7) equals
 X
X
X
X
X
X
X
X
X 
[[E(v) = (u, w)]]
t−
t−
t+
t+
t−
t−
t+
t
u,w>v

=

X

(v)

[[E(v) = (u, w)]]

u,w>v

=

X
u,w>v

(v)

t∈C−

 X

t−

(v)
t∈C−

[[E(v) = (u, w)]]

(u)

t∈C+

 X
(v)

t∈C−

X

(u)

t∈C−

t−

(v)
t∈C+

X

(v)

t∈C+

X 
t +0

t+

(u)
t∈C−

t∈V−

(v)

t∈V+

(u)

t∈V−

(u)

t∈V+

(Key Observation)

(u)
t∈C+

X   X
X 
t−
t +
t−
t
(u)

t∈C+

(u)

t∈C−

(v)

t∈C+

=0.
We justify the final equality: as we have removed all of the consistency violations, for any monomial m ∈Pu , if it occurs at the head of an arrow in M (u) then it must occur at the tail of an arrow in M (v) , and(v)
vice-versa. Hence for every term t = [[M (z) (u, m) = (a, α, −)]][[M (z) (u, m) = (w, β, +)]] in C− , there is(u)a term t′ = [[M (z) (u, m) = (w, β, +)]][[M (z) (u, m) = (a, α, −)]] in C+ , and vice-versa. Thus, these terms
sum to 0.
Finally, observe that each pol is the sum over all monomials m ∈ [N ], and for each m we have two
decision trees, each of depth at most d. Thus, pol has size at most N 2O(d) and degree at most 2d. Then, (5)is obtained by querying the decision tree for E(v). Finally, the Key Observation introduces one additional
decision tree, and hence the proof of (5) has size N 2O(d) and degree at most 4d.

52