TIME-SPACE TRADE-OFFS IN RESOLUTION: SUPERPOLYNOMIAL LOWER BOUNDS FOR SUPERLINEAR SPACE

摘要

We give the first time-space trade-off 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 size (and space) T(N) = N-Theta(log N) (and like all formulas have another resolution refutation of space N) but for which no resolution refutation can simultaneously have space S(N) = T(N)(o(1)) and size T(N)(O(1)). In other words, any substantial reduction in space results in a super polynomial increase in total size. We also show somewhat stronger time-space trade-off lower bounds for regular resolution, which are also the first to apply to superlinear space. For any function T that is at most weakly exponential, T(N) = 2(o(N1/4)), we give a tautology that has regular resolution proofs of size and space T(N), but no such proofs with space S(N) = T(N)(1-Omega(1)) and size T(N)(O(1)). Thus, any polynomial reduction in space has a superpolynomial cost in size. These tautologies are width 4 disjunctive normal form (DNF) formulas.