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

文章基本信息

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

    For quantified Boolean formulas (QBF) there are two main different approaches to solving: QCDCL and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than CDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of expansion solving techniques over QCDCL solving. Our first result shows that tree-like expansion systems allow short proofs of QBFs that are a source of hardness for QCDCL, i.e. tree-like Exp+Res is strictly stronger than tree-like Q-Resolution. In our second result we efficiently transform dag-like Q-Resolution proofs of QBFs with bounded quantifier complexity into Exp+Res proofs. This is theoretical confirmation of experimental findings by Lonsing and Egly, who observed that expansion QBF solvers often outperform QCDCL solvers on instances with few quantifier alternations.

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