可满足性模理论综述

来源：计算机工程与科学杂志2024年第3期北京时间：

作者：唐傲, 王晓峰, 何飞

单位：1.北方民族大学计算机科学与工程学院，宁夏 银川 750021；2.北方民族大学图像图形智能处理国家民委重点实验室，宁夏 银川 750021

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

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

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