ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2017, Vol. 54 ›› Issue (7): 1405-1425.doi: 10.7544/issn1000-1239.2017.20160303

• 综述 •    下一篇



  1. 1(基础软件国家工程研究中心(中国科学院软件研究所) 北京 100190);2(中国科学院大学 北京 100049);3(计算机科学国家重点实验室(中国科学院软件研究所) 北京 100190);4(中央财经大学信息学院 北京 100081) (
  • 出版日期: 2017-07-01
  • 基金资助: 

Survey on Development of Solving Methods and State-of-the-Art Applications of Satisfiability Modulo Theories

Wang Chong1,2,3, Lü Yinrun1,2,3, Chen Li1,2,3, Wang Xiuli4, Wang Yongji1,3   

  1. 1(National Engineering Research Center for Fundamental Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190);2(University of Chinese Academy of Sciences, Beijing 100049);3(State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190);4(School of Information, Central University of Finance and Economics, Beijing 100081)
  • Online: 2017-07-01

摘要: 可满足性模理论(satisfiability modulo theories, SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.

关键词: 可满足性模理论, SMT求解器, SMT求解算法, 测试用例自动生成, 程序缺陷检测, 云计算

Abstract: 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.

Key words: satisfiability modulo theories (SMT), SMT solver, decision algorithms of SMT, test-case generation, program defect detection, cloud computing