首页    期刊浏览 2024年12月02日 星期一
登录注册

文章基本信息

  • 标题:Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for Superlinear Space
  • 本地全文:下载
  • 作者:Paul Beame ; Chris Beck ; Russell Impagliazzo
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2011
  • 卷号:2011
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    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 Nlog2N (and like all formulas have Resolution refutations of space N) for which any Resolution refutation using space S and length T requires T(N058log2NS)(loglogNlogloglogN) . 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(N14) 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^{\Omega(\log\log N/\log\log\log N)}$.

  • 关键词:Proof Complexity; Resolution; Time Space Tradeoffs
国家哲学社会科学文献中心版权所有