We study the space complexity of refuting unsatisfiable random $k$-CNFs in
the Resolution proof system. We prove that for any large enough $\Delta$,
with high probability a random $k$-CNF over $n$ variables and $\Delta n$
clauses requires resolution clause space of
$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,
for any $0<\epsilon<1/2$. For constant $\Delta$, this gives us linear,
optimal, lower bounds on the clause space.

A nice consequence of this lower bound is the first lower bound for size
of treelike resolution refutations of random $3$-CNFs with clause density
$\Delta > > \sqrt{n}$. This bound is nearly tight. Specifically, we show
that with high probability, a random $3$-CNF with $\Delta n$ clauses
requires treelike refutation size of
$\exp(\Omega(n/\Delta^{\frac{1+\epsilon}{1-\epsilon}}))$,
for any $0 < \epsilon < 1/2$.

Our space lower bound is the consequence of three main contributions.

1. We introduce a 2-player Matching Game on bipartite graphs $G$ to
prove that there are no perfect matchings in $G$.

2. We reduce lower bounds for the clause space of a formula $F$ in
Resolution to lower bounds for the complexity of the game played on the
bipartite graph $G(F)$ associated with $F$.

3. We prove that the complexity of the game is large whenever $G$ is an
expander graph.

Finally, a simple probabilistic analysis shows that for a random formula
$F$, with high probability $G(F)$ is an expander.

We also extend our result to the case of $G-PHP$, a generalization of the
pigeonhole Principle based on bipartite graphs $G$. We prove that the
clause space for $G-PHP$ can be reduced to the game complexity on $G$.