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 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 ≥ (N 0.58 log 2 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 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-ε requires length T Ω(log log N/ log log log N) .

Authors

• Paul Beame
• Christopher Beck
• Russell Impagliazzo

Keywords

• proof complexity
• time-space tradeoffs