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

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