💻 computer science

Pebble Games and Algebraic Proof Systems

This paper establishes a precise parallelism between pebbling games (reversible, black, and black-white) and algebraic proof systems (Nullstellensatz, Monomial Calculus, and Polynomial Calculus) by proving that pebbling strategies on a graph $G$ directly correspond to refutations of pebbling formulas with matching space and time/size complexities, thereby enabling new degree separations and strong tradeoff results.

Original authors: Lisa-Marie Jaser, Jacobo Toran

Published 2026-05-06

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Lisa-Marie Jaser, Jacobo Toran

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a giant, complex puzzle on a board. The board is a map of one-way streets (a "Directed Acyclic Graph"), and your goal is to get a special marker to the very end of the road (the "sink").

This paper is about two different ways of looking at this puzzle:

The Game: A physical game where you move markers (pebbles) around the board to reach the end.
The Proof: A mathematical system where you write down equations to prove the puzzle is actually impossible to solve (a "refutation").

The authors, Lisa-Marie Jaser and Jacobo Torán, discovered that these two seemingly different worlds are actually mirror images of each other. They found a perfect translation guide between the rules of the game and the rules of the math.

The Three Versions of the Game

Think of the game as having three levels of difficulty, like video game modes:

Reversible Mode (The Strict Hiker): You can only place a marker on a spot if all the paths leading to it are already marked. Crucially, you can only remove a marker if the paths leading to it are still marked. It's like a hiker who can only turn back if they haven't left any footprints behind. This is the hardest, most restrictive version.
Black Mode (The Confident Builder): You still need all paths to be marked before placing a marker. But here, you can remove a marker anytime you want, even if the paths leading to it are empty. It's like building a house; you can take a brick away whenever you like, even if the wall is unstable.
Black-White Mode (The Gambler): You can place a "White" marker anywhere you want, anytime. But you can't remove it until the paths leading to it are marked. It's like making a guess (non-determinism) and only being allowed to take it back once you've proven your guess was right.

The Three Versions of the Math

On the other side, there are three ways to write the mathematical proof that the puzzle is impossible:

Nullstellensatz (NS): The "Static" system. You have to write the whole proof in one giant, static list of equations. You can't build it step-by-step; it has to be there all at once.
Monomial Calculus (MC): The "Middle Ground." You can build the proof step-by-step, but you are restricted in how you can multiply your numbers. It's like a construction crew that can only add one brick at a time in a specific way.
Polynomial Calculus (PC): The "Powerhouse." You can build the proof step-by-step with very few restrictions. You can multiply anything by anything.

The Big Discovery: The Perfect Mirror

The authors proved that the difficulty of the Game matches the difficulty of the Math in a very specific way:

Reversible Game $\leftrightarrow$ $\leftrightarrow$ Nullstellensatz (NS)
- The number of markers you need in the game matches the "degree" (complexity) of the math proof.
Black Game $\leftrightarrow$ $\leftrightarrow$ Monomial Calculus (MC)
- This is the paper's main new discovery. They showed that the number of markers needed in the "Black" game matches the complexity of the "Monomial Calculus" proof.
- Time vs. Size: If you can solve the game quickly (few steps) with few markers, you can write a short, simple math proof. If the game takes a long time, your math proof will be huge.
Black-White Game $\leftrightarrow$ $\leftrightarrow$ Polynomial Calculus (PC)
- While the "degree" (complexity) of the PC proof is always low (constant), the space (how many variables you need to hold in your head at once) matches the number of markers in the Black-White game.

Why Does This Matter? (The "So What?")

Before this paper, we knew the "Reversible" game matched the "Nullstellensatz" math. But we didn't know if the "Black" game matched the "Monomial Calculus" math. Now we do.

This connection allows the authors to use known results from game theory to prove new things about math proofs:

Separating the Systems: They proved that "Monomial Calculus" is strictly harder than "Polynomial Calculus" for certain puzzles. There are puzzles where the "Black" game requires a lot of markers, meaning the "Monomial Calculus" proof must be very complex, even though the "Polynomial Calculus" proof can be simple.
The Trade-off: They showed a "degree-size trade-off." Imagine you want to write a math proof. If you try to make the proof very simple (low degree), it might become astronomically long (huge size). If you allow the proof to be slightly more complex, you can make it much shorter. It's like trying to pack a suitcase: if you insist on folding everything perfectly (low complexity), it takes forever. If you just stuff it in (higher complexity), it's fast, but the suitcase is messy.

The "Variable Space" Surprise

Finally, the authors noticed something cool about "Space."

In the game, "Space" is the maximum number of markers on the board at any one time.
In the math, "Variable Space" is the maximum number of different letters (variables) you have to look at simultaneously.

They proved that for all three versions of the game and all three versions of the math, these two numbers are exactly the same. If you need 5 markers to win the game, you need to track 5 variables to write the proof.

Summary

This paper built a bridge between a physical game of moving markers and abstract algebraic proofs. By showing that the rules of the game perfectly predict the complexity of the math, the authors unlocked new ways to prove that some mathematical proofs are inherently difficult, while others can be surprisingly efficient. It's like realizing that the number of steps a hiker takes to climb a mountain tells you exactly how many pages of notes a mathematician needs to write to prove the mountain exists.

Technical Summary: Pebble Games and Algebraic Proof Systems

Problem Statement

The paper investigates the structural connections between pebble games on directed acyclic graphs (DAGs) and algebraic proof systems. Specifically, it seeks to establish precise correspondences between the resource measures (time and space) of pebbling strategies and the complexity measures (degree and size) of refutations for pebbling formulas ($Peb(G)$) within three specific algebraic proof systems: Nullstellensatz (NS), Monomial Calculus (MC), and Polynomial Calculus (PC).

