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

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

k 为斯科伦 (Skolem) 常数. 然后
∃¬P(x) → ¬P(k), 这里不展开介绍). 对 ¬∀x. P(x) 进行斯科伦化, 得到 ¬P(k), 称
¬P(k) 将被加入 F 中, 为便于讨论, 我们假设这里 ¬P(k) 已经是一个无量词公式. 于是 SMT 求解器将尝试调用内置
¬P(k) 的可满足性. 而在例 4 中我们将看到在没有引入归纳推理能力时, SMT 求解器无法完成对该
决策过程求解
问题中 ¬P(k) 的求解.
一个失败的推理过程: 对 ψ 进行斯科伦化之后得到公式集合 F := {A 1 ,A 2 ,¬ψ,¬len(k) ⩾ 0}. 由 {A 1 ,¬len(k) ⩾ 0},
SMT 求解器找到一个模型 k = cons(h,t) 且 len(k) = −1. 这里表示 k 是一个由 h 与 构造的类型为 list 的常数, 且长
t
度为 −1. 将这一模型代入 A 2 进行实例化, 得到 len(cons(h,t)) = 1+len(t). 于是 len(t) = −2. 再一次进行实例化, 将会
得到存在 hh 和 tt, 使得 t = cons(hh,tt), 且 len(t) = 1+len(tt). 从而 len(tt) = −3. 这一过程将会无限循环进行, 使求解
失败. 其原因在于当带量词的代数数据类型理论公式为 false 时, SMT 进行判定的公理模型是不标准模型 (non-
standard model), 即 SMT 求解器中包含的相关理论公理不足以满足我们对形如例 4 的问题进行证明.
归纳推理增强: 在 Reynolds 等人 [31] 通过对斯科伦化过程中引入归纳推理增强来解决上述问题. 假设当前类型
的公式项存在一个良基序 (well-founded ordering) R, 那么存在 k, 使如下公式成立:

(∀x. P(x))∨(¬P(k)∧∀x. (R(x,k) → P(x))) (2)

此时称 ∀x. R((x,k) → P(x)) 是 ¬P(k) 基于 R 的归纳增强 (inductive strengthening).
这一归纳增强方法可以视作将一种归纳模式 (induction schema) 引入 SMT 求解过程. 公式成立的具体证明过
程可参考文献 [31] 第 2 节 Remark 1.
从直观上看, 若对任意 x, P(x) 成立, 则公式 (2) 成立; 否则存在 y 使得 P(y) 不成立, 即 ¬P(y). 我们假设所有这
样的 y 构成集合 S, 则 S 不为空集, 对 S 中任意的一个元素 y 0 , 考虑从 y 0 出发的极大良基关系序列 y 0 ,y 1 ,... ∈ S , 其
中任意下标 i, 满足 R(y i+1 ,y i ). 那么由良基关系, 该序列必然是有限的, 令其在某个 y n 终止. 那么令 k 为 y n , 满足 ¬P(k),
且由于 y n 是序列中最后一个元素, 满足 ∀x. (R(x,k) → P(x)).
通常在 SMT 求解中根据待求解公式的背景理论, 有两种典型的良基关系 R 被使用: 在代数数据类型理论中,
t
对于代数数据类型的项 s 与 , s 是 的子项. 这对应使用结构归纳法的求解模式. 在整数理论中, 对
t R(s,t) 当且仅当
0 ⩽ s ⩽ t. 这对应使用数学归纳法的求解模式. 为了简化求解, 在实际的 SMT
于整数 s 和 t, 则通常 R(s,t) 当且仅当
求解器 cvc5 中, 实现了弱归纳法的求解模式: 对于代数数据类型的项 s 和 , s t
t R(s,t) 当且仅当 是 的直接子项, 例
s
如 list 类型中的 tail 项与原项. 对于整数 和 t, 则 R(s,t) 当且仅当 0 ⩽ s = t −1.
成功求解例 4: 引入归纳推理增强之后, 例 4 可以被成功求解. 此时对于 ψ, 将产生公式 ¬len(k) ⩾ 0∧∀y. (y =
tail(k) → len(y) ⩾ 0). 该公式化简为 len(k) < 0∧len(tail(k)) ⩾ 0. 而由 A 2 可推知 len(tail(k)) < len(k). 于是矛盾, 求解器
返回 UNSAT, 原命题 ψ 得证.
2.4 辅助证明引理生成技术
我们分别介绍目前 SMT 求解器 cvc5 中所实现的证明引理生成技术和近年来提出的其他引理生成技术.
2.4.1 cvc5 求解器引理生成技术
尽管在 SMT 求解的量词消去过程中引入归纳推理增强可以成功解决例 4, 但实际在许多情况下, 只引入归纳
推理增强依然不足以完成公式求解, 还需要结合启发式的子目标生成技术自动在公理集合中引入“中间引理”或
“子目标”来完成求解. 这一过程类似于程序验证问题中为循环程序引入循环不变式, 或补充前置或后置条件, 可以
视作一种对原已有条件的加强. 如何更好地自动生成引理以辅助 SMT 公式的求解是领域内一个重点研究方向, 在
第 3 节将对现有的重点方法进行梳理和介绍. 这里我们介绍 Reynolds 等人 [31] 的子目标生成方法, 该方法实现在
cvc5 求解器中. 通过自动生成子目标来证明待验证公式 ψ 的基本思路如下: 1) 首先确定相关 (relevant) 子目标 φ 1 .
2) 证明 φ 1 成立. 3) 将 φ 1 放入前提公式集合, 在 φ 1 成立的前提下证明 ψ.
实际的 SMT 求解过程在找到一个相关子目标 ∀x. f(x) = g(x) 之后, 会在公式集合中加入分离引理 (splitting
lemma): ¬∀x. f(x) = g(x)∨∀x. f(x) = g(x). 然后分别考虑 ¬∀x. f(x) = g(x) 和 ∀x. f(x) = g(x) 两种可能分支的情况.
在进行子目标生成时, Reynolds 等人 [31] 的基本方法是先基于已知符号枚举可能的公式, 然后通过启发式过滤方法