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

512 软件学报 2026 年第 37 卷第 2 期

EUF)、位向量 (bit vector, BV)、数组 (array)、线性整数算术 (linear integer arithmetic, LIA)、线性实数算术 (linear
real arithmetic, LRA)、非线性整数算术 (nonlinear integer arithmetic, NIA)、字符串 (string)、代数数据类型
(ADT) 等. 求解 SMT 公式可满足性问题的工具被称为 SMT 求解器, 目前, 主流的 SMT 求解算法是 DPLL(T) 算法 [21,22] ,
主流求解器有美国微软公司开发的 Z3 求解器 [23] 、美国斯坦福大学和爱荷华大学开发的 cvc5 求解器 [24] (注意这
里关于求解器名称的大小写问题, 根据 cvc5 相关论文 [24] , 在 CVC4 以前的求解器名称均使用大写字母“CVC”, 而
cvc5 决定使用小写的“cvc”字母)、由 Armin Biere 团队开发的 Boolector 求解器等 [25,26] . 另外基于 superposition 推
理系统 [27] 主流自动定理证明工具, 如英国曼彻斯特大学的 Kovács 等人 [11] 开发的 Vampire, 也能够接收 SMT 公式
作为输入, 通过自动推理技术来实现对 SMT 公式的证明和求解 [28] .
1.2 一阶逻辑
本节简单介绍本文可能涉及的一阶逻辑相关背景的基本概念和符号标记. 其中文字 (literal)、子句 (clause)、
∃ ∀ 等基本概念本文不再赘述.
逻辑连接符 ¬, ∧, ∨, ←, ↔ 以及全称量词 ,
前文提到 SMT 相比 SAT 的主要区别在于考虑“多种数据类型”和相应的一阶逻辑理论, 这里我们定义多种数
据类型记号 (multi-sorted signature) 为如下几种符号集合: 函数符号 (function symbol) 的集合 F 、谓词符号
P 、类型的集合 . 每一种符号都具有一个元数 (arity). 其中 0 元的函数被称为常数
(predicate symbol) 的集合 S
f g 表示函数符号, ,
x y
(constant). 我们使用 ⊤ 与 ⊥ 表示 0 元谓词 true 与 false. 一般用字母 , p q 表示谓词符号, , 表
示变量. 使用符号集合与变量递归定义“项 (term)”, 一般用字母 s t , 表示. 当一个项不包含变量时我们称其为基项
(ground term). 一个被解释符号 (interpreted symbol) 是一个意义被定义的函数或谓词. 例如当我们引入等式理论
(equality), 则等号符号“=”是等式理论中的被解释符号.
等式理论 (equality): 在一阶逻辑的语言中加入表示项 (term) 相等的二元谓词: “=”. 这里“=”作为被解释符号,
含义由等式理论中的公理所定义. 我们有如下公理.
1) ∀x. x = x (自反性, reflexivity).
2) ∀x,y. x = y → y = x (对称性, symmetry).
3) ∀x,y,z. x = y∧y = z → x = z (传递性, transitivity).
n
f ∀¯x, ¯y. (∧ x i = y i ) → f(¯x) = f(¯y) (函数同余性, function congruence).
4) 对任意正整数 n 和 n 元函数符号 ,
i=1
n
p ∀¯x, ¯y. (∧ x i = y i ) → p(¯x) ↔ p(¯y) (谓词同余性, predicate congruence).
5) 对任意正整数 n 和 n 元谓词符号 ,
i=1
其中, ¯ x 表示变量列表 (x 1 ,..., x n ).
一个解释 (interpretation) M 是公式 F 的一个模型 (model), 我们记作 M ⊨ F, 此时 F 在模型 M 中取值为 true.
进一步, 如果 F 存在至少一个模型, 则称其为可满足的; 反之则称其为不可满足的. 对于公式 F, 如果所有的解释都
F 是有效的 ⊨ F. 一个位置
是它的模型, 则称 (valid), 记作 (position) 是一个正整数的有限序列, 定义为 n· p, 其中 p
ϵ
是一个位置, n 是正整数; 用 表示空序列, 称为根位置 (root position). 位置用于表示项的子项. 设 t 为项, p 为位置,
则 t 在 p 处的子项记作 t| p . 其归纳定义如下: (1) 当 p = ϵ 时, t| ϵ = t; (2) 当 p = i· p 且 t = f(t 1 ,...,t n ) 时, 其中 1 ⩽ i ⩽ n,
′
ϵ
t| p = t i | p ′ . 例如对形如 f(g(a,b)) 的项, 有 f(g(a,b))| ϵ = f(g(a,b)), 表示该项取位置 时得到它自身. f(g(a,b))| 1·2·ϵ = b,
,
,
表示对 f(g(a,b)) 取位置 1·2·ϵ 得到 b, 即 f(g(a,b))| 1 = g(a,b) g(a,b)| 2 = b b| ϵ = b.
一个替换 (substitution) θ 是一个形如 {x 1 7→ t 1 ,..., x n 7→ t n } 的映射, 其中 x 和 分别为一阶逻辑理论中的变量和
t
E 上, 一个替换的应用 E
项, 且对任意 1 ⩽ i, j ⩽ n, i , j, 有 x i , x j . 在一个表达式 (application) 记作 Eθ. 这里表达式
E
中所有的 x i 都被 t i 所替换. 对依赖某个变量 x 的表达式 , 我们记作 E[x]. 当 x 被一个洞 (hole) (用于表示一个占位
s
t
符) 或一个项 t 替换时, 我们分别记作 E[·] 和 E[t]. 对项 中某个位置 p 的子项被 替代时, 可以表示为 s[t]| p , 或简
θ
t
t
s
写做 s[t]. 当一个替换 满足 sθ = tθ 时, 称其为两个项 和 的合一子 (unifier). 此时称 s 和 为可合一的 (unifiable).
x、 y、 是变量, a 是常数, θ = {x 7→ a,y 7→ z}, 那么应
z
例如两个项 s = f(x,y) 和 t = f(a,z), 其中 f 是函数. 定义替换
,
t
t
用替换 sθ = f(a,z) tθ = f(a,z), 有 sθ = tθ, 则 θ 是 s 和 的合一子. 对于项 s 和 的合一子 θ, 如果他们的每一个合一子
θ
t
η, 都存在一个替换 µ 使得 η = θµ, 则称这个合一子 为 s 和 的“most general unifier”, 简称为“mgu”, 即 θ = mgu(s,t).