布尔不可满足子式的求解方法研究进展

摘要：

解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.

关键词：形式化验证、布尔公式、可满足问题、不可满足子式、DPLL算法

所属期刊栏目：20

分类号：TP391.7(计算技术、计算机技术)

资助基金：国家自然科学基金60603088,90707003

在线出版日期：2008-11-27（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：1253-1260