SMT求解技术简述

摘要

SMT is the problem of deciding the satisfiability of a first order formula with respect to some theory formulas. It is being recognized as increasingly important due to its applications in different communities, in particular in formal verification, program analysis and software testing. This paper provides a brief overview of SMT and its theories. Then this paper introduces some approaches aiming to improve the efficiency of SMT solving, including eager and lazy approaches and optimum technique which have been proposed in the last ten years. This paper also introduces some state-of-the-art SMT solvers, including Z3, Yices and CVC3/CVC4. Finally, this paper gives a preliminary prospect on the research trends of SMT, which include SMT with quantifier, optimization problems subject to SMT and volume computation for SMT.%SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域，尤其是形式验证、程序分析、软件测试等领域，都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术，着重介绍并分析了这些技术，包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点，包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望，量词的处理、优化问题和解空间大小的计算等尤其值得关注。