求解布尔不可满足子式的消解悖论算法

A resolution-based Boolean unsatisfiable subformulas computing algorithm

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

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.