While previous work (e.g., [dRMNR21], [BCIP02]) had established connections between reversible pebbling and NS, and between black pebbling and PC/NS degrees, the relationship between black pebbling and the intermediate system Monomial Calculus remained less explored. Furthermore, the paper addresses the gap regarding variable space complexity across all three proof systems and their corresponding pebbling game variants (reversible, black, and black-white).

Methodology

The authors employ a bidirectional translation methodology between combinatorial game strategies and algebraic derivations:

From Pebbling to Proofs (Black $\to$ MC):
- The authors construct a Monomial Calculus (MC) refutation from a black pebbling strategy.
- They utilize the dual notion of white pebbling (where pebbles are placed on any vertex but removed only if predecessors are pebbled) to map the removal of black pebbles to the derivation of polynomials.
- The construction involves deriving monomials corresponding to pebble configurations. Placing a pebble corresponds to multiplying by a variable, while removing a pebble involves a linear combination with a pebbling axiom multiplied by a monomial.
- The size of the resulting proof is analyzed by counting the intermediate monomials generated during these operations.
From Proofs to Pebbling (MC $\to$ Black):
- The authors restrict attention to input MC refutations (analogous to input Resolution), where every derivation step involves an axiom.
- They prove that for Horn formulas (which pebbling formulas are), any MC refutation can be transformed into an input MC refutation without increasing degree or size (Lemma 3.4).
- From an input refutation, they extract a black pebbling strategy by tracking the variables present in the monomials of the proof's "backbone." The removal of a variable in the proof corresponds to removing a pebble, justified by the presence of predecessor variables (axioms).
Variable Space Analysis:
- The paper analyzes variable space (the maximum number of distinct variables appearing simultaneously in a refutation configuration).
- It leverages known results regarding the simulation of Resolution to extend variable space equivalences to stronger systems like PC.

Key Contributions and Results

1. Equivalence between Black Pebbling and Monomial Calculus

The paper establishes a tight correspondence between black pebbling and MC refutations for pebbling formulas $Peb(G)$ on a DAG $G$ with a single sink:

Theorem 3.1: If there exists a black pebbling strategy with space $s$ and time $t$ , there exists an MC refutation with degree $s$ and size $ts$. The variable space of this refutation equals $s$ .
Theorem 3.6: Conversely, if there exists an MC refutation with degree $s$ and size $t$ , there exists a black pebbling strategy with space $s$ and time $t+s$ .
Significance: This mirrors the known equivalence between reversible pebbling and Nullstellensatz established in [dRMNR21], placing MC as the algebraic counterpart to black pebbling.

2. Degree Separations

Using the established equivalences and known bounds on pebbling prices, the authors derive new separations between algebraic proof systems:

MC vs. PC: There exist families of unsatisfiable formulas with constant PC degree but requiring MC degree $\Omega(n / \log n)$ (Theorem 3.8). This improves upon previous constant-factor separations.
NS vs. MC: There exist families where MC refutations have constant degree (e.g., 2) while NS refutations require degree $\Omega(\log n)$ (Theorem 3.9). This is derived from the logarithmic gap between black and reversible pebbling prices on path graphs.
General Tradeoffs: For any function $s(n)$ , there are formulas with MC degree $O(s(n))$ requiring NS degree $\Omega(s(n) \log n)$ (Theorem 3.10).

3. Degree-Size Tradeoffs for MC

The paper demonstrates that MC exhibits strong degree-size tradeoffs, distinct from the behavior of PC:

Theorem 3.12: There are formulas with MC refutations of degree $d_n$ and size $2^{\Omega(n \log n)}$ , but refutations of degree $d_n + 1$ have size $O(n^3)$ .
Theorem 3.14 & 3.16: Robust tradeoffs are shown where reducing the degree below a certain threshold forces the size to become superpolynomial, even for arbitrarily slow-growing degree functions.
Implication: Unlike PC, where strong degree lower bounds imply exponential size lower bounds (via [IPS99]), MC allows for polynomial-size refutations even with high degree lower bounds.

4. Variable Space Equivalences

The authors show that the variable space complexity of refuting $Peb(G)$ exactly matches the pebbling price for all three game/system pairs:

NS: Variable space equals Reversible pebbling price ($Rev(G)$).
MC: Variable space equals Black pebbling price ($Black(G)$).
PC: Variable space equals Black-White pebbling price ($BW(G)$).
Result: This allows the transfer of known pebbling space separations to variable space separations in proof complexity. For instance, Theorem 4.4 and 4.5 show families where $VSpace_{PC}$ is linear while $VSpace_{MC}$ is superlinear or quadratic.

Significance and Claims

The paper claims to provide a "parallelism" between the hierarchy of pebbling games (Reversible $\subset$ Black $\subset$ Black-White) and the hierarchy of algebraic proof systems (NS $\subset$ MC $\subset$ PC).

Unification: It unifies the understanding of algebraic proof complexity by identifying Monomial Calculus as the natural system corresponding to black pebbling, filling a gap between the static Nullstellensatz and the dynamic Polynomial Calculus.
Separations: It provides the first strong degree separations between MC and PC, and refines the separation between NS and MC.
Tradeoffs: It establishes that MC admits strong degree-size tradeoffs, showing that high degree does not necessarily imply exponential size in this system, contrasting with PC.
Variable Space: It resolves the correspondence for variable space across all three systems, demonstrating that while degree measures fail to capture the complexity of PC relative to black-white pebbling (due to constant degree refutations), variable space measures succeed.

The authors conclude that these results underline the importance of MC as a natural proof system and open questions regarding the optimality of these separations and the exact degree gap between NS and MC.