🤖 AI

How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization

本文介绍了一种利用对称性破缺层列表表示法和先进剪枝技术的新型分枝定界算法，该算法显著缩短了归结证明长度，通过将证明规模减少 25–60%，在寻找最短不可满足性证明方面，其性能优于最先进的求解器，且解决的实例数量是其两倍。

原作者： Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović

发布于 2026-08-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在现代计算领域，软件通常扮演着不知疲倦的逻辑学家的角色，检查一组复杂的规则是否能同时得到满足。这个过程被称为命题可满足性（propositional satisfiability），它是从验证微芯片安全性到规划自主机器人运动等各种应用背后的引擎。当计算机程序发现一组规则包含矛盾——即没有任何可能的实事排列方式能使它们全部为真时——它会宣布该问题是“不可满足的”。几十年来，该领域研究人员的主要目标一直是快速找到解决方案。然而，一个新问题出现了：如果计算机说一个问题是不可能的，我们如何能绝对确定它是正确的？答案在于一种证明，即一条证明不可能性的逐步逻辑链。这条链被称为“证明”。虽然现代计算机在寻找这些证明方面速度极快，但它们并不总是能高效地找到最短的证明。一个不必要的冗长证明就像是一个让旅行者绕远路、欣赏风景的地图，尽管存在直达路径，但它浪费了时间和资源；而在高风险的验证任务中，更短的证明更容易被检查和信任。

代尔夫特理工大学的一个研究小组开发了一种新方法来搜寻这些最短可能的证明。他们的工作解决了这样一个特定的挫折：虽然目前的软件可以在几秒钟内生成一个有效的不可满足性证明，但该证明可能比必要的长度要长得多。事实上，对于许多标准测试问题，现有最佳软件生成的证明被发现至少比现有的绝对最短证明长百分之五十。研究人员意识到，寻找最短证明不仅仅是让现有软件运行得更快的问题；它是一个独特的优化问题，类似于在广阔且多雾的迷宫中寻找单一的最有效路径。挑战在于，可能的路径数量如此庞大，以至于逐一检查是不可能的。该团队的突破在于发明了一种新的组织这些路径的方法，以消除冗余搜索，并创建一个能够在完全探索之前就剪掉死胡同的系统。

其创新的核心是一种新的表示证明本身的方法，他们称之为“层级列表”（layer list）。想象一下，将证明视为一个建筑工程，新的事实建立在旧的事实之上。传统方法经常会对这些事实添加的顺序感到困惑，仅仅因为它们的组装顺序不同，就将两组相同的实事视为不同的问题。这造成了大量的无效重复搜索。新的层级列表方法根据事实的“间接层级”对其进行分组，本质上是根据推导这些事实所需的逻辑步骤将其组织成层级。这种结构打破了此前减慢搜索速度的所有混乱对称性，确保计算机只对每个唯一的实事集合进行一次查看。通过这种方式组织搜索，研究人员可以设计出一种“分支界限”（branch-and-bound）算法。这是一种系统的策略，计算机在探索证明树的不同分支时，如果它计算出该路径必然比它已经找到的解更长，就会立即停止探索该分支。

为了使这种搜索更加高效，团队引入了几种剪枝技术，或者说是切断无用路径的规则。其中一个规则涉及识别“前沿”子句（frontier clauses），即当前规则集中最核心的事实。研究人员证明，任何证明都可以仅使用这些核心事实进行重写，而不会使证明变得更长。如果一个潜在的证明步骤依赖于一个已被更强、更核心的事实所覆盖的非核心事实，算法会立即丢弃该步骤。另一个强大的工具是“支配”（dominance）检查，即计算机将当前的搜索状态与之前访问过的状态进行比较。如果当前的路径明显比已经探索过的路径更差——意味着它使用了更多的步骤或更少的核心事实——计算机就会放弃它。最后，他们建立了一个数学下界，即基于产生矛盾的最小规则子集所确定的任何证明的最小可能长度。如果当前的搜索路径不可能超越这个最小值，算法就会停止在该路径上浪费时间。

