Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR24-042 | 22nd February 2024 17:25

Pebble Games and Algebraic Proof Systems Meet Again

RSS-Feed




TR24-042
Authors: Lisa Jaser, Jacobo Toran
Publication: 3rd March 2024 09:43
Downloads: 285
Keywords: 


Abstract:

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}


Comment(s):

Comment #1 to TR24-042 | 24th March 2024 06:46

Mistake found in the proof of Theorem 30

Authors: Jacobo Toran
Accepted on: 24th March 2024 06:46
Keywords: 


Comment:

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] .




ISSN 1433-8092 | Imprint