首页    期刊浏览 2024年11月09日 星期六
登录注册

文章基本信息

  • 标题:From Small Space to Small Width in Resolution
  • 本地全文:下载
  • 作者:Yuval Filmus ; Massimo Lauria ; Mladen Mikša
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2014
  • 卷号:2014
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation---previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.

  • 关键词:degree ; PCR ; Polynomial Calculus ; Proof Complexity ; Resolution ; Space ; width
国家哲学社会科学文献中心版权所有