求解布尔不可满足子式的消解悖论算法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金资助项目(61103083,61133007);国家863计划资助项目(2012AA01A301);国家973计划资助项目(2011CB309705)


A resolution-based Boolean unsatisfiable subformulas  computing algorithm
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    求解布尔不可满足子式在超大规模集成电路设计与验证领域都具有非常重要的理论与应用价值,帮助EDA工具迅速定位错误与不一致。针对求解不可满足子式的非完全方法,提出了消解悖论与悖论解析树的概念,在此基础上提出一种启发式局部搜索算法。该算法根据公式的消解规则,采用局部搜索过程直接构造证明不可满足性的悖论解析树,而后递归搜索得到不可满足子式;算法中融合了布尔推理技术、动态剪枝方法及蕴含消除方法以提高搜索效率。基于随机测试集进行了实验对比,结果表明提出的算法优于同类算法。

    Abstract:

    Computing unsatisfiable subformulas of Boolean formulas has practical applications in VLSI design and verification. The unsatisfiable subformulas can help electronic design automation tools to rapidly locate the errors and inconsistency. The definitions of resolution refutation and refutation parsing tree, and a heuristic local search algorithm to extract unsatisfiable subformulas from the resolution refutation of a formula are presented. The approach directly constructs the refutation parsing tree for proving unsatisfiability with a local search procedure, and then recursively derives unsatisfiable subformulas. The algorithm combines with reasoning heuristics, dynamic pruning and subsumption elimination method to improve the efficiency. The experimental results show that our algorithm outperforms the similar algorithms on the random benchmarks.

    参考文献
    相似文献
    引证文献
引用本文

张建民,黎铁军,徐炜遐,等.求解布尔不可满足子式的消解悖论算法[J].国防科技大学学报,2015,37(1):21-27.
ZHANG Jianmin, LI Tiejun, XU Weixia, et al. A resolution-based Boolean unsatisfiable subformulas  computing algorithm[J]. Journal of National University of Defense Technology,2015,37(1):21-27.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2014-06-10
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2015-03-19
  • 出版日期:
文章二维码