ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2017, Vol. 54 ›› Issue (7): 1405-1425.doi: 10.7544/issn1000-1239.2017.20160303

    Next Articles

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

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

CLC Number: