SMT求解技术的发展及最新应用研究综述

摘要

可满足性模理论(satisfiability modulo theories, SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.%The satisfiability modulo theories (SMT) problem is a decision problem for the satisfiability of first-order logical formula with respect to combinations of background theories.SMT supports many background theories, so it can describe a lot of practical problems in industrial fields or academic circles.Also, the expression ability and the efficiency of decision algorithms of SMT are both better than those of SAT (satisfiability).With its efficient satisfiability decision algorithms, SMT has been widely used in many fields, in particular in test-case generation, program defect detection, register transfer level (RTL) verification, program analysis and verification, solving linear optimization over arithmetic constraint formula, etc.In this paper, we firstly summarize fundamental problems and decision procedures of SAT.After that, we give a brief overview of SMT, including its fundamental concepts and decision algorithms.Then we detail different types of decision algorithms, including eager and lazy algorithms which have been studied in the past five years.Moreover, some state-of-the-art SMT solvers, including Z3, Yices2 and CVC4 are analyzed and compared based on the results of the SMT's competition.Additionally, we also focus on the introduction for the application of SMT solving in some typical communities.At last, we give a preliminary prospect on the research focus and the research trends of SMT.