可满足性模理论综述  

A survey of satisfiability modulo theories

作　　者：唐傲 王晓峰[1,2] 何飞 TANG Ao;WANG Xiao-feng;HE Fei(School of Computer Science and Engineering,North Minzu University,Yinchuan 750021;Key Laboratory of Images&Graphics Intelligent Processing of State Ethnic Affairs Commission,North Minzu University,Yinchuan 750021,China)

机构地区：[1]北方民族大学计算机科学与工程学院,宁夏银川750021 [2]北方民族大学图像图形智能处理国家民委重点实验室,宁夏银川750021

出　　处：《计算机工程与科学》2024年第3期400-415,共16页Computer Engineering & Science

基　　金：国家自然科学基金(62062001);宁夏青年拔尖人才项目(2021)。

摘　　要：可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。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.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]