• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Conference on Tools with Artificial Intelligence >An Algorithm to Compute Minimal Unsatisfiable Subsets for a Decidable Fragment of First-Order Formulas
【24h】

An Algorithm to Compute Minimal Unsatisfiable Subsets for a Decidable Fragment of First-Order Formulas

机译：计算一阶公式可确定片段的最小不满足子集的算法

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

摘要

In the past few years, SAT-based methods in propositional logic have been widely used to tackle practical problems in electronic design automation, software testing and hardware verification. However, lots of industrial problems can naturally be transformed to certain decidable fragments of first-order logic (FOL), which are more expressive than propositional logic. In this paper, we propose a novel algorithm to compute all minimal unsatisfiable subsets for a constrained variant of first-order formulas. By this means, we not only evaluate the satisfiability of specified formulas, but also extract minimal unsatisfiable cores. A heuristic strategy is proposed to improve the performance. Experimental results demonstrate that our algorithm performs well on many industrial instances, and the heuristic strategy is more robust than other strategies in time and space efficiency.
机译：在过去的几年中，命题逻辑中基于SAT的方法已被广泛用于解决电子设计自动化，软件测试和硬件验证中的实际问题。但是，许多工业问题自然可以转化为某些确定性的一阶逻辑（FOL）片段，比命题逻辑更具表现力。在本文中，我们提出了一种新颖的算法来计算一阶公式的约束变体的所有最小不满足子集。通过这种方式，我们不仅可以评估指定公式的可满足性，还可以提取最少的不满足需求的核。提出了一种启发式策略来提高性能。实验结果表明，我们的算法在许多工业实例上表现良好，启发式策略在时间和空间效率上比其他策略更健壮。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号