1 Introduction
In this work, we obtain strong tradeoffs in proof complexity by making a connection to pebble games played on graphs. In this introductory section we start with a brief overview of these two areas and then explain how our results follow from connecting the two.
1.1 Proof Complexity
Proof complexity is the study of efficiently verifiable certificates for mathematical statements. More concretely, statements of interest claim to provide correct answers to questions like:

Given a CNF formula, does it have a satisfying assignment or not?

Given a set of polynomials over some finite field, do they have a common root?
There is a clear asymmetry here in that it seems obvious what an easily verifiable certificate for positive answers to the above questions should be, while it is not so easy to see what a concise certificate for a negative answer could look like. The focus of proof complexity is therefore on the latter scenario.
In this paper we study the algebraic proof system system Nullstellensatz introduced by Beame et al. [BIKPP94LowerBounds]. A Nullstellensatz refutation of a set of polynomials with coefficients in a field is an expression
(1.1) 
(where are also polynomials), showing that lies in the polynomial ideal in the ring generated by . By (a slight extension of) Hilbert’s Nullstellensatz, such a refutation exists if and only if there is no common valued root for the set of polynomials .
Nullstellensatz can also be viewed as a proof system for certifying the unsatisfiability of CNF formulas. If we translate a clause like, e.g., to the polynomial , then an assignment to the variables in a CNF formula (where we think of as true and as false) is satisfying precisely if all the polynomials vanish.
The size of a Nullstellensatz refutation (1.1) is the total number of monomials in all the polynomials and expanded out as linear combinations of monomials. Another, more wellstudied, complexity measure for Nullstellensatz is degree, which is defined as .
In order to prove a lower bound on the Nullstellensatz degree of refuting a set of polynomials , one can construct a design, which is a map from degree polynomials in to such that

is linear, i.e., for ;

;

for all and such that ;

for all such that .
Designs provide a characterization of Nullstellensatz degree in that there is a design for if and only if there is no Nullstellensatz refutation of in degree [Buss98LowerBoundsNS]
. Another possible approach to prove degree lower bounds is by computationally efficient versions of Craig’s interpolation theorem. It was shown in
[PS98Algebraic] that constantdegree Nullstellensatz refutations yield polynomialsize monotone span programs, and that this is also tight: every span program is a unique interpolant for some set of polynomials refutable by Nullstellensatz. This connection has not been used to obtain Nullstellensatz degree lower bounds, however, due to the difficulty of proving span program lower bounds.Lower bounds on Nullstellensatz degree have been proven for sets of polynomials encoding combinatorial principles such as the pigeonhole principle [BCEIP98Relative], induction principle [BP98Good], housesitting principle [CEI96Groebner, Buss98LowerBoundsNS], matching [BIKPRS97ProofCplx], and pebbling [BCIP02Homogenization]. It seems fair to say that research in algebraic proof complexity soon moved on to stronger systems such as polynomial calculus [CEI96Groebner, ABRW02SpaceComplexity], where the proof that lies in the ideal generated by can be constructed dynamically by a stepbystep derivation. However, the Nullstellensatz proof system has been the focus of renewed interest in a recent line of works [RPRC16Exponential, PR17StronglyExponential, PR18LiftingNS, dRMNPRV19Lifting] showing that Nullstellensatz lower bounds can be lifted to stronger lower bounds for more powerful computational models using composition with gadgets. The size complexity measure for Nullstellensatz has also received attention in recent papers such as [Berkholz18Relation, AO19ProofCplx].
In this work, we are interested in understanding the relation between size and degree in Nullstellensatz. In this context it is relevant to compare and contrast Nullstellensatz with polynomial calculus as well as with the wellknown resolution proof system [Blake37Thesis], which operates directly on the clauses of a CNF formula and repeatedly derives resolvent clauses from clauses of the form and until contradiction, in the form of the empty clause without any literals, is reached. For resolution, size is measured by counting the number of clauses, and width, measured as the number of literals in a largest clause in a refutation, plays an analogous role to degree for Nullstellensatz and polynomial calculus.
By way of background, it is not hard to show that for all three proof systems upper bounds on degree/width imply upper bounds on size, in the sense that if a CNF formula over variables can be refuted in degree/width , then such a refutation can be carried out in size . Furthermore, this upper bound has been proven to be tight up to constant factors in the exponent for resolution and polynomial calculus [ALN16NarrowProofs], and it follows from [LLMO09Expressing] that this also holds for Nullstellensatz. In the other direction, it has been shown for resolution and polynomial calculus that strong enough lower bounds on degree/width imply lower bounds on size [IPS99LowerBounds, BW01ShortProofs]. This is known to be false for Nullstellensatz, and the pebbling formulas discussed in more detail later in this paper provide a counterexample [BCIP02Homogenization].
The size lower bounds in terms of degree/width in [IPS99LowerBounds, BW01ShortProofs] can be established by transforming refutations in small size to refutations in small degree/width. This procedure blows up the size of the refutations exponentially, however. It is natural to ask whether such a blowup is necessary or whether it is just an artifact of the proof. More generally, given that a formula has proofs in small size and small degree/width, it is an interesting question whether both measures can be optimized simultaneously, or whether there has to be a tradeoff between the two.
For resolution this question was finally answered in [Thapen16Tradeoff], which established that there are indeed strong tradeoffs between size and width making the size blowup in [BW01ShortProofs] unavoidable. For polynomial calculus, the analogous question remains open.
In this paper, we show that there are strong tradeoffs between size and degree for Nullstellensatz. We do so by establishing a tight relation between Nullstellensatz refutations of pebbling formulas and reversible pebblings of the graphs underlying such formulas. In order to discuss this connection in more detail, we first need to describe what reversible pebblings are. This brings us to our next topic.
1.2 Pebble Games
In the pebble game first studied by Paterson and Hewitt [PH70Comparative], one places pebbles on the vertices of a directed acyclic graph (DAG) according to the following rules:

