Page 38 - 《软件学报》2026年第2期

冯维直 等: 带递归定义的 SMT 公式求解技术综述 517

去得到无量词公式, 然后将其抽象为命题逻辑公式, 判断其可满足性, 如果不可满足则原公式不可满足, 如果可满
足则通过理论求解器检查背景理论是否可满足. 由于现代 SAT 求解算法的发展, 许多优化技术可以极大提升 SAT
判定的效率, 因此 DPLL(T) 算法优先进行 SAT 判定, 必要时才进行难度更高的背景理论判定.
算法 1. DPLL(T) 算法基本框架.

输入: 一个背景理论 T 的公式 φ in , 符号表为 Σ;
输出: 当 φ in 在背景理论 T 下可满足, 则输出 SAT, 否则输出 UNSAT.
1. φ := quant_elim(φ in )
2. F := φ a
3. while true do
4. A := get_model(F)
5. if A == none then
6. return UNSAT
7. else
c
8. µ := check_sat T (A )
9. if µ == SAT then
10. return SAT
11. else
12. F := F ∧¬µ a
13. end
14. end
15. end
DPLL 算法: 这里我们简单介绍 SAT 判定的 DPLL 算法. DPLL 算法得名于该算法发明人: Davis-Putnam-
Logemann-Loveland. 它的基本思路可以理解为通过不断地尝试给变量赋值, 在发现冲突 (即某一个赋值使得公式
出现矛盾) 时回溯, 逐步缩小搜索空间, 最终找到满足布尔公式的解或证明原公式不可满足. 20 世纪 90 年代开始,
在 DPLL 框架上涌现出许多优化技术, 极大提升了算法效率. 最显著一个优化是被称为冲突子句学习 (conflict
driven clause learning, CDCL) 的技术. 它相比 DPLL 框架最大的区别在于对冲突分析和回溯的技术. 当它发现冲突
时, 不会简单回溯尝试其他赋值, 而是从冲突中学习一个新的子句, 将该子句添加到原问题公式中, 从而避免未来
出现类似冲突, 减少搜索空间. 另外 CDCL 算法优化了原来根据决策变量顺序回溯的机制, 而是根据冲突分析进
行计算, 基于学习到的子句直接跳到导致冲突的决策层.
2.2 代数数据类型理论的判定算法

本节主要介绍无量词代数数据类型理论的判定算法. 公式只含有代数数据类型中的构造子、选择子等符号.
即本节研究的问题中待求解公式的形式如例 2 中的公式 (1).
目前主流 SMT 求解器对无量词 ADT 公式的基本求解框架是先对 ADT 公式的结构进行展平, 逐步猜测变量
对应构造子, 然后构建同余闭包进行判定. 在实现中一般采用一些启发式优化策略, 在猜测对应构造子、消去选择
子等基本结构这些过程中进行剪枝, 从而缩减由于复杂结构带来的搜索空间爆炸问题. 但面对公式规模较大且包
含多种数据类型的情况时求解效率依然有限. 下面具体介绍相关算法.
对于无量词代数数据类型理论公式的判定, 最早由 Oppen 等人 [2,29] 在 1980 年提出了一种线性时间判定算法,
通过代数数据类型公式构造有向图, 计算图中节点的同余闭包 (congruence closure) 从而得到公式中相关项 (term)
的等价关系来进行判定, 但该算法只适用于单个归纳数据类型且带有单个构造子 (constructor) 的递归定义数据结构.
对于更一般的问题, 如允许互递归数据类型以及数据类型中包含多个构造子的情况, 其判定问题被证明是