We study the space required by Polynomial Calculus refutations of random $k$-CNFs. We are interested in how many monomials one needs to keep in memory to carry on a refutation. More precisely we show that for $k \geq 4$ a refutation of a random $k$-CNF of $\Delta n$ clauses and $n$ variables requires monomial space $\Omega(n \Delta^{-\frac{1+\epsilon}{k-3-\epsilon}} )$ with high probability. For constant $\Delta$ we prove that monomial space complexity is $\Theta(n)$ with high probability. This solves a problem left open in Alekhnovich et al. (STOC, 2000) and in Ben-Sasson, Galesi (FOCS, 2001; Random Struct. Algorithms, 2003).
We study the \emph{twofold matching game}: it is a prover-delayer game on a bipartite graph in which the prover wants to show that the left side has no pair of disjoint matching sets on the right side. The prover has a bounded amount of memory. We show that any delayer's winning strategy against such prover is also a strategy to satisfy all equations in a bounded memory polynomial calculus refutation.
We show that a random $k$-CNF with $k \geq 4$ has large enough expansion with high probability. This allows lower bounds on the memory of a winning prover in the corresponding twofold matching game. A lower bound on the monomial space required to refute the formula follows.
We claim without proof that our result also applies to pigeonhole principles on bipartite graphs.
There is a non trivial error in the main proof. I will post an updated version as soon as the proof is fixed.
