一周协作，完成 CDCL 求解器的形式化验证

SAT，即布尔可满足性问题，研究的是：对于一个由布尔变量和逻辑运算组成的公式，是否存在一组变量取值，使整个公式成立？SAT 求解器用于回答这个问题。它可以报告 SAT，表示找到了满足公式的赋值；报告 UNSAT，表示不存在这样的赋值；也可能因为时间或资源限制，报告 UNKNOWN，表示尚未得出结论。

但我们如何确认求解器给出的答案是正确的？对于 SAT，可以把返回的赋值代入公式，检查它是否确实满足所有约束。对于 UNSAT，检查则更复杂：没有找到解，并不意味着解不存在。因此，一些现代 SAT 求解器会在报告 UNSAT 时，同时生成一份不可满足性证明，交由独立的检查器验证这次求解的结论。

那么，能否直接证明求解器的算法及其实现是正确的，使结果的正确性不必依赖每次运行另行生成的证明？也就是说，对于满足输入条件的公式，只要求解器给出 SAT 或 UNSAT 的判断，这个判断就一定成立。

QCP 团队围绕这一目标，与 GPT 5.6 sol、Opus 4.8 协作，在一周内完成了一个 C 语言 CDCL SAT 求解器的功能正确性验证。借助 QCP 和 Rocq，团队为这份具体实现建立了可由定理证明器检查的证明：在输入满足规约的前提下，求解器若报告 SAT，其给出的赋值就满足原始公式；若报告 UNSAT，原始公式就确实不存在满足赋值。

这项工作的代码、标注和证明已收录于 QCP 2.1.0。它也记录了一次人与 AI 共同完成程序验证的实践：围绕同一份实现，将正确性要求逐步落实为可以检查的证明。

CDCL 算法

CDCL（Conflict-Driven Clause Learning，冲突驱动的子句学习）是求解 SAT 问题的经典算法，也是许多现代 SAT 求解器的基础。它在搜索变量赋值的过程中，通过分析冲突生成新的子句，以避免再次进入已经排除的搜索分支。

CDCL 通常处理合取范式（CNF）公式。一个 CNF 公式是若干子句的合取，每个子句又是若干文字的析取；文字是一个布尔变量或它的否定。含有 m 个子句的公式可以写成：

要求整个公式为真，就要求每个子句中至少有一个文字为真。求解器从尚未赋值的状态出发，交替进行决策和单位传播。决策是选取一个尚未赋值的变量，尝试为它指定真值；单位传播则处理只剩一个文字尚未赋值、其余文字都为假的子句。要使这个子句成立，剩下的文字必须为真，因此可以直接推出它的取值。传播反复进行，直到没有这样的子句，或者某个子句的所有文字都变为假，产生冲突。

考虑下面的公式：

如果决策令 x 为假，第一个子句就要求 y 为真，而第二个子句要求 y 为假，两者发生冲突。这说明当前决策无法扩展为公式的一个解。CDCL 会进一步分析冲突的原因，从已有子句中推导出一个学习子句。在这个例子中，对两个子句中的 y 做归结，就得到单文字子句 x：

更一般地，归结规则允许从两个分别含有 p 和 ¬p 的子句推出一个新子句。下面的 A、B 表示其余文字的析取：

冲突分析沿着单位传播的原因反复使用这一规则。得到的学习子句是原始公式的逻辑推论，因此加入它不会排除原始公式的任何解。若用 L 表示学习子句，这一性质可以写为：

学习之后，求解器撤销一部分赋值，回到较早的决策层级，再利用学习子句继续传播。这个过程称为回跳：目标层级由学习子句决定，可以跳过多个决策层级，而不必逐层回退。在上面的例子中，求解器撤销 x 为假的决策，并在没有决策的第 0 层由学习子句推出 x 为真。之后无论 y 取何值，两个原始子句都成立。

整个算法重复决策、传播、冲突分析、学习和回跳。如果得到满足所有子句的赋值，就返回 SAT；如果在第 0 层发生冲突，就可以判定公式为 UNSAT。关于 CDCL 的算法背景，可参阅 Marques-Silva、Lynce 和 Malik 的 Conflict-Driven Clause Learning SAT Solvers。

我们验证了什么

本次验证的对象是一个 C 语言 CDCL 实现，包括决策、单位传播、冲突分析、子句学习和回跳等过程。cdcl_solver 是这个实现的主要函数入口，负责组织这些过程并返回求解结果。

我们通过入口函数 cdcl_solver 的 specification（规约）说明这个实现的整体正确性要求：只要调用前满足规约中的输入条件，求解器返回时就一定满足相应的输出条件。 其中，Require 描述输入公式和初始程序状态，Ensure 描述求解结果及返回时的程序状态。对各个求解过程的验证共同支持这一入口规约。