If all (immediate) predecessors of an empty vertex contain pebbles, a pebble may be placed on .

A pebble may be removed from any vertex at any time.
The game starts and ends with the graph being empty, and a pebble should be placed on the (unique) sink of at some point. The complexity measures to minimize are the total number of pebbles on at any given time (the pebbling space) and the number of moves (the pebbling time).
The pebble game has been used to study flowcharts and recursive schemata [PH70Comparative], register allocation [Sethi75CompleteRegisterAllocation]
, time and space as Turingmachine resources
[Cook74ObservationTimeStorageTradeOff, HPV77TimeVsSpace], and algorithmic timespace tradeoffs [Chandra73Efficient, SS77SpaceTimeFFT, SS79SpaceTimeOblivious, SS83SpaceTimeLinear, Tompa78TimeSpaceComputing]. In the last two decades, pebble games have seen a revival in the context of proof complexity (see, e.g., [Nordstrom13SurveyLMCS]), and pebbling has also turned out to be useful for applications in cryptography [DNW05Pebbling, AS15HighParallel]. An excellent overview of pebbling up to ca. 1980 is given in [Pippenger80Pebbling] and some more recent developments are covered in the upcoming survey [Nordstrom09PebblingSurveyFTTCS].Bennett [Bennett89TimeSpaceReversible] introduced the reversible pebble game as part of a broader program [Bennett73LogicalReversibility] aimed at eliminating or reducing energy dissipation during computation. Reversible pebbling has also been of interest in the context of quantum computing. For example, it was noted in [Soeken1] that reversible pebble games can be used to capture the problem of “uncomputing” intermediate values in quantum algorithms.
The reversible pebble game adds the requirement that the whole pebbling performed in reverse order should also be a correct pebbling, which means that the rules for pebble placement and removal become symmetric as follows:

If all predecessors of an empty vertex contain pebbles, a pebble may be placed on .

If all predecessors of a pebbled vertex contain pebbles, the pebble on may be removed.
Reversible pebblings have been studied in [LV96Reversibility, Kralovic04TimeSpaceReversible, KSS18PebblingMeetsColoring] and have been used to prove timespace tradeoffs in reversible simulation of irreversible computation in [LTV98Reversible, LMT00Reversible, Williams00Reversible, BTV01Reversible]. In a different context, Potechin [Potechin10Monotone] implicitly used reversible pebbling to obtain lower bounds in monotone space complexity, with the connection made explicit in later works [CP14Monotone, FPRC13Average]. The paper [CLNV15Hardness] (to which this overview is indebted) studied the relative power of standard and reversible pebblings with respect to space, and also established PSPACE
hardness results for estimating the minimum space required to pebble graphs (reversibly or not).
1.3 Our Contributions
In this paper, we obtain an exactly tight correspondence between on the one hand reversible pebblings of DAGs and on the other hand Nullstellensatz refutations of pebbling formulas over these DAGs. We show that for any DAG it holds that can be reversibly pebbled in time and space if and only if there is a Nullstellensatz refutation of the pebbling formula over in size and degree . This correspondence holds regardless of the field in which the Nullstellensatz refutation is operating, and so, in particular, it follows that pebbling formulas have exactly the same complexity for Nullstellensatz regardless of the ambient field.
We then revisit the timespace tradeoff literature for the standard pebble game, focusing on the papers [CS80GraphPebbling, CS82ExtremeTimeSpaceTradeoffs, LT82AsymptoticallyTightBounds]. The results in these papers do not immediately transfer to the reversible pebble game, and we are not fully able to match the tightness of the results for standard pebbling, but we nevertheless obtain strong timespace tradeoff results for the reversible pebble game.
This allows us to derive Nullstellensatz sizedegree tradeoffs from reversible pebbling timespace tradeoffs as follows. Suppose that we have a DAG such that:

