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

作     者：李思昆 张建民 沈胜宇 Li Sikun;Zhang Jianmin;Shen Shengyu

作者机构：国防科学技术大学计算机学院长沙410073 

基　　金：国家自然科学基金(60603088 90707003) 

出 版 物：《计算机辅助设计与图形学学报》 (Journal of Computer-Aided Design & Computer Graphics)

年 卷 期：2008年第20卷第10期

页      码：1253-1260页

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

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

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203104038...