Title | ||
---|---|---|
Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space |
Abstract | ||
---|---|---|
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). |
Year | DOI | Venue |
---|---|---|
2011 | 10.1145/2213977.2213999 | STOC '12 Proceedings of the forty-fourth annual ACM symposium on Theory of computing |
Keywords | DocType | Citations |
log log n,resolution refutation,smaller space bound,regular resolution proof,time-space tradeoffs,log2 n,nlog2 n,superlinear space,size n,log log log n,lower bound,space n,proof complexity | Journal | 20 |
PageRank | References | Authors |
0.67 | 22 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Paul Beame | 1 | 2234 | 176.07 |
Christopher Beck | 2 | 27 | 1.53 |
Russell Impagliazzo | 3 | 5444 | 482.13 |