Abstract:
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$.