can be reversibly pebbled in time .

can be reversibly pebbled in space .

There is no reversible pebbling of that simultaneously achieves time and space .
Then for Nullstellensatz refutations of the pebbling formula over (which will be formally defined shortly) we can deduce that:

Nullstellensatz can refute in size .

Nullstellensatz can also refute in degree .

There is no Nullstellensatz refutation of that simultaneously achieves size and degree .
We prove four such tradeoff results, which can be found in Section 4. The following theorem is one example of such a result (specifically, it is a simplified version of Theorem 4.1).
Theorem 1.1.
There is a family of CNF formulas of size such that:

There is a Nullstellensatz refutation of in degree .

There is a Nullstellensatz refutation of of nearlinear size and degree

Any Nullstellensatz refutation of in degree at most must have exponential size.
It should be noted that this is not the first time proof complexity tradeoff results have been obtained from pebble games. Pebbling formulas were used in [BenSasson09SizeSpaceTradeoffs, BN11UnderstandingSpace] to obtain sizespace tradeoffs for resolution, and later in [BNT13SomeTradeoffs] also for polynomial calculus. However, the current reductions between pebbling and Nullstellensatz are much stronger in that they go in both directions and are exact even up to additive constants.
With regard to Nullstellensatz, it was shown in [BCIP02Homogenization] that Nullstellensatz degree is lowerbounded by standard pebbling price. This was strengthened in [dRMNPRV19Lifting], which used the connection between designs and Nullstellensatz degree discussed above to establish that the degree needed to refute a pebbling formula exactly coincides with the reversible pebbling price of the corresponding DAG (which is always at least the standard pebbling price, but can be much larger). Our reduction significantly improves on [dRMNPRV19Lifting] by constructing a more direct reduction, inspired by [GKRS18Adventures], that can simultaneously capture both time and space.
1.4 Outline of This Paper
After having discussed the necessary preliminaries in Section 2, we present the reductions between Nullstellensatz and reversible pebblings in Section 3. In Section 4, we prove timespace tradeoffs for reversible pebblings in order to obtain sizedegree tradeoffs for Nullstellensatz. Section LABEL:sec:conclusion contains some concluding remarks with suggestions for future directions of research.
2 Preliminaries
All logarithms in this paper are base unless otherwise specified. For a positive integer we write to denote the set of integers .
A literal over a Boolean variable is either the variable itself or its negation (a positive or negative literal, respectively). A clause is a disjunction of literals. A clause is a clause that contains at most literals. A formula in conjunctive normal form (CNF) is a conjunction of clauses . A CNF formula is a CNF formula consisting of clauses. We think of clauses and CNF formulas as sets, so that the order of elements is irrelevant and there are no repetitions. A truth value assignment to the variables of a CNF formula is satisfying if every clause in contains a literal that is true under .
2.1 Nullstellensatz
Let be any field and let be a set of variables. We identify a set of polynomials in the ring with the statement that all have a common valued root. A Nullstellensatz refutation of this claim is a syntactic equality
(2.1) 
where are also polynomials in . We sometimes refer to the polynomials as axioms and as Boolean axioms.
As discussed in the introduction, Nullstellensatz can be used as a proof system for CNF formulas by translating a clause to the polynomial and viewing Nullstellensatz refutations of as refutations of the CNF formula .
The degree of a Nullstellensatz refutation (1.1) is . We define the size of a refutation (2.1) to be the total number of monomials encountered when all products of polynomials are expanded out as linear combinations of monomials. To be more precise, let denote the number of monomials in a polynomial written as a linear combination of monomials. Then the size of a Nullstellensatz refutation on the form (1.1) is
(2.2) 
This is consistent with how size is defined for the “dynamic version” of Nullstellensatz known as polynomial calculus [CEI96Groebner, ABRW02SpaceComplexity], and also with the general size definitions for socalled algebraic and semialgebraic proof systems in [ALN16NarrowProofs, Berkholz18Relation, AO19ProofCplx].
We remark that this is not the only possible way of measuring size, however. It can be noted that the definition (2.2) is quite wasteful in that it forces us to represent the proof in a very inefficient way. Other papers in the semialgebraic proof complexity literature, such as [GHP02ExponentialLowerBound, KI06LowerBounds, DMR09TightRankLowerBounds], instead define size in terms of the polynomials in isolation, more along the lines of
(2.3) 
or as the bit size or “any reasonable size” of the representation of all polynomials , and .
In the end, the difference is not too important since the two measures (2.2) and (2.3) are at most a square apart, and for size we typically want to distinguish between polynomial and superpolynomial. In addition, and more importantly, in this paper we will only deal with CNF formulas with , and in this setting the two definitions are the same up to a constant factor . Therefore, we will stick with (2.2), which matches best how size is measured in the closely related proof systems resolution and polynomial calculus, and which gives the cleanest statements of our results.^{2}^{2}2We refer the reader to Section 2.4 in [AH18SizeDegree] for a more detailed discussion of the definition of proof size in algebraic and semialgebraic proof systems.
When proving lower bounds for algebraic proof systems it is often convenient to consider a multilinear setting where refutations are presented in the ring . Since the Boolean axioms are no longer needed, the refutation (2.1) can be written simply as
(2.4) 
where we assume that all results of multiplications are implicitly multilinearized. It is clear that any refutation on the form (2.1) remains valid after multilinearization, and so the size and degree measures can only decrease in a multilinear setting. In this paper, we prove our lower bound in our reduction in the multilinear setting and the upper bound in the nonmultilinear setting, making the tightly matching results even stronger.
2.2 Reversible Pebbling and Pebbling Formulas
Throughout this paper denotes a directed acyclic graph (DAG) of constant fanin with vertices and edges . For an edge we say that is a predecessor of and a successor of . We write to denote the sets of all predecessors of , and drop the subscript when the DAG is clear from context. Vertices with no predecessors/successors are called sources/sinks. Unless stated otherwise we will assume that all DAGs under consideration have a unique sink .
A pebble configuration on a DAG is a subset of vertices . A reversible pebbling strategy for a DAG with sink , or a reversible pebbling of for short, is a sequence of pebble configurations such that , , and such that each configuration can be obtained from the previous one by one of the following rules:

