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

文章基本信息

  • 标题:On Q-Resolution and CDCL QBF Solving
  • 本地全文:下载
  • 作者:Mikolas Janota
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2016
  • 卷号:2016
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    Q-resolution and its variations provide the underlying proof systems for the DPLL-based QBF solvers. While (long-distance) Q-resolution models a conflict driven clause learning (CDCL) QBF solver, it is not known whether the inverse is also true. This paper provides a negative answer to this question. This contrasts with SAT solving, where CDCL solvers have been shown to simulate resolution.

  • 关键词:conflict driven clause learning ; Q-Resolution ; QBF
国家哲学社会科学文献中心版权所有