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

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

除了 SMT 求解器和自动定理证明器外, 我们还关注到可以通过 CHC 求解器来求解带有递归函数的 SMT 问
题. CHC 求解器主要用于软件模型检测问题中的程序验证问题, 而 ADT 和递归函数的递归结构, 也可以被表示成
CHC 求解程序验证问题算法需要的迁移系统形式. 在使用 CHC 求解 SMT 公式时, 需要先将 SMT 公式从通用形
式转换为 CHC 特定形式. 本文介绍了 CHC 求解的主流算法和通过 CHC 算法求解递归函数 SMT 问题的方法和
工具. 基于 CHC 求解的方法可以称为第 2 类方法, 与第 1 类方法最大的不同在于这类方法不通过归纳推理来求解
递归函数问题, 而是通过生成归纳不变式和递归函数展开的算法完成求解. 实验结果表明这一类方法能够与第 1
类方法互补.
我们通过从现有文献收集和手工构造的方式获得了两类具有程序验证背景的实验样例集. 分别是纯整数理论
样例集和 ADT 理论整数理论混合样例集. 在这两个样例集上进行实验, 然后对比分析了基于不同求解算法的几种
主流求解工具的表现. 实验结果表明, 现有求解器在求解带递归函数的 SMT 问题上可提升空间较大. 尤其是在“证
明”任务上, 对于这两类样例, 单一求解器能求解的数目均不到一半.
这些主流求解器中, 对于递归函数问题, Z3 没有实现自动归纳推理方法, 因此能求解数目最少, 但它实现了递
归函数的模型寻找方法, 可以求解一部分性质不成立的“找错”问题.
cvc5 的主要技术是基于归纳推理增强和引理生成算法, 它的综合表现较好, 在每一类问题上都能够解出一定
数量的问题, 但在整数归纳推理, 非线性理论求解等部分还有待加强, 可以考虑在 DPLL(T) 求解框架中引入类似
Vampire 的整数归纳推理模式. 并进一步提升其引理生成算法在复杂样例上的能力. 结合当下大模型在程序生成
和数学推理上的热门趋势, 或许可以基于大模型方法来帮助算法进一步理解复杂的递归函数公式, 并更好地生成
用于辅助证明的引理.
Vampire 的主要技术是在自动推理系统中引入各种归纳推理模式, 但它的引理生成算法较弱, 这导致它在手
工构造的复杂整数样例和 ADT 整数混合样例上求解表现均不如 cvc5. 虽然在推理系统中引入自动归纳证明的文
献较多, 但大多数集中在引入不同类型归纳模式, 这可以认为是一种“广度优先”思路, 能够提高推理系统能求解的
问题种类. 这一思路可以在其他求解算法未深入涉足的问题类型 (例如整数理论递归函数求解) 上取得优势, 但在
更通用问题类别上难以胜过其他工具. 需要进一步提升推理系统求解各种类型问题的“深度”, 如加强自动定理证
明工具对非线性理论和 ADT 理论背景公式的求解算法能力, 提升基于推理系统的辅助证明引理生成技术等.
CHC 求解器对于“找错”任务的处理能力好于 SMT 求解器和自动定理证明工具. 在“证明”任务上, 对于整数类
型问题的处理能力相对较好, 对于复杂的 ADT 理论问题的求解能力则有待提升. 而且得益于 CHC 求解算法基于
归纳不变式生成的原理, CHC 求解器可以求解一部分基于归纳推理方法无法求解的问题, 这提示我们可以尝试将
自动归纳推理算法与 CHC 求解的归纳不变式生成算法相结合, 帮助提升现有工具/算法应对复杂多样理论背景问
题的求解能力.

References
[1] Bjørner N, Gurfinkel A, McMillan K, Rybalchenko A. Horn clause solvers for program verification. In: Beklemishev LD, Blass A,
Dershowitz N, Finkbeiner B, Schulte W, eds. Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of
His 75th Birthday. Cham: Springer, 2015. 24–51. [doi: 10.1007/978-3-319-23534-9_2]
[2] Oppen DC. Reasoning about recursively defined data structures. Journal of the ACM (JACM), 1980, 27(3): 403–411. [doi: 10.1145/
322203.322204]
[3] Barrett CW, Shikanian I, Tinelli C. An abstract decision procedure for a theory of inductive data types. Journal on Satisfiability Boolean
Modeling and Computation, 2007, 3(1–2): 21–46. [doi: 10.3233/SAT190028]
[4] Reynolds A, Blanchette JC. A decision procedure for (co)datatypes in SMT solvers. Journal of Automated Reasoning, 2017, 58(3):
341–362. [doi: 10.1007/s10817-016-9372-6]
[5] Reynolds A, Viswanathan A, Barbosa H, Tinelli C, Barrett C. Datatypes with shared selectors. In: Proc. of the 9th Int’l Joint Conf. Held
as Part of the Federated Logic Conf. on Automated Reasoning. Oxford: Springer, 2018. 591–608. [doi: 10.1007/978-3-319-94205-6_39]
[6] Hojjat H, Rümmer P. Deciding and interpolating algebraic data types by reduction. In: Proc. of the 19th Int’l Symp. on Symbolic and
Numeric Algorithms for Scientific Computing. Timisoara: IEEE, 2017. 145–152. [doi: 10.1109/SYNASC.2017.00033]