Satisfiability modulo theories(SMT)refers to the decidability problem of first-order logic formulas under specific background theories.SMT based on first-order logic have a stronger expressive capability compared to SAT,with higher abstraction ability to handle more complex issues.SMT solv-ers find applications in various domains and have become essential engines for formal verification.Cur-rently,SMT is widely used in fields such as artificial intelligence,hardware RTL verification,automa-ted reasoning,and software engineering.Based on recent developments in SMT,this paper first ex-pounds on the fundamental knowledge of SMT and lists common background theories.It then analyzes and summarizes the implementation processes of Eager,Lazy,and DPLL(T)methods,providing fur-ther insights into the implementation processes of mainstream solvers Z3,CVC5,and MathSAT5.Sub-sequently,the paper introduces extension problems of the SMT as#SMT,the SMTlayer approach ap-plied to deep neural networks(DNNs),and quantum SMT solvers.Finally,the paper offers a per spec-tive on the development of SMT and discusses the challenges they face.
维普
万方数据