Name
Title | ||
|---|---|---|
Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space. |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1137/130914085 | SIAM JOURNAL ON COMPUTING |
Keywords | Field | DocType |
proof complexity,resolution,time-space trade-offs,lower bounds | Binary logarithm,Discrete mathematics,Combinatorics,Exponential function,Polynomial,Space trade,Mathematical proof,Omega,Proof complexity,Mathematics | Journal |
Volume | Issue | ISSN |
45 | SP4 | 0097-5397 |
Citations | PageRank | References |
1 | 0.37 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul Beame | 1 | 2234 | 176.07 |
| Christopher Beck | 2 | 27 | 1.53 |
| Russell Impagliazzo | 3 | 5444 | 482.13 |