SMT求解技术简述

• 作者: 张健 金继伟 马菲菲
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 可满足性模理论(SMT) DPLL(T) 求解器
• 年，卷（期）: 2015,（7）
• 所属期刊栏目: 综述?探索
• 页码范围: 769-780
• 页数: 12页
• 分类号: TP30
• 字数: 9826字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1405041

摘要

SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域，尤其是形式验证、程序分析、软件测试等领域，都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术，着重介绍并分析了这些技术，包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点，包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望，量词的处理、优化问题和解空间大小的计算等尤其值得关注。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张健	中国科学院软件研究所	272	3714	30.0	51.0
2	金继伟	中国科学院软件研究所	1	21	1.0	1.0
3	马菲菲	中国科学院软件研究所	1	21	1.0	1.0