| 可满足性求解技术研究 |
| |
| 引用本文： | 张建民,沈胜宇,李思昆.可满足性求解技术研究[J].计算机工程与科学,2010,32(1):50-54. |
| |
| 作者姓名： | 张建民 沈胜宇 李思昆 |
| |
| 作者单位： | 国防科学技术大学计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目(60603088,90707003) |
| |
| 摘 要： | 求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。
|
| 关 键 词： | 布尔可满足问题 可满足性模理论问题 完全方法 不完全方法 |
| 收稿时间： | 2008-09-28 |
| 修稿时间： | 2008-12-03 |
Advances in Satisfiability Solving Techniques |
| |
| ZHANG Jian-min,SHEN Sheng-yu,LI Si-kun.Advances in Satisfiability Solving Techniques[J].Computer Engineering & Science,2010,32(1):50-54. |
| |
| Authors: | ZHANG Jian-min SHEN Sheng-yu LI Si-kun |
| |
| Affiliation: | School of Computer Science/a>;National University of Defense Technology/a>;Changsha 410073/a>;China |
| |
| Abstract: | Solving the satisfiability of formulae is theoretically important in the practical applications of various fields,such as formal verification,electronic design automation and artificial intelligence. This paper introduces the principles of the Boolean Satisfiability and Satisfiability Modulo Theories. The existing algorithms are introduced and compared according to their types. The qualities of these algorithms are also analyzed. Finally,we discuss the current challenges,and outline the future research tren... |
| |
| Keywords: | Boolean satisfiability(SAT) satisfiability modulo theories(SMT) complete method incomplete method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
