Space proof complexity for random $3$-CNFs via a $(2-\epsilon)$-Hall's Theorem

TL;DR

This paper establishes new lower bounds on the space complexity for refuting random 3-CNF formulas in Resolution and algebraic proof systems, using a novel variant of Hall's theorem involving bipartite graph matchings.

Contribution

It introduces a new combinatorial technique based on a $(2- ext{epsilon})$-Hall's theorem to prove space lower bounds in proof complexity for random 3-CNFs.

Findings

Resolution refutations require $oldsymbol{ ilde{ ext{Omega}}}(n/ ext{log} n)$ clauses in memory.

Polynomial Calculus with Resolution needs $oldsymbol{ ilde{ ext{Omega}}}(n/ ext{log} n)$ monomials in memory.

Total space lower bound in Resolution is $oldsymbol{ ilde{ ext{Omega}}}(n^2/ ext{log}^2 n)$.

Abstract

We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $\phi$ in $n$ variables requires, with high probability, $\Omega(n/\log n)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $\phi$ requires, with high probability, $\Omega(n/\log n)$ clauses each of width $\Omega(n/\log n)$ to be kept at the same time in memory. This gives a $\Omega(n^2/\log^2 n)$ lower bound for the total space needed in Resolution to refute $\phi$. The main technical innovation is a variant of Hall's theorem. We show that in bipartite graphs $G$ with bipartition $(L,R)$ and left-degree at most 3, $L$ can be covered by certain families of disjoint paths, called $(2,4)$-matchings, provided that $L$ expands in $R$ by a factor of $(2-\epsilon)$, for $\epsilon < \frac{1}{23}$.