当研究人员测试这种新方法时，结果非常显著。在处理一组来自2002年竞赛的标准测试问题时，他们的方法将现有最先进软件生成的证明长度减少了百分之三十到百分之六十。在较小的合成公式上，减少幅度在百分之二十五到百分之五十之间。在许多情况下，证明长度缩减了一半。此外，当目标是寻找绝对最短的证明并证明不存在更短的证明时，他们的方法解决的问题数量是之前最佳方法的两倍，且速度快了几个数量级。对于两种方法都能解决的问题，新方法明显更快，通常在几秒钟内就能完成旧方法需要数小时才能完成的任务。然而，研究人员也发现了其成功的局限性。该方法在证明变得极其庞大时（具体为超过一百万步时）表现稳定，但在这种规模下，存储证明结构所需的内存超出了当前计算机的处理能力，导致程序崩溃。

这项工作并不声称要让原始的寻找证明的软件过时；相反，它提供了一个精炼这些系统输出的强大工具。研究人员强调，虽然更短的证明通常更容易验证，但更短的证明并不自动意味着原始软件寻找它的速度更快。这种新方法的目的是为为什么一个问题没有解提供一个更清晰、更高效的辩解。通过剥离冗余步骤并专注于最直接的逻辑路径，该团队提供了一种让人工智能的推理过程更加透明和可靠的方法。他们的研究结果表明，对于许多问题而言，证明长度的“提升空间”是巨大的，并且通过改变我们组织这些证明搜索的方式，我们可以揭示那些一直存在、只是隐藏在层层不必要的复杂性之后的解决方案。

技术摘要：发现最短、更短及最短的 UNSAT 公式证明

问题陈述

现代 SAT 求解器是强大的工具，能够确定命题公式的可满足性并生成不可满足（UNSAT）实例的归结证明（resolution proofs）。这些证明对于验证至关重要，能够确保求解器的“UNSAT”结论是正确的。然而，尽管像 CaDiCaL 这样的现代求解器在经验上能产生相对较短的证明，但并不能保证这些证明是最短的。

寻找最短归结证明的问题是一个优化问题，其可行集是给定公式的所有有效证明集合，目标是最小化证明长度（子句数量）。该问题比仅仅寻找一个有效的证明要困难得多，因为其搜索空间呈指数级增长且具有高度对称性。先前的工作（如 Peitl 和 Szeider (2021)）尝试通过 SAT 编码来解决此问题，但由于搜索空间的爆炸和不完整的对称性破缺，仅限于非常小的公式（最多约 12 个子句）。

方法论

作者提出了一种全新的分支定界算法（branch-and-bound algorithm），旨在枚举归结证明并找到最短的一个。其核心方法论依赖于三个主要组成部分：一种新的证明表示法、一种特定的分支策略以及高级剪枝技术。

1. 层列表表示法 (Layer List Representation)

为了解决置换对称性问题（即重新排列子句会产生不同但等价的证明），作者引入了层列表表示法 $(L_0, L_1, \dots, L_n)$ 。

结构： $L_0$ 包含公理（原始公式子句）。随后的每一层 $L_j$ 包含通过将前一层（ $L_{j-1}$ ）中的一个子句与早期层（ $L_0 \cup \dots \cup L_{j-1}$ ）中的任意一个子句进行归结而得到的子句。
“要么取之，要么弃之”属性 (Take-it-or-leave-it Property)： 一个关键约束规定，如果一个子句可以在更早的层中被推导出来，则它必须被放置在该层。这防止了一个子句在能够被更早推导出的情况下出现在后续层中。
唯一性： 定理 2 证明，对于任何构成证明的子句集，存在且仅存在一个唯一的规范层列表表示。这种表示法打破了由子句置换引起的对称性，这与之前的基于 DAG 的编码不同，后者可以用不同的拓扑排序表示同一组子句。

2. 分支定界搜索

该算法将层列表的构建视为对子问题的递归搜索。

子问题定义： 子问题 $P$ 追踪 Previous（前 $k-1$ 层的子句）、Current（第 $k$ 层的子句）、Next（第 $k+1$ 层的候选子句）以及 Forgotten（本可以更早推导但未包含在内的子句）。
划分： 算法不是枚举所有归结项的子集，而是针对下一层的单个候选子句进行分支。它决定是将一个候选子句包含在 Next 层中，还是将其移至 Forgotten 集合，从而有效地探索有效层列表的空间。

