QBF求解算法研究综述

• 作者: 李舟军 陈石坤
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: SAT QBF 求解算法 模型检验 形式化验证
• 年，卷（期）: 2011,（5）
• 所属期刊栏目: 算法理论
• 页码范围: 811-822
• 分类号: TP301.6
• 字数: 12454字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	国防科学技术大学计算机学院	136	2221	23.0	43.0
5	陈石坤	国防科学技术大学计算机学院	3	11	1.0	3.0