__
TR11-149 | 4th November 2011 12:06
__

#### Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for Superlinear Space

**Abstract:**
We give the first time-space tradeoff lower bounds for Resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size $N$ that have Resolution refutations of space and size each roughly $N^{\log_2 N}$ (and like all formulas have Resolution refutations of space $N$) for which any Resolution refutation using space $S$ and length $T$ requires $T\ge (N^{0.58\log_2 N}/S)^{\Omega(\log\log N/\log\log\log N)}$. By downward translation, a similar tradeoff applies to all smaller space bounds.

We also show somewhat stronger time-space tradeoff lower bounds for Regular Resolution, which are also the first to apply to superlinear space. Namely, for any space bound $S$ at most $2^{o(N^{1/4})}$ there are formulas of size $N$, having clauses of width 4, that have Regular Resolution proofs of space $S$ and slightly larger size $T=O(NS)$, but for which any Regular Resolution proof of space $S^{1-\epsilon}$ requires length T^{\Omega(\log\log N/\log\log\log N)}$.