for such that (a pebble placement on ).

for such that (a pebble removal from ).
The time of a pebbling is and the space is .
We could also say that a reversible pebbling should be such that and , and define the time of such a pebbling to be . This is so since once we have reached a configuration containing we can simply run the pebbling backwards (because of reversibility) until we reach the empty configuration again, and without loss of generality all time and spaceoptimal reversible pebblings can be turned into such pebblings. For simplicity, we will often take this viewpoint in what follows.
For technical reasons it is sometimes important to distinguish between visiting pebblings, for which , and persistent pebblings, which meet the more stringent requirement that . (It can be noted that for the more relaxed standard pebble game discussed in the introductory section any pebbling can be assumed to be persistent without loss of generality.)


Pebble games can be encoded in CNF by socalled pebbling formulas [BW01ShortProofs], or pebbling contradictions. Given a DAG with a single sink , we associate a variable with every vertex and add clauses encoding that

the source vertices are all true;

if all immediate predecessors are true, then truth propagates to the successor;

but the sink is false.
In short, the pebbling formula over consists of the clauses for all (note that if is a source ), and the clause .
We encode this formula by a set of polynomials in the standard way. Given a set , we denote by the monomial (in particular, ). For every vertex , we have the polynomial
(2.5) 
and for the sink we also have the polynomial
(2.6) 
See Figure 1 for an illustration, including how the CNF formula is translated to a set of polynomials.
3 Reversible Pebblings and Nullstellensatz Refutations
In this section, we prove the correspondence between the reversible pebbling game on a graph and Nullstellensatz refutation of the pebbling contradiction of . Specifically, we prove the following result.
Theorem 3.1.
Let be a directed acyclic graph with a single sink, let be the corresponding pebbling contradiction, and let be a field. Then, there is a reversible pebbling strategy for with time at most and space at most if and only if there is a Nullstellensatz refutation for over of size at most and degree at most . Moreover, the same holds for multilinear Nullstellensatz refutations.
3.1 From Pebbling to Refutation
We start by proving the “only if” direction of Theorem 3.1. Let
(3.1) 
be an optimal reversible pebbling strategy for . Let be the first configuration in which there is a pebble on the sink . Without loss of generality, we may assume that : if the last steps were more efficient than the first steps, we could have obtained a more efficient strategy by replacing the first steps with the (reverse of) the last steps, and vice versa.
We use to construct a Nullstellensatz refutation over for the pebbling contradiction . To this end, we will first construct for each step of a Nullstellensatz derivation of the polynomial . The sum of all these polynomials is a telescoping sum, and is therefore equal to
(3.2) 
We will then transform this sum into a Nullstellensatz refutation by adding the polynomial
(3.3) 
We turn to constructing the aforementioned derivations. To this end, for every , let denote the vertex which was pebbled or unpebbled during the th step, i.e., during the transition from to . Then, we know that in both configurations and the predecessors of have pebbles on them, i.e., . Let us denote by the set of other vertices that have pebbles during the th step. Finally, let be a number that equals to if was pebbled during the th step, and equals to if was unpebbled. Now, observe that
(3.4) 
where the last step follows since the predecessors of are necessarily in . Therefore, our final refutation for is
(3.5)  
Note, in fact, it is a multilinear Nullstellensatz refutation, since it contains only multilinear monomials and does not use the Boolean axioms. It remains to analyze its degree and size.
For the degree, observe that every monomial in the proof is of the form , and the degree of each such monomial is exactly the number of pebbles used in the corresponding configuration. It follows that the maximal degree is exactly the space of the pebbling strategy .
Let us turn to considering the size. Observe that for each of the configurations , the refutation contains exactly two monomials: for all , one monomial for is generated in the th step, and another in the th step, and for the configuration the second monomial is generated when we add . In addition, the refutation contains exactly one monomial for the configuration , which is generated in the first step. Hence, the total number of monomials generated in the refutation is exactly , as required.
3.2 From Refutation to Pebbling
We turn to prove the “if” direction of Theorem 3.1. We note that it suffices to prove it for multilinear Nullstellensatz refutations, since every standard Nullstellensatz refutation implies the existence of a multilinear one with at most the same size and degree. Let
(3.6) 
be a multilinear Nullstellensatz refutation of over of degree . We use this refutation to construct a reversible pebbling strategy for .
To this end, we construct a “configuration graph” , whose vertices consist of all possible configurations of at most pebbles on (i.e., the vertices will be all subsets of of size at most ). The edges of will be determined by the polynomials of the refutation, and every edge in will constitute a legal move in the reversible pebbling game (i.e., it will be legal to move from to and vice versa). We will show that contains a path from the empty configuration to a configuration that contains the sink , and our pebbling strategy will be generated by walking on this path from to and back.
The edges of the configuration graph are defined as follows: Let be a vertex of , and let be a monomial of that does not contain . Let be the set of vertices such that (such a set exists since the refutation is multilinear). Then, we put an edge in that connects and (we allow parallel edges). It is easy to see that the edge connects configurations of size at most , and that it indeed constitutes a legal move in the reversible pebbling game. We note that is a bipartite graph: to see it, note that every edge
connects a configuration of an odd size to a configuration of an even size.
For the sake of the analysis, we assign the edge a weight in that is equal to coefficient of in . We define the weight of a configuration to be the sum of the weights of all the edges that touch (where the addition is done in the field ). We use the following technical claim, which we prove at the end of this section.
Claim 3.2.
Let be a configuration in that does not contain the sink . If is empty, then its weight is . Otherwise, its weight is .
We now show how to construct the required pebbling strategy for . To this end, we first prove that there is a path in from the empty configuration to a configuration that contains the sink . Suppose for the sake of contradiction that this is not the case, and let be the connected component of that contains the empty configuration. Our assumption says that none of the configurations in contains .
The connected component is bipartite since is bipartite. Without loss of generality, assume that the empty configuration is in the lefthand side of . Clearly, the sum of the weights of the configurations on the lefthand side should be equal to the corresponding sum on the righthand side, since they are both equal to the sum of the weights of the edges in . However, the sum of the weights of the configurations on the righthand side is (since all these weights are by Claim 3.2), while the sum of the weights of the lefthand side is (again, by Claim 3.2). We reached a contradiction, and therefore must contain some configuration that contains the sink .
Next, let be a path from the empty configuration to . Our reversible pebbling strategy for is
(3.7) 
This is a legal pebbling strategy since, as noted above, every edge of constitutes a legal move of the reversible pebbling game. The strategy uses space , since all the configurations in contain at most pebbles by definition. The time of is . It therefore remains to show that the size of the Nullstellensatz refutation from Equation 3.6 is at least .
To this end, note that every edge in the path corresponds to some monomial in some polynomial . When the monomial is multiplied by the axiom , it generates two monomials in the proof: the monomial and the monomial . Hence, the Nullstellensatz refutation contains at least monomials that correspond to edges from the path. In addition, the product must contains at least one monomial, since the refutation must use the sink axiom (because without this axiom is not a contradiction). It follows that the refutation contains at least monomials, as required. We conclude this section by proving Claim 3.2.
Proof of Claim 3.2..
We start by introducing some terminology. First, observe that a monomial may be generated multiple times in the refutation of Equation 3.6, and we refer to each time it is generated as an occurrence of . We say that an occurrence of is generated by a monomial of if it is generated by the product . Throughout the proof, we identify a configuration with the monomial .
We first prove the claim for the nonempty case. Let be a nonempty configuration. We would like to prove the weight of is . Recall that the weight of is the sum of the coefficients of the occurrences of that are generated by monomials that do not contain the corresponding vertex . Observe that Equation 3.6 implies that the sum of the coefficients of all the occurrences of is : the coefficient of on the righthand side is , and it must be equal to the coefficient of on the lefthand side, which is the sum of the coefficients of all the occurrences.
To complete the proof, we argue that every monomial that does contain the vertex contributes to that sum. Let be a monomial of that contains the vertex and generates an occurrence of . Let be the coefficient of . Then, it must hold that
(3.8)  
where the second equality holds since we contains and we are working with a multilinear refutation, and the third equality holds since we assumed that generates an occurrence of . It follows that generates two occurrences of , one with coefficient and one with coefficient , and therefore it contributes to the sum of the coefficients of all the occurrences of .
We have shown that the sum of the coefficients of all the occurrences of is , and that the occurrences generated by monomials that contain contribute to this sum, and therefore the sum of coefficients of occurrences that are generated by monomials that do not contain must be , as required. In the case that is the empty configuration, the proof is identical, except that the sum of the coefficients of all occurrences is , since the coefficient of is on the right hand side of Equation 3.6. ∎
4 Nullstellensatz Tradeoffs from Reversible Pebbling
In this section we prove Nullstellensatz refutation sizedegree tradeoffs for different degree regimes. Let us first recall what is known with regards to degree and size. In what follows, a Nullstellensatz refutation of a CNF formula refers to a Nullstellensatz refutation of the translation of to polynomials. As mentioned in the introduction, if a CNF formula over variables can be refuted in degree then it can be refuted in simultaneous degree and size . However, for Nullstellensatz it is not the case that strong enough degree lower bounds imply size lower bounds.
A natural question is whether for any given function there is a family of CNF formulas of size such that

