• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Conference on Tools with Artificial Intelligence >Enhanced Unsatisfiable Cores for QBF: Weakening Universal to Existential Quantifiers
【24h】

Enhanced Unsatisfiable Cores for QBF: Weakening Universal to Existential Quantifiers

机译：增强QBF的不匹配核心：削弱普遍性的存在量词

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

摘要

We propose an enhanced notion of unsatisfiable cores for QBF in prenex CNF that weakens universal to existential quantifiers in addition to the traditional removal of clauses. We can thus obtain unsatisfiable cores that are semantically different from those obtained by the traditional notion; this gives rise to explanations — and, via hitting set duality, diagnoses — of unsatisfiability that are not provided by traditional unsatisfiable cores. We use a source-to-source transformation on QBF that reduces the weakening of universal to existential quantifiers to the removal of clauses. This enables any tool or method that can compute unsatisfiable cores of the traditional notion to also compute unsatisfiable cores of our enhanced notion. We implement our approach in the QBF solver DepQBF, and we experimentally evaluate it on a subset of QBFLIB. Several case studies illustrate that interesting information can be learned from our enhanced notion of unsatisfiable cores.
机译：除了传统的条款外，我们提出了在Prenex CNF中增强了对QBF的QBF QBF QBF的不匹配核的概念。因此，我们可以获得与传统概念获得的语义不同的不匹配核心;这引起了解释 - 并且通过击中设定的二元性，诊断 - 不可履行的不可起作用，这些核心不具核心。我们在QBF上使用源源转换，从而降低了普遍性地削弱了存在量化器以去除条款。这使任何可以计算传统概念的不可采取的核心的任何工具或方法，也可以计算我们增强概念的不可挑离的核心。我们在QBF Solver DepQBF中实现了我们的方法，我们通过实验评估了QBFlib的子集。几个案例研究表明，可以从我们增强的不可挑离核心的增强概念来了解有趣的信息。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号