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

文章基本信息

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

    In their influential paper `Short proofs are narrow -- resolution made simple', Ben-Sasson and Wigderson introduced a crucial tool for proving lower bounds on the lengths of proofs in the resolution calculus. Over a decade later their technique for showing lower bounds on the size of proofs, by examining the width of all possible proofs, remains one of the most effective lower bound techniques in propositional proof complexity.

    We continue the investigation into the application of this technique to proof systems for quantified Boolean formulas. We demonstrate a relationship between the size of proofs in level-ordered Q-Resolution and the width of proofs in Q-Resolution. In general, however, the picture is not positive, and for most stronger systems based on Q-Resolution, the size-width relation fails.

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