3. 剪枝与优化

搜索过程由若干剪枝程序引导，以消除非最优分支：

前沿剪枝 (Frontier Pruning)： 算法将推导限制在“前沿”子句（未被其他已知子句包含/覆盖的子句）上。定理 3 确立了任何使用非前沿子句的证明都可以转化为仅使用前沿子句的证明，且不会增加长度。
支配剪枝 (Dominance Pruning)： 定义了子问题之间的支配关系。如果子问题 $P'$ 支配 $P$ （意味着 $P'$ 使用了更少或相等的公理、可以推导出更多的子句、拥有更多的前沿，并且遗漏了更少的子句），那么从 $P$ 中可以恢复的任何证明也可以从 $P'$ 中恢复，且长度相等或更优。被支配的子问题会被丢弃。
下界估计 (Lower Bounding)： 算法使用最小不可满足子集（SMUS）的大小来估计剩余证明长度的下界。具体而言，它利用了这样一个事实：对于具有 $m$ 个子句的极小不可满足公式，至少需要 $2m-1$ 步。该界限通过使用 Forqes 包或自定义的分支定界程序计算 SMUS，被推广到了非极小公式上。

核心贡献

层列表表示法： 一种新型证明编码，能将任何证明子句集唯一地映射到单一结构中，打破了所有的置换对称性，并改进了现有的基于 DAG 的对称性破缺方法。
分支定界算法： 一种作用于层列表前缀的完备搜索程序，能够找到最优（最短）的归结证明。
剪枝机制： 一套剪枝技术，包括基于前沿的简化、基于子问题的支配关系以及基于 SMUS 的下界估计。
随时运行能力 (Anytime Capability)： 该算法作为一个随时运行的优化器，在整个搜索过程中提供有效的上界（目前找到的最短证明）和下界。

实验结果

作者在两个数据集上评估了他们的方法：合成公式（例如，Pigeonhole、Parity、Random 3-CNF）和 SAT Competition 2002 的 UNSAT 实例。

证明长度缩减：
- 在合成公式上，该方法与 CaDiCaL 相比，证明长度减少了 25% 到 50%。
- 在 SAT Competition 2002 实例上，证明缩短了 30% 到 60%。
- 在特定案例（如子集基数公式）中，一致观察到至少 40% 的缩减。
最优性与速度：
- 与 Peitl 和 Szeider (2021) 的基准方法相比，所提方法求解达到最优状态的实例数量增加了一倍。
- 对于两者都解决的实例，所提方法将达到最优所需的时间降低了数个数量级（例如，将求解 9 子句公式的时间从数千秒缩短至数秒）。
- 该方法成功计算了高达 8 子句公式的归结硬度数 ( $h_m$ )，并部分计算了 9 子句的情况，在执行时间上显著优于基准方法。
局限性：
- 该方法对内存需求较高。当 CaDiCaL 的证明长度超过约 $10^6$ 步时，会遇到内存溢出错误，因为算法必须解包并存储大型归结证明以进行分析。
- 下界剪枝受限于 SMUS 的计算；对于某些公式（如 Pigeonhole），该界限不够紧凑，无法有效地剪枝搜索。

重要性

该论文声称其主要意义在于证明了：最先进的 SAT 求解器生成的证明往往远非最优，并且这些证明是可以系统性缩短的。通过引入对称性破缺表示法和高效的分支定界搜索，作者提供了一种方法来实现：

验证求解器效率： 估算求解器步骤中的“改进空间”，揭示标准求解器可能比必要步骤多消耗了 50% 到 200% 的步骤。
优化证明系统： 为证明最小化提供了一种比以往精确方法更具扩展性的工作流。
推进证明复杂度研究： 提供了一个计算归结硬度数和探索极小证明结构的实用工具，这对理解命题逻辑问题的内在复杂性具有重要意义。

作者总结道，虽然他们的方法在处理极大型证明时存在内存限制，但它代表了在自动发现最优归结证明方面迈出的实质性一步，比之前的基于 SAT 编码的方法更快地解决了更多实例。