has a Nullstellensatz refutation ;

has a Nullstellensatz refutation of (close to) linear size and degree ;

Any Nullstellensatz refutation of in degree only slightly below must have size nearly .
We present explicit constructions of formulas providing such tradeoffs in several different parameter regimes. We first show that there are formulas that require exponential size in Nullstellensatz if the degree is bounded by some polynomial function, but if we allow slightly larger degree there is a nearly linear size proof.
Theorem 4.1.
There is a family of explicitly constructible unsatisfiable CNF formulas of size such that:

There is a Nullstellensatz refutation of in degree .

For any constant , there is a Nullstellensatz refutation of of size and degree

There exists a constant such that any Nullstellensatz refutation of in degree at most must have size .
We also analyse a family of formulas that can be refuted in close to logarithmic degree and show that even if we allow up to a certain polynomial degree, the Nullstellensatz size required is superpolynomial.
Theorem 4.2.
Let be an arbitrarily small positive constant and let be any arbitrarily slowly growing monotone function . Then there is a family of explicitly constructible unsatisfiable CNF formulas of size such that:

There is a Nullstellensatz refutation of in degree .

For any constant , there is a Nullstellensatz refutation of of size and degree

Any Nullstellensatz refutation of in degree at most
must have size superpolynomial in .
Still in the smalldegree regime, we present a very robust tradeoff in the sense that superpolynomial size lower bound holds for degree from to .
Theorem 4.3.
There is a family of explicitly constructible unsatisfiable CNF formulas of size such that:

