Sciweavers

STOC
2012
ACM

Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space

12 years 2 months ago
Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space
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 Nlog2 N (and like all formulas have Resolution refutations of space N) for which any Resolution refutation using space S and length T requires T ≥ (N0.58 log2 N /S)Ω(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 2o(N1/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 S1− requires length TΩ(log log N/ log log log N) . Categories and Subject Descriptors F.0 [Theory of...
Paul Beame, Christopher Beck, Russell Impagliazzo
Added 28 Sep 2012
Updated 28 Sep 2012
Type Journal
Year 2012
Where STOC
Authors Paul Beame, Christopher Beck, Russell Impagliazzo
Comments (0)