SMT求解技术简述

摘要：

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

关键词：可满足性模理论(SMT)、DPLL(T)、求解器

分类号：TP30(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.61100064

在线出版日期：2015-07-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：769-780