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 k4 a refutation of a random k-CNF of n clauses and n variables requires monomial space (n−1+k−3−) with high probability. For constant we prove that monomial space complexity is (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 k4 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.