There is a Nullstellensatz refutation of in degree .

For any constant , there is a Nullstellensatz refutation of of size and degree

There exists a constant such that any Nullstellensatz refutation of in degree at most must have size .
Finally, we study a family of formulas that have Nullstellensatz refutation of quadratic size and that present a smooth sizedegree tradeoff.
Theorem 4.4.
There is a family of explicitly constructible unsatisfiable CNF formulas of size such that any Nullstellensatz refutation of that optimizes size given degree constraint (and less than ) has size .
We prove these results by obtaining the analogous timespace tradeoffs for reversible pebbling and then applying the tight correspondence between size and degree in Nullstellensatz and time and space in reversible pebbling.
4.1 Reversible Pebbling TimeSpace Tradeoffs
Our strategy for proving reversible pebbling tradeoffs will be to analyse standard pebbling tradeoffs. Clearly lower bounds from standard pebbling transfer to reversible pebbling; the next theorem shows how, in a limited sense, we can also transfer upper bounds. It is based on a reversible simulation of irreversible computation proposed by [Bennett89TimeSpaceReversible] and analysed precisely in [LS90NoteOnBennett].
Theorem 4.5 ([Bennett89TimeSpaceReversible, LS90NoteOnBennett]).
Let be an arbitrary DAG and suppose can be pebbled (in the standard way) using pebbles in time . Then for any , can be reversibly pebbled in time using pebbles.
We also use the following general proposition, which allows upper bounding the reversible pebbling price of a graph by using its depth and maximum indegree.
Proposition 4.6.
Any DAG with maximum indegree and depth has a persistent reversible pebbling strategy in space at most .
Proof.
We will use the fact that if a graph has a persistent reversible strategy in space then it has a visiting reversible strategy in space .
The proof is by induction on the depth. For we can clearly persistently reversibly pebble the graph with pebble. For , we persistently reversibly pebble all but one of the (that is, at most ) immediate predecessors of the sink one at a time. By the induction hypothesis, this can be done with at most pebbles. At this point there are at most predecessors of the sink which are pebbled and no other pebbles on the graph. Let be the only nonpebbled predecessor of the sink. We do a visiting reversible pebbling of until a pebble is placed on . We now pebble the sink and then reverse the visiting pebbling of until the subtree rooted at has no pebbles on it. By the induction hypothesis, this can be done with at most pebbles. All that is left to do is to to remove the pebbles which are on predecessors of the sink. Again by the induction hypothesis, this can be done with pebbles. ∎
4.2 CarlsonSavage Graphs
The first family of graphs for which we present reversible pebbling tradeoffs consists of the socalled CarlsonSavage graphs, which are illustrated in Figure 2 and are defined as follows.
Definition 4.7 (CarlsonSavage graph [CS80GraphPebbling, CS82ExtremeTimeSpaceTradeoffs, Nordstrom12RelativeStrength]).
The twoparameter graph family , for , is defined by induction over . The base case is a DAG consisting of two sources and sinks with directed edges , for and , i.e., edges from both sources to all sinks. The graph has sinks and is built from the following components:

