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

文章基本信息

  • 标题:Are Short Proofs Narrow? QBF Resolution is not Simple
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Leroy Chew ; Meena Mahajan
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2015
  • 卷号:2015
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    The groundbreaking paper `Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that lower bounds for space again can be obtained via lower bounds for width.

    In this paper we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Exp+Res and IR-calc, however only in the weak tree-like models.

    Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.

  • 关键词:lower bounds ; Proof Complexity ; QBF ; Resolution ; simulations
国家哲学社会科学文献中心版权所有