TR01-031 Authors: Eli Ben-Sasson, Nicola Galesi

Publication: 26th April 2001 16:21

Downloads: 2229

Keywords:

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