disjoint copies of a pyramid graph of height .

one copy of .

disjoint and identical line graphs called spines, where each spine is composed of sections, and every section contains vertices.
The above components are connected as follows: In every section of every spine, each of the first vertices has an incoming edge from the sink of one of the first pyramids, and each of the last vertices has an incoming edge from one of the sinks of (where different vertices in the same section are connected to different sinks).
Note that has multiple sinks. We define a (reversible) pebbling of a multisink graph to be a (reversible) pebbling that places pebbles on each sink at some point (the pebbles do not need to be present in the last configuration). Let be the singlesink subgraph of consisting of all vertices that reach the first sink of . Since all sinks are symmetric, pebbling and pebbling are almost equivalent.
Proposition 4.8.
Any (reversible) pebbling of induces a (reversible) pebbling of in at most the same space and the same time. From any (reversible) pebbling of we can obtain (reversible) pebbling of by (reversibly) pebbling each sink of one at a time, that is, simulating times, once for each sink. Note that and .
Carlson and Savage proved the following properties of this graph.
Lemma 4.9 ([CS82ExtremeTimeSpaceTradeoffs]).
The graphs are of size , have indegree , and have standard pebbling price .
Theorem 4.10 ([CS82ExtremeTimeSpaceTradeoffs]).
Suppose that is a standard pebbling of in space less than for . Then
This lower bound holds for space up to . By allowing only a constant factor more pebbles it is possible to pebble the graph (in the standard way) in linear time.
Lemma 4.11 ([Nordstrom12RelativeStrength]).
The graphs have standard pebbling strategies in simultaneous space and time linear in the size of the graphs.
The standard pebbling price upper bound does not carry over to reversible pebbling because the line graph requires more pebbles in reversible pebbling than in standard pebbling. However, we can adapt the standard pebbling strategy to reversible pebbling using the following fact on the line graph.
Proposition 4.12 ([LV96Reversibility]).
The visiting reversible pebbling price of the line graph on vertices is and the persistent reversible pebbling price is .
Using this result, we get the following upper bound (which is slightly stronger then what we would get by applying Theorem 4.5).
Lemma 4.13.
The graphs have reversible pebbling price at most .
Proof.
The proof is by induction on . Clearly, can be reversibly pebbled with pebbles. In order to pebble any sink of , we can reversibly pebble the corresponding spine with the spaceefficient strategy for reversibly pebbling a line graph (as per Proposition 4.12) and every time we need to place or remove a pebble on a given vertex of the spine, we reversibly pebble the subgraph that reaches this vertex. By Proposition 4.6, pyramids of depth can be reversibly pebbled with pebbles. Therefore, by induction on we get that the reversible pebbling price of is at most . ∎
Lemma 4.14.
For any , the graphs have reversible pebbling strategies in simultaneous space and time (where denotes the number of vertices).
We can now choose different values for the parameters and and obtain graphs with tradeoffs in different space regimes. The first family of graphs we consider are those that exhibit exponential time lowerbounds.
Theorem 4.15.
There are explicitly constructible families of singlesink DAGs of size and maximum indegree such that:

