基于悖论证明与局部搜索的不可满足子式求解算法

An Unsatisfiable Subformulae Extraction Algorithm Based on Refutation Proof and Local Search

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.

Functional verification and debugging has consumed more and more percent of the total design cycle,owing to the growing scale and complexity of software and hardware designs.Therefore an efficient method is necessary to accelerate debugging and locating bugs in the designs.An unsatisfiable subformula can help automatic tools to improve the efficiency of the errors localization.In recent years the algorithms of deriving unsatisfiable subformulae are mostly based on the DPLL backtrack-search algorithm.However little attention has been concentrated on the incomplete methods.The authors proposed the definitions of refutation proof and refutation parsing tree,and a heuristic local search algorithm to extract unsatisfiable subformulae from the refutation proof of a formula.The approach firstly builds the resolution parsing tree with a local search procedure,combined with reasoning heuristics,dynamic pruning and subsumption elimination method,and then recursively derives unsatisfiable subformulae from the refutation parsing tree.The experimental results show that our algorithm outperforms the similar algorithms on the practical and random benchmarks,and also indicate that the pruning and subsumption elimination technique can effectively reduce the memory consumption and runtime.