QBF求解算法研究综述

作     者：李舟军 陈石坤 Li Zhoujun;Chen Shikun

作者机构：国防科学技术大学计算机学院长沙410073 北京航空航天大学计算机学院北京100191 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2011年第48卷第5期

页      面：811-822页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金项目(90718017 60703075) 高等学校博士学科点专项科研基金项目(20070006055) 

主　　题：SAT QBF 求解算法 模型检验 形式化验证 

摘      要：近10年来,布尔可满足性(SAT)求解技术飞速发展,并已经成功应用于模型检验、定理证明等领域,特别是在限界模型检验(BMC)中取得了明显的进展,然而,由于命题逻辑公式的长度随系统规模指数倍增长,基于SAT的模型检验仍然存在状态空间爆炸问题.带量词的布尔公式(QBF)作为SAT公式的自然扩展,具有紧凑的空间结构、更强大、更直观的表达能力,能够简洁地描述模型检验中的公式.基于QBF的模型检验有希望缓解状态空间爆炸问题,成为当前研究的一个热点.总结了当前主流的QBF求解算法及常用的优化技术,指出了该领域中值得关注的新趋势.