ECCC-Report TR01-031https://eccc.weizmann.ac.il/report/2001/031Comments and Revisions published for TR01-031en-usThu, 26 Apr 2001 16:21:57 +0300
Paper TR01-031
| Space Complexity of Random Formulae in Resolution |
Eli Ben-Sasson,
Nicola Galesi
https://eccc.weizmann.ac.il/report/2001/031We 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$.
Thu, 26 Apr 2001 16:21:57 +0300https://eccc.weizmann.ac.il/report/2001/031