关键词: 一阶逻辑, 可满足性模理论, Lazy方法, DPLL(T), SMT求解器, #SMT

Abstract: 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 solvers find applications in various domains and have become essential engines for formal verification. Currently, SMT is widely used in fields such as artificial intelligence, hardware RTL verification, automated reasoning, and software engineering. Based on recent developments in SMT, this paper first expounds 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 further insights into the implementation processes of mainstream solvers Z3, CVC5, and MathSAT5. Subsequently, the paper introduces extension problems of the SMT as  #SMT, the SMTlayer approach applied to deep neural networks (DNNs), and quantum SMT solvers. Finally, the paper offers a per spective on the development of SMT and discusses the challenges they face.

Key words: first-order logic, satisfiability modulo theories (SMT), Lazy method, DPLL(T), SMT solver, #SMT