• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International conference on principles and practice of constraint programming >Evaluating QBF Solvers: Quantifier Alternations Matter
【24h】

Evaluating QBF Solvers: Quantifier Alternations Matter

机译：评估QBF解算器：量词替代品很重要

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a QBF in prenex conjunctive normal form (PCNF) is directly related to the theoretical hardness of the respective QBF satisfiability problem in the polynomial hierarchy. We show empirically that the performance of solvers based on different solving paradigms substantially varies depending on the numbers of alternations in PCNFs. In related theoretical work, quantifier alternations have become the focus of understanding the strengths and weaknesses of various QBF proof systems implemented in solvers. Our results motivate the development of methods to evaluate orthogonal solving paradigms by taking quantifier alternations into account. This is necessary to showcase the broad range of existing QBF solving paradigms for practical QBF applications. Moreover, we highlight the potential of combining different approaches and QBF proof systems in solvers.
机译：我们目前对量化器交替对量化布尔公式（QBF）求解器的评估产生影响的实验研究。结合前正态形式（PCNF）的QBF中量词替换的数量与多项式层次结构中各个QBF可满足性问题的理论硬度直接相关。我们凭经验表明，基于不同求解范式的求解器的性能会根据PCNF中交替的数量而显着变化。在相关的理论工作中，量词的替换已成为理解求解器中实现的各种QBF证明系统的优缺点的重点。我们的研究结果激励了通过考虑量词替换来评估正交求解范例的方法的发展。这对于展示适用于实际QBF应用的各种现有QBF解决范例很有必要。此外，我们强调了在求解器中结合不同方法和QBF证明系统的潜力。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号