Verification of a DPLL Transition System in Rocq

想象一个计算机在不断进行高风险“真或假”游戏的场景。在这个游戏中，计算机被交给一个巨大的、纠缠在一起的逻辑语句结——就像一个食谱说：“如果你加入了糖，你也必须加入面粉，但如果你加入了面粉，你就不能加盐。”寻找一种既能遵循食谱又不会破坏任何规则的方法，这就是目标。这就是可满足性问题（SAT）。这在数字领域相当于试图将一百万个不同的拼图碎片放入一个盒子中，而有些碎片是红色的，有些是蓝色的，且说明书规定：“红色不能与蓝色相邻。”

我们为什么要关心这个？因为这不仅仅是一个逻辑谜题；它是几乎所有复杂计算背后的引擎。从设计微芯片到证明一个数学定理是否成立，计算机都使用 SAT 求解器来穿越这些庞大的逻辑迷宫。但问题在于：这些求解器极其复杂。如果代码中隐藏了一个微小的漏洞，计算机可能会自信地告诉你一个证明是有效的，而实际上它是一堆废话。这就是为什么数学家和计算机科学家痴迷于形式化验证（formal verification）。把它想象成建造一个超级严格、不可破坏的安全网。与其仅仅希望计算机正常工作，不如使用一种特殊的“数学显微镜”（称为证明助手）来检查逻辑的每一个步骤，确保机器永远不会在答案上撒谎。

论文的大冒险：构建一台值得信赖的逻辑机器

在这篇论文中，Julia Dijkstra 和 Benedikt Ahrens 向着让这些逻辑机器变得值得信赖迈出了巨大的一步。他们不仅仅是写了一个程序；他们在名为 Rocq 的工具中，为一种著名的逻辑求解方法——DPLL（Davis-Putnam-Logemann-Loveland）构建了一个经过数学证明的骨架。

请不要把 DPLL 方法看作是一个死板地执行脚本的机器人，而要把它看作一场**“状态切换”的游戏**。想象一位侦探正在试图解开一个谜团。侦探从一本空白的笔记本开始（没有任何线索）。他们有一套关于如何更新笔记本的规则：

1. “噢，我明白了！”规则（单元传播/Unit Propagate）： 如果一条线索说“不是管家就是女佣”，而侦探已经知道女佣是清白的，那么笔记本必须更新为“是管家做的”。侦探别无选择；逻辑强制要求这一移动。
2. “纯粹猜测”规则（纯文字/Pure Literal）： 如果侦探看到一条关于“园丁”的线索，却从未看到任何关于“园丁不是干的”线索，那么他们可以安全地假设园丁参与其中，而不必担心产生矛盾。
3. “分支探索”规则（决策/Decide）： 如果侦探卡住了，他们会挑选一个随机线索（比如“是管家做的”）并将其作为一项决策记录下来。这是路口的一个分叉。
4. “哎呀，走错路了”规则（回溯/Backtrack）： 如果侦探做了一个决策，后来发现了一个矛盾（一条说“管家没做”）的线索，他们必须擦除该决策之后发生的所有事情，翻转该决策（现在变成管家没做了），然后重试。
5. “游戏结束”规则（失败/Fail）： 如果他们擦除了所有内容，翻转了最后一个决策，却仍然遇到了矛盾，那么游戏结束。这个谜团是无法解决的。

作者的主要成就，是将这整个游戏过程以 Rocq 可以读取并验证的语言记录了下来。他们不仅仅是说“这看起来没错”。他们证明了三件极其重大的事情：

• 正确性（Correctness）： 如果游戏以一个解结束，那么那个解一定是真实的。计算机不会凭空幻觉出一个模型。
• 完备性（Completeness）： 如果存在解，游戏一定会找到它。计算机不会在不该放弃的时候卡住或放弃。
• 终止性（Termination）： 游戏永远不会运行到死循环。它在数学上保证会停止，要么带着一个解，要么带着“游戏结束”。

加入新花样：“纯粹”规则

该论文的一个酷炫贡献是，他们在游戏中加入了一个之前版本的理论中遗漏的特定规则：纯文字规则（Pure Literal Rule）。在侦探的比喻中，这是侦探意识到：“嘿，我从未见过任何反对园丁的证据，所以我干脆假设园тельно是罪魁祸首。”作者证明了加入这个规则可以在不破坏任何安全保证的前提下提高游戏的效率。他们展示了即使有了这个额外的捷径，逻辑依然严丝合缝。

从理论到真正的（但简单的）机器人

在理论上证明了游戏规则完美运行之后，作者问道：“我们真的能制造出一个玩这个游戏的机器人吗？”他们创建了一个策略（strategy）——一套关于侦探下一步该选哪条规则的指令。他们在 Rocq 中构建了这个策略的具体版本，然后使用一种被称为**提取（extraction）**的魔法工具，将他们的数学证明转化为了一个用 OCaml 编写的真实计算机程序。

他们用一些简单的谜题测试了这个新机器人。它成功了！它正确地解决了问题，包括一个名为 zebra.cnf 的谜题，其中包含 155 个变量和 1,135 个子句。然而，作者对机器人的局限性非常坦诚。它就像一辆概念性的玩具车：它行驶完美，证明了引擎有效，但它还不是 F1 赛车。它运行缓慢，因为它使用简单的列表来记录线索，而现实世界的赛车则使用高速内存。作者承认这个版本还没准备好去击败当今企业使用的工业级选手，但它是一个经过验证的核心（verified core）。它是一个微小、不可破坏的基础，未来可以在此之上构建更快、更智能的求解器。

这对未来意味着什么

这篇论文并不声称已经解决了如何制造世界上最快的 SAT 求解器的问题。相反，它声称构建了一个最安全的蓝图。通过在 Rocq 中证明抽象规则，他们创建了一个“受信任的核心”。未来的研究人员现在可以拿着这个蓝图，并添加现代求解器的各种高级功能——比如“从错误中学习”（子句学习）或“跳跃式回溯”（非典型回溯）——并确信其底层逻辑依然稳固。

简而言之，Dijkstra 和 Ahrens 不仅仅是造了一辆更好的车；他们造了一辆永远不会撞车的汽车蓝图，证明了轮子背后的逻辑在数学上是完美的。这是一个经过验证的小步，为未来更庞大、更复杂且值得信赖的逻辑机器铺平了道路。