跳转至

文章背景与核心概要

在软硬件形式化验证与程序分析中，可满足性模理论 (Satisfiability Modulo Theories, SMT) 求解器是至关重要的底层推理引擎。面对含有量词的复杂一阶逻辑命题，传统 SMT 求解器通常依靠“量词实例化”将其降解为无变量的具体基项 (Ground Instances) 并结合 CDCL(T) 算法进行冲突分析，但这种方法学到的冲突子句往往过于狭隘具体，错失了利用高阶非基项结构将证明长度实现指数级精简的良机。为此，本研究（LPAR 2026 扩展论文）提出了一种创新的统一演算体系，将基项实例化、CDCL(T) 规则与高阶非基项冲突分析有机融合。求解器在具体基项上高效推理，而在原始非基项子句上执行归结消解，从而提炼出更通用、无冗余的泛化子句，并成功引入时间次回溯机制，从数学上证明了该框架能够统一模拟 CDCL、SCL 及一阶逻辑消解法。

引入非基项子句学习拓展 SMT 求解能力

Extending SMT Solving with Non-Ground Clause Learning

核心概述

Summary

量词实例化是求解含有变量的非基项可满足性模理论 (Satisfiability Modulo Theories, SMT) 问题的传统主流手段。在这一框架下，求解器首先生成具体的基项实例 (Ground Instances)，随后应用带有理论扩展的冲突驱动子句学习 (CDCL(T)) 风格的算法进行推理。然而，标准的冲突分析过程仅能学习到具体的基项子句，无法捕捉深层的非基项变量结构，从而错失了在理论上将证明长度缩减数个数量级（指数级精简）的绝佳机会。

Quantifier instantiation is the traditional approach to non-ground Satisfiability Modulo Theories (SMT) solving, where solvers generate ground instances and apply CDCL(T)-style reasoning. However, standard conflict analysis only learns ground clauses, failing to capture the underlying non-ground structure from which exponential proof-length savings could otherwise be derived.

本文（作者 Yasmine Briefs 和 Christoph Weidenbach 在 LPAR 2026 录用论文的扩展版本）提出了一种统一的逻辑演算体系，将基项实例化、CDCL(T) 推理规则与非基项冲突分析深度结合。通过在原始非基项子句上直接执行归结消解 (Resolution) 步骤，求解器能够提炼出通用性更强、且不含冗余的学习子句，同时还成功融入了时间次回溯 (Chronological Backtracking) 机制。作者从形式化逻辑上严密证明了该框架能够完整模拟 CDCL、SCL(FOL)、SCL(T) 以及经典的一阶消解法。

This paper—an extended version of the LPAR 2026 paper by Yasmine Briefs and Christoph Weidenbach—proposes a unified calculus combining ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. By performing resolution steps on original non-ground clauses, the solver yields significantly more general, non-redundant learned clauses, while also successfully integrating chronological backtracking. The authors formally prove that this framework simulates CDCL, SCL(FOL), SCL(T), and standard Resolution.

元数据与文档信息

Metadata & Document Information

字段 详情
arXiv 编号 arXiv:2609.11509 [cs.AI]
主要学科领域 人工智能 (cs.AI)
次要学科领域 计算机科学中的逻辑 (cs.LO)
作者 Yasmine Briefs, Christoph Weidenbach
提交日期 2026年9月10日
备注说明 LPAR 2026 会议论文的扩展版
DOI 链接 10.48550/arXiv.2609.11509
Field Details
arXiv Identifier arXiv:2609.11509 [cs.AI]
Primary Subject Artificial Intelligence (cs.AI)
Secondary Subjects Logic in Computer Science (cs.LO)
Authors Yasmine Briefs, Christoph Weidenbach
Submission Date September 10, 2026
Comments Extended version of LPAR 2026 paper
DOI 10.48550/arXiv.2609.11509

论文摘要

Abstract

量词实例化目前是非基项 SMT 求解的主流方法：求解器生成基项实例，并利用 CDCL(T) 风格的推理来求解派生出的基项 SMT 问题。当遭遇逻辑冲突时，现有的冲突分析仅学习基项子句，尽管该冲突实质上源自非基项子句的实例化。然而，非基项推理相比于纯基项推理，能够产生呈指数级简短的证明过程。我们提出了一种包含基项实例化、CDCL(T) 风格规则和非基项冲突分析的新型演算。求解器在基项实例上进行推理，但冲突分析的归结步骤直接作用于其原始的非基项子句。这使得学到的子句通常比基项冲突具备更高的通用性。在合理的策略下，学到的子句甚至完全不含冗余。我们还展示了如何将时间次回溯融入 SMT 求解过程中。我们的演算体系为 CDCL(T) 风格的 SMT 求解、一系列基于实例化的算法过程以及非基项子句学习提供了统一的理论框架，并证明了其能够模拟 CDCL、SCL(FOL)、SCL(T) 乃至经典消解法。

Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.

全文获取与外部资源

Full-Text & External Resources

文献与学术研究工具

Bibliographic & Research Tools