Pebble Games and Algebraic Proof Systems

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.