| 布尔不可满足子式的求解方法研究进展 |
| |
| 引用本文： | 李思昆,张建民,沈胜宇. 布尔不可满足子式的求解方法研究进展[J]. 计算机辅助设计与图形学学报, 2008, 20(10) |
| |
| 作者姓名： | 李思昆 张建民 沈胜宇 |
| |
| 作者单位： | 国防科学技术大学计算机学院,长沙,410073 |
| |
| 摘 要： | 解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.
|
| 关 键 词： | 形式化验证 布尔公式 可满足问题 不可满足子式 DPLL算法 |
Research Advances in Methods of Extracting Boolean Unsatisfiable Subformulae |
| |
| Li Sikun,Zhang Jianmin,Shen Shengyu. Research Advances in Methods of Extracting Boolean Unsatisfiable Subformulae[J]. Journal of Computer-Aided Design & Computer Graphics, 2008, 20(10) |
| |
| Authors: | Li Sikun Zhang Jianmin Shen Shengyu |
| |
| Affiliation: | Li Sikun Zhang Jianmin Shen Shengyu (School of Computer Science,National University of Defense Technology,Changsha 410073) |
| |
| Abstract: | 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,... |
| |
| Keywords: | formal verification Boolean formula satisfaction problem unsatisfiable subformula DPLL algorithm |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
