Space proof complexity for random 3-CNFs

TL;DR

This paper establishes tight lower bounds on the space complexity of refuting random 3-CNF formulas in Resolution and Polynomial Calculus systems, demonstrating that significant memory is required for such proofs.

Contribution

It introduces new space lower bounds for random 3-CNF refutations in Resolution and Polynomial Calculus, including a novel variant of Hall's Lemma for bipartite graphs.

Findings

Resolution refutations require (n) clauses of width (n) in memory.

Polynomial Calculus with Resolution refutations require (n) monomials in memory.

Total space lower bound for Resolution is (n^2).

Abstract

We investigate the space complexity of refuting $3$-CNFs in Resolution and 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)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $\phi$ requires, with high probability, $\Omega(n)$ clauses each of width $\Omega(n)$ to be kept at the same time in memory. This gives a $\Omega(n^2)$ lower bound for the total space needed in Resolution to refute $\phi$. These results are best possible (up to a constant factor). The main technical innovation is a variant of Hall's Lemma. 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 VW-matchings, provided that $L$ expands in $R$ by a factor of $(2-\epsilon)$, for $\epsilon < 1/23$.