• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Constraints >A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
【24h】

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

机译：分支定界算法，用于提取最小的最小不满足子公式

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Explaining the causes of infeasibility of Boolean formulas has practical applications in numerous fields, such as artificial intelligence (repairing inconsistent knowledge bases), formal verification (abstraction refinement and unbounded model checking), and electronic design (diagnosing and correcting infeasibility). Minimal unsatisfiable subformulas (MUSes) provide useful insights into the causes of infeasibility. An unsatisfiable formula often has many MUSes. Based on the application domain, however, MUSes with specific properties might be of interest. In this paper, we tackle the problem of finding a smallest-cardinality MUS (SMUS) of a given formula. An SMUS provides a succinct explanation of infeasibility and is valuable for applications that are heavily affected by the size of the explanation. We present (1) a baseline algorithm for finding an SMUS, founded on earlier work for finding all MUSes, and (2) a new branch-and-bound algorithm called Digger that computes a strong lower bound on the size of an SMUS and splits the problem into more tractable subformulas in a recursive search tree. Using two benchmarkrnsuites, we experimentally compare Digger to the baseline algorithm and to an existing incomplete genetic algorithm approach. Digger is shown to be faster in nearly all cases. It is also able to solve far more instances within a given runtime limit than either of the other approaches.
机译：解释布尔公式不可行的原因已在许多领域中得到了实际应用，例如人工智能（修复不一致的知识库），形式验证（抽象性提炼和无限制模型检查）以及电子设计（诊断和纠正不可行）。最小的不满意子公式（MUSes）可为不可行的原因提供有用的见解。不满意的公式通常具有许多MUS。但是，基于应用程序域，可能需要关注具有特定属性的MUS。在本文中，我们解决了找到给定公式的最小基数MUS（SMUS）的问题。 SMUS对不可行提供了简洁的解释，对于受解释大小严重影响的应用程序非常有价值。我们提出（1）用于查找SMUS的基线算法，该算法基于早期用于查找所有MUS的工作，并且（2）一种称为Digger的新的分支定界算法，该算法计算SMUS大小的下限并进行拆分将问题分解为递归搜索树中更易处理的子公式。使用两个基准套件，我们将Digger与基准算法和现有的不完全遗传算法方法进行了实验比较。 Digger在几乎所有情况下都显示出更快的速度。与其他方法相比，它还能够在给定的运行时限制内解决更多实例。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号