The graph has reversible pebbling price .

For any constant , there is a reversible pebbling of in time and space

There is a constant such that any standard pebbling of in space at most
must take time at least .
Proof.
Let be the singlesink subgraph of consisting of all vertices that reach the first sink, for and .
Given Theorem 3.1 which proves the tight correspondence between reversible pebbling and Nullstellensatz refutations, Theorem 4.1 follow from Theorem 4.15.
It is also interesting to consider families of graphs that can be reversibly pebbled in very small space, close to the logarithmic lower bound on the number of pebbles required to reversibly pebble a singlesink DAG. In this smallspace regime, we cannot expect exponential time lower bounds, but we can still obtain superpolynomial ones.
Theorem 4.16.
Let be an arbitrarily small positive constant and let be any arbitrarily slowly growing monotone function . Then there is a family of explicitly constructible singlesink DAGs of size and maximum indegree such that:

The graph has reversible pebbling price .

For any constant , there is a reversible pebbling of in time and space

Any standard pebbling of in space at most
requires time superpolynomial in .
Proof.
The proof is analogous to that of Theorem 4.16 with parameters and . ∎
Remark 4.17.
We note that in the second items of both the foregoing theorems, we could have reduced the time of the reversible pebbling to by applying Theorem 4.5 with . This would have come at a cost of an extra logarithmic factor in the corresponding space bounds.
4.3 Stacks of Superconcentrators
Lengauer and Tarjan [LT82AsymptoticallyTightBounds] studied robust superpolynomial tradeoffs for standard pebbling and showed that there are graphs that have standard pebbling price , but that any standard pebbling in space up to , for some constant , requires superpolynomial time. For reversible pebbling we get almost the same result for the same family of graphs.
Theorem 4.18.
There are explicitly constructible families of singlesink DAGs of size and maximum indegree such that:

The graph has reversible pebbling price .

For any constant , there is a reversible pebbling of in time and space

There exists a constant such that any standard pebbling of using at most pebbles requires time .
Note that, together with Theorem 3.1, this implies Theorem 4.3. Now in order to prove this theorem we must first introduce the family of graphs we will consider.
Definition 4.19 (Superconcentrator [Valiant75NonLinear]).
A directed acyclic graph is an superconcentrator if it has sources , sinks , and for any subsets and of sources and sinks of size it holds that there are vertexdisjoint paths between and in .
Pippenger [Pippenger77Superconcentrators] proved that there are superconcentrators of linear size and logarithmic depth, and Gabber and Galil [GG81Explicit] gave the first explicit construction. For concreteness, we will consider the explicit construction by Alon and Capalbo [AC03SmallerExplicitSuperconcentrators] which has better parameters.
Theorem 4.20 ([AC03SmallerExplicitSuperconcentrators]).
For all integers , there are explicitly constructible superconcentrators for with edges, depth , and maximum indegree .
It is easy to see that we can modify these superconcentrators so that the maximum indegree is by substituting each vertex with indegree by a binary tree with leafs. Note that this only increase the size and the depth by constant factors.
Corollary 4.21.
There are superconcentrators with vertices, maximum indegree and depth .
Given an superconcentrator , we define a stack of superconcentrators to be disjoint copies of where each sink of the th copy is connected to a different source of the st copy for . Since we want singlesink DAGs, we add a binary tree with leafs and depth , and connect each sink of the th copy of to a different leaf of the tree. Lengauer and Tarjan [LT82AsymptoticallyTightBounds] proved the following theorem for stacks of superconcentrators.
Theorem 4.22 ([LT82AsymptoticallyTightBounds]).
Let denote a stack of (explicitly constructible) linearsize superconcentrator with bounded indegree and depth . Then the following holds:

The standard pebbling price of is .

There is a lineartime standard pebbling strategy for with .

If is a standard pebbling strategy for in space , then
Comments
There are no comments yet.