Pebble Games and Algebraic Proof Systems
Pith reviewed 2026-05-19 08:00 UTC · model grok-4.3
The pith
Pebble games on DAGs correspond to algebraic proof systems with exact space matching.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
For any DAG G with a single sink, a monomial calculus refutation of Peb(G) with simultaneous degree s and size t implies a black pebbling strategy on G with space s and time t plus s. From a black pebbling strategy with space s and time t one can extract a monomial calculus refutation of degree s and size t times s. The same pattern of correspondences applies to the other two pairs of games and systems. In each case the space required by a pebbling strategy on G equals the variable space of a refutation of Peb(G) in the corresponding algebraic system.
What carries the argument
The explicit strategy-to-refutation and refutation-to-strategy translations that map pebbling moves to algebraic proof steps while preserving the numerical values of space or degree and time or size.
If this is right
- Known pebbling bounds on graphs yield degree separations between Nullstellensatz, Monomial Calculus and Polynomial Calculus.
- Strong degree-size tradeoffs hold for monomial calculus refutations.
- Variable space complexity in each algebraic system can be bounded using results on the matching pebbling game.
- Separations between the variable space measures of the three systems follow directly from known pebbling separations.
Where Pith is reading between the lines
- The exact numerical match indicates that variable space is the appropriate complexity measure for comparing these proof systems via pebbling.
- The translations could be applied to derive new lower bounds in algebraic proof complexity by studying graphs that require large pebbling space.
- Similar exact correspondences may exist between other combinatorial games and additional algebraic or proof systems.
Load-bearing premise
The pebbling formulas are built from the graph in the standard way and the translations between strategies and refutations preserve the exact numerical measures without hidden losses.
What would settle it
A specific directed acyclic graph where the minimal space of a black pebbling strategy differs from the minimal variable space of any monomial calculus refutation of its pebbling formula would disprove the claimed exact match.
read the original abstract
Analyzing refutations of the well known 0pebbling formulas Peb$(G)$ we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG $G$ with a single sink, if there is a Monomial Calculus refutation for Peb$(G)$ having simultaneously degree $s$ and size $t$ then there is a black pebbling strategy on $G$ with space $s$ and time $t+s$. Also if there is a black pebbling strategy for $G$ with space $s$ and time $t$ it is possible to extract from it a MC refutation for Peb$(G)$ having simultaneously degree $s$ and size $ts$. These results are analogous to those proven in {deRezende et al.21} for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC. We also notice that for any directed acyclic graph $G$ the space needed in a pebbling strategy on $G$, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb$(G)$ in each of the algebraic proof systems NS, MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper establishes connections between pebble games on DAGs and algebraic proof systems. For any DAG G with a single sink, it proves that a Monomial Calculus refutation of Peb(G) with degree s and size t implies a black pebbling strategy with space s and time t+s, and conversely a black pebbling strategy with space s and time t yields an MC refutation of degree s and size ts. These bidirectional translations are presented as analogous to prior results for reversible pebbling and Nullstellensatz. The paper further claims that pebbling space exactly matches variable space complexity in the corresponding systems (NS, MC, PC), and uses known pebbling bounds to derive degree separations between the systems as well as degree-size tradeoffs for MC.
Significance. If the claimed exact measure-preserving translations hold, the work provides a tight dictionary between combinatorial pebbling measures and algebraic proof complexity measures. This would enable direct transfer of pebbling lower bounds to proof complexity, yielding concrete degree separations and tradeoffs. The exact space-to-variable-space matching is a particularly clean contribution that strengthens the analogy across all three pairs of games and systems.
major comments (1)
- [Abstract (black-pebbling to MC direction)] Abstract (black-pebbling to MC direction): the claim that a black pebbling strategy of space s and time t yields an MC refutation of degree s and size exactly ts is load-bearing for all subsequent separations and tradeoffs. The construction simulates each pebbling move by generating monomials; if the number of monomials produced per step scales with the in-degree of the vertex or the number of literals in the corresponding clause of Peb(G), the total size may exceed ts by a multiplicative factor linear in maximum in-degree. The manuscript must exhibit the explicit monomial-generation rule and prove that no such hidden factor arises.
minor comments (1)
- [Abstract] The phrase '0pebbling formulas' in the abstract is presumably a typographical error for 'pebbling formulas'.
Simulated Author's Rebuttal
We thank the referee for the positive assessment of the significance of our results and for the careful reading that identified this point about the black-pebbling to MC translation. We address the comment directly below.
read point-by-point responses
-
Referee: Abstract (black-pebbling to MC direction): the claim that a black pebbling strategy of space s and time t yields an MC refutation of degree s and size exactly ts is load-bearing for all subsequent separations and tradeoffs. The construction simulates each pebbling move by generating monomials; if the number of monomials produced per step scales with the in-degree of the vertex or the number of literals in the corresponding clause of Peb(G), the total size may exceed ts by a multiplicative factor linear in maximum in-degree. The manuscript must exhibit the explicit monomial-generation rule and prove that no such hidden factor arises.
Authors: We appreciate the referee highlighting the need for explicitness on this load-bearing claim. The construction (detailed in Section 3 of the manuscript) translates each of the t pebbling steps by generating monomials via multiplication of existing space-s monomials by a single new variable; the clause for a vertex v is simulated without enumerating all predecessors explicitly because the presence of the predecessor monomials in the current space allows a single multiplication step per new pebble. Consequently the number of monomials added per step is bounded by a small constant independent of in-degree, yielding total size exactly ts. Nevertheless, to satisfy the request we will revise the manuscript by adding a self-contained lemma that states the precise monomial-generation rule for each pebbling move and proves the size bound by induction on t, with no hidden factor linear in maximum in-degree. This revision will be incorporated in the next version. revision: yes
Circularity Check
Explicit bidirectional constructions from game and proof definitions; no circularity
full rationale
The paper proves the claimed correspondences by constructing explicit translations: each pebbling move is simulated by a sequence of monomial-calculus inferences (and conversely), with the numerical measures (space s, time t, degree s, size ts or t+s) preserved directly by the simulation rules. These constructions are derived from the standard definitions of Peb(G), the black-pebbling game, and the monomial calculus, without parameter fitting, self-definition, or load-bearing reliance on the authors' prior work. The analogy to deRezende et al. 2021 is cited only for context; the new proofs for MC/black-pebbling stand independently. Separations then invoke externally established pebbling bounds from the literature rather than quantities internal to this paper.
Axiom & Free-Parameter Ledger
axioms (2)
- domain assumption G is a directed acyclic graph with a single sink.
- domain assumption Peb(G) is the standard pebbling formula associated with G.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.