Search Results

Analyzing refutations of the well known pebbling 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 [Susanna F. de Rezende et al., 2021] 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.