论文部分内容阅读
解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值，而不可满足子式能够为公式不可满足的原因提供精确的解释，帮助应用领域的自动化工具迅速定位错误，诊断问题失败的本质缘由。近年来涌现了许多基于sAT求解器DPLL回溯搜索过程的完全算法，但关于不完全方法提取不可满足子式的研究相对较少。因此，本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列，并融合了布尔推理技术以提高搜索效率；而后通过一个