• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Parallel SAT Solving in Bounded Model Checking
【24h】

Parallel SAT Solving in Bounded Model Checking

机译：边界模型检查中的并行SAT解决

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

摘要

Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.
机译：边界模型检查（BMC）是一种增量反驳技术，用于搜索长度增加的反例。固定长度的反例的存在由一阶逻辑公式表示，该逻辑公式使用适当的求解器检查其可满足性。我们应用通信并行求解器来检查BMC公式的可满足性。与其他并行求解技术相比，我们的方法不会并行化单个公式的可满足性检查，但是并行求解器可处理具有不同反例长度的公式。我们将最初为顺序BMC开发的Shtrichman的约束共享和复制方法调整为并行设置。由于现在已经并行化了学习机制，因此在并行设置中是否从Shtrichman的概念中受益并不明显。我们在许多基准测试中证明，并行求解器之间的充分通信可以产生预期的结果。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号