Page 32 - 《软件学报》2026年第2期
P. 32

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


                 maton  中寻找有限模型    (finite model finder) 问题进行求解, 该方法实现在  RInGen  求解器中.
                    2) 递归函数求解: 递归函数是程序中除了递归数据结构外的另一种常见递归定义. 递归函数在一阶逻辑公式
                 层次一般表示为带有全称量词、ADT             理论、未解释函数理论和整数理论等混合理论的公式, 对这种混合理论公
                 式的求解具有较大的挑战性. 近年来有不少相关的研究工作发表在形式化领域的重要会议或期刊上, 但即使是最
                 好的算法和工具, 能处理的问题数目和形式也十分有限, 有较大的提升空间. 本文将分别介绍                            SMT  求解器、自动
                 定理证明器和     CHC  求解器所对应的一阶逻辑推理框架中对递归函数的处理方法.
                    SMT  求解器一般通过在      DPLL(T) 判定框架中加入归纳推理增强和自动生成辅助证明引理的方法来求解递归
                 函数问题. 如前文所述, 表示带有递归函数问题的一阶逻辑公式一般为包括全称量词、未解释函数、ADT                                 理论和
                 整数理论的混合理论公式. SMT         求解器在量词消去过程中引入表示归纳模式的断言, 然后通过一个专门的引理生
                 成模块来提升理论判定过程中对复杂的未解释函数、ADT                   理论和整数理论混合公式的处理能力.
                    自动定理证明器主要通过在推理系统中引入特定的归纳模式, 如结构归纳、整数归纳和基于函数定义的归纳
                 模式等, 作为新的推理规则来提升推理能力. 并结合启发式优化方法提升推理过程的效率.
                    CHC  求解器通过尝试生成归纳不变式来证明待验证目标. 这一类方法的思路可以理解为将带有递归函数的
                 逻辑公式判定问题视作检测迁移系统是否满足安全性质的模型检测问题. 在求解带递归函数                              SMT  公式时, 需要先
                 将  SMT  公式转换为   CHC  形式, 然后再调用    CHC  求解器. CHC  求解器对带有递归函数公式的求解依赖于其处理
                 量词、未解释函数、ADT        理论和整数理论的能力. 主流          CHC  求解器可以在一定程度上求解这类问题, 但求解能
                 力有限   (见本文第   5  节实验部分). 2022  年  Govind  等人  [15] 通过基于展开和抽象等特定的递归函数求解技术来提升
                 CHC  求解器处理递归函数问题的能力. 该方法在基于              CHC  求解器  Spacer 开发的  Racer 系统中实现.
                    总的来说, SMT    求解器和自动定理证明器主要关注在原推理框架基础上进行自动归纳推理增强, 并通过引理
                 生成方法来辅助提升求解效率. CHC           求解器直接通过      CHC  求解框架生成原递归函数的归纳不变式来进行验证,
                 并可以基于递归函数展开和抽象等技术来优化求解效率.
                    主流求解工具实验对比: 本文从现有文献中选择了包含整数理论和                      ADT  理论的公开数据集, 并从实际的程序
                 验证问题中构造了一部分数据集作为补充. 在这些数据集上我们对主流的求解工具进行了统一的实验对比和分
                 析, 并根据实验结果评估和分析了主流工具在不同类型的递归函数问题求解能力优劣. 本文期望为关注递归定义
                 求解、引理生成和       CHC  求解等领域的研究者梳理重点求解技术和主流工具, 提供潜在的改进优化思路, 探究可能
                 的研究方向.
                  1   相关背景知识

                    我们首先对本文涉及的一阶逻辑相关背景知识进行简单介绍, 包括可满足性问题、代数数据类型理论和
                 superposition  演算等相关内容.
                  1.1   可满足性问题和可满足性模理论
                    命题逻辑可满足性问题         (propositional satisfiability problem) 是逻辑学和计算机科学中重要问题, 一般简称为
                 SAT  问题, 指对于给定的一组布尔逻辑公式, 判定是否存在一组变量赋值使得该公式为真, 如果存在, 则称该公式
                 可满足   (SAT), 否则称为不可满足      (unsatisfiable, UNSAT). SAT  问题是第  1  个被证明的  NPC (non-deterministic
                 polynomial-time complete) 问题  [16] . SAT  被广泛应用于电子设计自动化  (electronic design automation, EDA) 和程序
                 验证分析等领域. 2000    年左右, SAT   求解算法取得突破, 可以处理大规模命题逻辑公式求解的                   SAT  求解器开始出
                 现并成为研究热点      [17–20] , 并且开始应用于工业界解决实际问题.
                    但  SAT  问题只考虑命题逻辑, 在许多实际场景下表达能力有限, 研究者考虑使用一阶逻辑公式与特殊背景理
                 论进行融合, 提出可满足性模理论           (SMT) 问题. SMT  的基本思想是针对多种数据类型和相应的一阶逻辑理论, 提
                 出一个一般的框架, 从而可以求解涵盖多种特定背景理论的一阶逻辑公式的可满足性判定问题. SMT                               涉及的理论
                 为一些数学理论和计算机领域内用到的数据结构理论, 主要理论包括等式未解释函数                           (equality uninterpreted function,
   27   28   29   30   31   32   33   34   35   36   37