TR24-042 Authors: Lisa Jaser, Jacobo Toran

Publication: 3rd March 2024 09:43

Downloads: 155

Keywords:

Analyzing refutations of the well known

pebbling formulas 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 NS, MC and PC on the other side. In particular we prove:

\begin{itemize}

\item 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 $2t(s-1)$.

These results are analogous to those proven in [de Rezende et al. 21] for the case of reversible pebbling and

Nullstellensatz.

Using them we prove degree separations between NS and MC

as well as strong degree-size tradeoffs for MC.

\item We show that the variable space needed for the refutation of pebbling formulas in Polynomial Calculus exactly

coincides with the black-white pebbling number of the corresponding graph.

One direction of this result was known. We present an new elementary proof of it.

\item

We show that for any unsatisfiable CNF formula $F,$ the variable space in a Resolution refutation

of the formula is a lower bound for the monomial space in a PCR refutation for

the extended formula $F[\oplus]$.

This implies that

for any DAG

$G$, the monomial space needed in the PCR refutation of an XOR pebbling formulas is lower bounded

by the black-white pebbling number of the corresponding graph. This solves affirmatively Open Problem 7.11 from

[Buss NordstrÃ¶m 21].

\item

The last result

also

proves a strong separation between degree and monomial space in PCR of size $\Omega(\frac{n}{\log n})$

with the additional property

that it is independent of the field characteristic. This question

was posed in [Filmus et al. 13].

\end{itemize}

We found out a mistake in the proof of Theorem 30, therefore we do not claim anymore that we have proven that for any unsatisfiable CNF formula F the variable space in a Resolution refutation

of the formula is a lower bound for the monomial space in a PCR refutation for

the extended formula $F[\oplus]$. This result is still open.

Also, we were pointed out that the result in Theorem 28 follows directly from known results

from [Ben09] and [BNT13] .