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

Research Advances in Methods of Extracting Boolean Unsatisfiable Subformulae

作　　者：李思昆[1] 张建民[1] 沈胜宇[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机辅助设计与图形学学报》2008年第10期1253-1260,共8页Journal of Computer-Aided Design & Computer Graphics

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

摘　　要：解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.Explaining the causes of infeasibility of Boolean formulae has theoretical importance and practical applications in various fields, such as formal verification and electronic design automation. An unsatisfiable subformula can provide a succinct explanation of infeasibility, and help application automatic tools to rapidly locate the errors, and to determine the underlying reasons for the failure. In recent years, there are many different contributions to research on extraction of Boolean unsatisfiable subformulae, due to the increasing importance in numerous practical applications. The existing algorithms are introduced and compared according to their types. Then we present our recent research works to derive unsatisfiable subformulae. Finally, we discuss the current challenges of methods to extract Boolean unsatisfiable subformulae, and outline the future research directions.

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

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]