| QBF求解算法研究综述 |
| |
| 引用本文： | 李舟军,陈石坤.QBF求解算法研究综述[J].计算机研究与发展,2011,48(5). |
| |
| 作者姓名： | 李舟军 陈石坤 |
| |
| 作者单位： | 1. 国防科学技术大学计算机学院,长沙,410073;北京航空航天大学计算机学院,北京,100191
2. 国防科学技术大学计算机学院,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金项目，高等学校博士学科点专项科研基金项目 |
| |
| 摘 要： | 近10年来,布尔可满足性(SAT)求解技术飞速发展,并已经成功应用于模型检验、定理证明等领域,特别是在限界模型检验(BMC)中取得了明显的进展,然而,由于命题逻辑公式的长度随系统规模指数倍增长,基于SAT的模型检验仍然存在状态空间爆炸问题.带量词的布尔公式(QBF)作为SAT公式的自然扩展,具有紧凑的空间结构、更强大、更直观的表达能力,能够简洁地描述模型检验中的公式.基于QBF的模型检验有希望缓解状态空间爆炸问题,成为当前研究的一个热点.总结了当前主流的QBF求解算法及常用的优化技术,指出了该领域中值得关注的新趋势.
|
| 关 键 词： | SAT QBF 求解算法 模型检验 形式化验证 |
Survey on QBF Evaluation Algorithms |
| |
| Li Zhoujun,Chen Shikun.Survey on QBF Evaluation Algorithms[J].Journal of Computer Research and Development,2011,48(5). |
| |
| Authors: | Li Zhoujun Chen Shikun |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
