Nullstellensatz Size-Degree Trade-offs from the Reversible Pebbling Game

We discuss recent work in which we establish a tight relationship between Nullstellensatz certificates of the so-called "pebbling" formulas — which play an important role in a variety of results in proof complexity, circuit complexity, and logic — and the "reversible pebbling game", a well-studied combinatorial pebbling game on directed graphs. To be precise: we show that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz certificate of the pebbling formula over G in length t+1 and degree s. This result is independent of the underlying field of the Nullstellensatz certificate, and implies sharp bounds for other proof systems in the literature; furthermore, we can apply known reversible pebbling time-space tradeoffs to obtain strong length-degree trade-offs for Nullstellensatz certificates. To our knowledge these are the first strong tradeoffs known for this propositional proof system.
This is joint work with Susanna de Rezende, Or Meir and Jakob Nordstrom.