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

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

解, 则统计到表 7 样例来源 Z3/cvc5/Vampire 下; 若能被 Spacer/Racer/Eldarica 中任意求解器求解, 则统计到样例来
源 Spacer/Racer/Eldarica 下; 若能被这里所有求解器中任意求解器求解, 则统计到样例来源任意工具下. 括号中的
百分比表示求解数占这一类样例总数的比例.
将表 7 括号中的百分比分别与表 5、表 6 括号中的百分比进行对比, 可以看出, 类似算法的求解工具可求解
样例重合度较大, 百分比提升不明显, 但如果考虑不同算法综合求解能力, 则求解数提升较大: 对于整数样例,
Z3/cvc5/Vampire 和 Spacer/Eldarica 这两类工具中, 单一求解器表现最好的分别是 Vampire 和 Eldarica, 解出数比
例分别为 37.84% 和 47.30%. 如表 7 样例来源为 Z3/cvc5/Vampire 下, 整数样例总解出数的结果所示, 如果分别考
虑每一类工具, 则能被任意 Z3/cvc5/Vampire 求解样例数为 52.25%, 相比 Vampire 提升 52.25%–37.84%=14.41%;
能被任意 CHC 求解器求解比例为 48.65%, 相比 Eldarica 提升了 48.65%–47.30%=1.35%. 这两者提升都较为有限.
但如果综合所有工具来看, 能被任意工具求解的样例数占比为 69.37%. 提升比例达到 69.37%–37.84%=31.53% 和
69.37%–47.30%=22.07%. 相比只考虑单一种类算法的情况提升较大. 类似地对比 ADT 样例中待证明数据结果,
Z3/cvc5/Vampire 和 Spacer/Racer/Eldarica 中表现最好的分别为 cvc5 和 Racer, 求解比例如表 6 中数据 44.05% 和
23.21%. 同类算法求解比例分别为 47.62% 和 24.40%, 表明分别看两类求解器, 那么在每一类求解器中最优求解器
求解样例基本覆盖其他求解器能求解的样例. 但如果综合所有求解器来看, 求解比例为 60.12%, 相比 cvc5 和
Racer 分别提升了 60.12%–47.62%=12.5% 和 60.12%–24.40%=35.72%, 具有一定的提升效果, 这表明两类工具所能
求解样例可以在一定程度上互为补充.

表 7 所有待证明样例不同求解算法对比结果

样例来源 总数 Z3/cvc5/Vampire Spacer/Racer/Eldarica 任意工具
文献[55]样例 120 86 86 108
手工构造样例 102 30 22 46
整数样例总解出数 222 116 (52.25%) 108 (48.65%) 154 (69.37%)
ADT和整数混合理论待证明样例 168 80 (47.62%) 41 (24.40%) 101 (60.12%)
所有待证明验证总解出数 390 196 (50.26%) 149 (38.21%) 255 (65.38%)

6 总 结

本文主要关注带有递归定义的 SMT 公式求解技术. 我们对求解 SMT 公式的 3 类主流工具: SMT 求解器、自
动定理证明器以及 CHC 求解器分别进行介绍. 在每一类工具中详细展示了通用判定算法和针对递归定义的专用
求解技术.
对于 SMT 求解器, 我们从通用的 DPLL(T) 判定算法开始, 介绍了无量词代数数据类型的理论判定算法和为
求解递归函数问题的归纳增强与子引理生成技术. 对于自动定理证明器, 我们从推理框架开始, 介绍了近年来在推
理系统中引入自动归纳推理的一系列工作.
上述两类是目前直接求解 SMT 公式的主流方法和工具, 它们都基于在原求解判定框架中引入归纳推理方法
来提升对带有递归函数的 SMT 公式的求解能力. 可将它们归为第 1 类方法, 根据我们对这类方法相关文献的整
理, 可以发现这类方法的引入来源于认识到带有递归定义的 SMT 公式尽管表示形式极为复杂, 但具有特定的归纳
结构, 于是可以通过在求解环境中引入表示归纳推理的基础步骤公式和归纳步骤公式的两类特定公式来实现“归
纳推理增强”. 使得求解工具具有自动进行归纳证明的能力, 不带有归纳推理增强的原算法则几乎无法自动求解任
何递归函数问题. 另外在引入归纳推理增强的基础上, 辅助证明引理的生成技术对求解效率起到非常大的作用. 这
是由于求解器缺少对用未解释函数和 ADT 结构表达的递归函数问题基本性质的理解, 辅助引理的引入, 可以提供
必要的公理, 来提高求解器对递归函数相关计算关系和性质的认识, 帮助对复杂公式进行化简. 因此基于 SMT 求
解和自动定理证明求解的方法, 主要的研究重点是在引入必要的归纳推理模式基础上, 进一步提升求解过程中辅
助证明引理生成的效率和质量.