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

文章基本信息

  • 标题:The Riis Complexity Gap for QBF Resolution
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Judith Clymo ; Stefan Dantchev
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2018
  • 卷号:2018
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    We give an analogue of the Riis Complexity Gap Theorem for Quanti fied Boolean Formulas (QBFs). Every fi rst-order sentence  without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like Q-Resolution are either of polynomial size (if  has no models) or at least exponential in size (if  has some in finite model). However, di fferently from the translations to propositional logic, the translation to QBF must be given additional structure in order for the polynomial upper bound to hold in tree-like Q-Resolution. This extra structure is not needed in the system tree-like Exp+Res, where we see the complexity gap on a natural translation to QBF.

  • 关键词:Complexity Gaps ; Proof Complexity ; quantified Boolean formulas
国家哲学社会科学文献中心版权所有