ECCC-Report TR11-149https://eccc.weizmann.ac.il/report/2011/149Comments and Revisions published for TR11-149en-usFri, 04 Nov 2011 16:36:45 +0200
Paper TR11-149
| Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for Superlinear Space |
Chris Beck,
Russell Impagliazzo,
Paul Beame
https://eccc.weizmann.ac.il/report/2011/149We 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)}$.Fri, 04 Nov 2011 16:36:45 +0200https://eccc.weizmann.ac.il/report/2011/149