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

• Type: Journal
• Year: 2012
• Where: STOC
• Authors: Paul Beame, Christopher Beck, Russell Impagliazzo
• Keywords: Algorithms, Oswald Veblen, Proof Complexity, Resolution Proofs, STOC 2012