下面摘录规约的主要结构，省略辅助参数；其中的省略号仅用于展示，完整规约见本节末尾。

int cdcl_solver(sat_data* s) /*@
  With (F : cnf) ...
  Require cnf_wf(n, F) && solver_input_core(s, F, ...)
  Ensure
    (exists J, __return == 1 && models(J, F) &&
      solver_sat_arm_core(s, F, ..., J)) ||
    (__return == 0 && cnf_unsat(n, F) &&
      solver_unsat_arm_core(s, F, ...)) ||
    (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, ...))
*/

输入需要满足什么条件

F 是规约中表示原始输入公式的逻辑变量，n 是变量个数。cnf_wf(n, F) 要求公式中的变量编号都在 0 到 n - 1 的范围内。solver_input_core 则把这个逻辑公式与 s 指向的 C 数据结构联系起来。它要求：

• 子句表正确存储原始公式 F，初始时还没有学习子句；原始公式中的每个子句都非空。
• 所有变量都尚未赋值，对应的赋值、原因和决策层级数组处于规约规定的初始状态。
• 结构体和数组满足规约的内存要求，子句状态及计数与实际内容一致；变量个数满足 0 ≤ n < INT_MAX，已有子句数不超过子句表容量。

这些都是调用者需要满足的前置条件。这条入口规约以已经构造好的求解器状态为起点；输入文件的解析和初始状态的构造，需要在调用入口之前满足上述条件。

返回 SAT 时保证什么

__return 表示函数返回值。第一个分支规定，返回 1 时，存在赋值 J，使 models(J, F) 成立，也就是 J 满足原始公式的每个子句：

solver_sat_arm_core(..., J) 进一步要求，这个 J 与返回时 C 程序的赋值数组所表示的赋值相同。因此，验证结论既包括“公式有解”，也包括“程序实际保存的赋值就是一个解”。这里的 F 始终是调用前的原始公式，即使求解过程中加入了学习子句，最终也必须满足原始公式。

返回 UNSAT 时保证什么

第二个分支规定，返回 0 时，cnf_unsat(n, F) 成立，即不存在对这 n 个变量的赋值能够满足原始公式：

这个结论排除了所有可能的赋值，而不仅是当前搜索尝试过的赋值。证明必须说明，程序执行到这个返回分支时，确实足以推出原始公式无解。用户不需要再检查本次运行生成的 UNSAT 证明，才能得到这条规约所保证的结论。

容量耗尽与证明的范围

第三个分支对应返回 -2：子句表容量已经耗尽，无法继续加入学习子句。规约在这个分支中保留了对数据结构和所占内存的描述，但不给出 SAT 或 UNSAT 判断。它对应引言中“尚未得出结论”的情况，不能当作公式无解。

三个输出分支还分别描述返回时的内存状态。例如，SAT 分支保留公式的存储关系，并将赋值数组与 J 对应起来；UNSAT 分支保留相应的数组内存，但不承诺其中保存了满足赋值。证明因此需要覆盖实现中的状态更新，不能仅凭抽象算法的正确性得出结论。

这份规约证明的是部分功能正确性：前置条件成立时，函数若返回，结果就满足上述三个分支之一。本次工作没有证明函数一定终止，也没有保证它一定能在子句表容量耗尽之前给出 SAT 或 UNSAT 判断。

int cdcl_solver(sat_data* s )/*@ With (F : cnf) original_count (snap : dense_snapshot)
      (ranks : Z -> option nat) values reasons levels states true_counts unassigned
      row_table n live cap
    Require cnf_wf(n, F) &&
    solver_input_core(s, F, original_count, snap, ranks,
      values, reasons, levels, states, true_counts, unassigned, row_table, n, live, cap)
    Ensure
      (exists J, __return == 1 &&
      models(J, F) &&
        solver_sat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap, J)) ||
      (__return == 0 &&
      cnf_unsat(n, F) &&
        solver_unsat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap)) ||
      (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, original_count,
        snap, ranks, values, reasons, levels, states, true_counts, unassigned,
        row_table, n, live, cap))
*/

验证结果

首次完成验证时，这个求解器包含 362 行 C 代码，配有 2,275 行标注和 14,977 行证明库。QCP 共生成 1,037 个验证条件，其中 253 个通过补充证明完成，对应的 Manual .v 文件共 11,675 行。

完整的 C 实现、QCP 标注和 Rocq 证明已随 QCP 2.1.0 公开，可通过文首链接查看。