布尔可满足性求解器深度工程：从 DPLL 到 CDCL 的两观察文字传播、1UIP 学习与重启策略全链路实战

布尔可满足性求解器深度工程：从 DPLL 到 CDCL 的两观察文字传播、1UIP 学习与重启策略全链路实战

执行摘要：SAT 是第一个被证明的 NP-Complete 问题，理论上"不可能"高效求解；但现实中的现代 CDCL 求解器能在分钟级解掉百万变量、千万子句的工业实例。这个反差不是理论失效，而是三十年的工程积累：两观察文字（2-watched literals） 让单元传播变成近乎 O(1) 摊还操作且支持 O(1) 回溯撤销；冲突驱动子句学习（CDCL） 把失败转化为知识，配合 非时序回溯 直接跳回冲突真正相关的决策层；VSIDS 启发式 + Luby/Glucose 重启 + LBD 子句数据库缩减 三者共同对抗"重尾"（heavy-tail）现象。本文拆开这四层机制，附可运行的传播与 1UIP 学习代码，并说明它在 EDA 形式验证、依赖求解与符号推理中的真实用法。

一、为什么 NP-Complete 还能被"解掉"

先建立正确的心智模型。CNF 公式的可满足性判定在最坏情况下是指数级的，但工业实例不是随机 3-SAT 的相变点配方，而是带有强结构的：大量子句是局部约束、变量呈现社区结构、存在大量可消去的辅助变量。

这带来一个关键洞察：求解器的瓶颈从来不是"搜索空间太大"，而是"不知道该剪哪里"。DPLL 笨在它只会在赋值冲突时回退一层，而这一层往往与冲突毫无关系——它可能退掉一个在另一个无关子问题里的决定，然后在下游重走一遍同样的死路。CDCL 的全部工程，本质上是把"我刚才为什么失败"这件事编码成一个新的子句永久记住。

一个直观的数字：对同一个 EDA 等价性检查实例，纯 DPLL 可能需要 10^9 次决策；加上子句学习后降到 10^5 量级；再加上重启与子句缩减，降到 10^4 量级。每一层都是数量级的差别。

二、DPLL 与它的两个致命弱点

DPLL 的骨架只有两步：决策（选一个未赋值变量，猜一个相位）与 单元传播（unit propagation，反复找出只剩一个未赋值文字的子句，强制该文字为真）。

def dpll(assign, clauses):
    assign, clauses = unit_propagate(assign, clauses)
    if has_empty_clause(clauses):
        return False          # 出现空子句 = 冲突
    if all_vars_assigned(assign):
        return True
    v = pick_var(assign)      # 决策
    for phase in (True, False):
        if dpll({**assign, v: phase}, clauses):
            return True
    return False

两个弱点：

1. 时序回溯（chronological backtracking）：冲突发生在决策层 40，但它只回退到层 39，而冲突的真正原因可能在层 12。于是层 39..13 的所有分支被白白重搜一遍。
2. 不记录失败原因：同一个冲突模式会在搜索树的其他分支重复出现成千上万次。

CDCL 对第一点的回答是 非时序回溯（backjumping），对第二点的回答是 子句学习。

三、两观察文字：让传播与撤销都是 O(1)

朴素单元传播每赋值一个变量就要扫描所有含该文字的子句，代价与子句总数成正比——在千万子句规模下不可接受。2-watched literals 的洞察是：一个子句只有在它"倒数第二个"未假文字被赋值时，才可能变成单元子句或冲突子句。因此每个子句只需盯住两个尚未被判假的文字。

class Watcher:
    __slots__ = ('clause', 'blocker')   # blocker 缓存另一个观察文字，避免解引用

def propagate(trail, watches, value):
    """value: 变量 -> True/False/None；返回冲突子句或 None"""
    qi = 0
    while qi < len(trail):
        lit = trail[qi]; qi += 1
        wl = watches[~lit]          # 被判假的文字的观察列表
        watches[~lit] = []
        for w in wl:
            c = w.clause
            # 快速路径：blocker 仍为真，子句不可能成为单元子句
            if value[var(w.blocker)] == sign(w.blocker):
                watches[~lit].append(w)
                continue
            if c[0] == ~lit: c[0], c[1] = c[1], c[0]
            if value[var(c[0])] == sign(c[0]):      # 另一个观察文字已真
                watches[~lit].append(Watcher(c, c[0]))
                continue
            found = None
            for k in range(2, len(c)):              # 寻找新的观察文字
                if value[var(c[k])] != ~sign(c[k]):
                    found = k; break
            if found is None:
                watches[~lit].append(w)
                if value[var(c[1])] == ~sign(c[1]):
                    return c                        # 冲突
                enqueue(trail, value, c[1], c)      # 单元子句
            else:
                c[1], c[found] = c[found], c[1]
                watches[~c[1]].append(Watcher(c, c[0]))
    return None

三个工程要点常被忽略：

• 观察列表按假文字索引，撤销时什么都不用做。回溯只需弹出 trail 上的赋值，观察列表保持有效——这是"惰性"数据结构在求解器里最漂亮的一次应用。
• blocker 缓存是纯粹的性能 hack，却能把传播时间砍掉 20%~30%，因为它避免了一次随机内存访问。在 SAT 求解器里，cache miss 才是真正的敌人，不是浮点运算。
• 观察列表用 数组而非链表 存储，遍历时的局部性远好于指针追逐。

四、冲突分析：把失败编译成一个子句

传播返回冲突子句后，CDCL 不急着回溯，而是构造 蕴含图（implication graph）：节点是赋值，边是导致该赋值的子句。冲突节点有两个入边对应同一个变量的正反文字。

从冲突子句出发，反复用"蕴含它的那个子句"去消解（resolve）掉当前决策层的变量，直到子句只剩一个当前层的文字——这个文字就是 唯一蕴含点（Unique Implication Point, UIP）。第一个找到的 UIP 称为 1UIP，实践中最有效。

def analyze(conflict, trail, reason, level):
    """返回 (学习子句, 回溯目标层)"""
    learnt = set(conflict)
    seen = set()
    btlevel = 0
    i = len(trail) - 1
    counter = 0
    while True:
        while True:                      # 找到 trail 上最近的未处理文字
            l = trail[i]; i -= 1
            if var(l) not in seen and level[var(l)] > 0:
                break
        seen.add(var(l))
        if level[var(l)] >= level[var(trail[-1])]:
            counter += 1
        else:
            learnt.add(l)
            btlevel = max(btlevel, level[var(l)])
        # 统计 learnt 中处于当前层的文字数；减到 1 即到达 1UIP
        cur_cnt = sum(1 for x in learnt if level[var(x)] == level[var(trail[-1])])
        if cur_cnt + counter <= 1:
            break
        r = reason[var(l)]
        for x in r:
            if x != l and var(x) not in seen:
                learnt.add(x)
        # 消解：去掉 l 与 ~l
        learnt = {x for x in learnt if var(x) != var(l)}
    learnt.add(~trail[-1])
    return list(learnt), btlevel

学习子句的语义是 "这个组合不要再试了"，它被永久加入子句库，同时 btlevel 直接把搜索跳回真正相关的决策层——这就是 backjumping。注意回溯目标层可能比当前层小很多，跳过的分支从此不再访问。

一个容易被低估的细节：学习子句的第一个文字必须是 UIP 文字，第二个文字应是回溯层中最近被赋值的变量。这个排序规则让新子句在下一次传播中立刻能作为 watch 结构生效，而不是退化成一条"死"子句。

五、重启：对抗重尾分布的唯一手段

SAT 求解的运行时间分布是 重尾 的：同一个求解器在同一个实例上，换一个随机种子，可能 3 秒解出，也可能 3 小时解不出。这不是玄学，而是启发式在早期做出了糟糕的决策，把搜索引向了错误区域，而子句学习又不断强化这个错误方向。

重启解决这个问题，但重启本身不带代价的前提是学到的一切都保留下来——子句库、VSIDS 活动度、相位保存都在，丢掉的只是那条错误的决策路径。

LBD（Literal Block Distance） 是 Glucose 引入的核心指标：学习子句中不同决策层的数量。LBD 小意味着这条子句把少量"概念层"的变量绑在一起，是通用性强的好子句（glue clause）；LBD 大通常意味着它只是某条具体路径的偶然产物。子句数据库缩减时优先保留 LBD ≤ 3 的子句，可以长期保留（"永不过期"子句），其余按活动度几何衰减淘汰。

六、VSIDS 与相位保存

VSIDS（Variable State Independent Decaying Sum）：每个变量维护一个活动度分数，冲突时参与冲突分析的变量加分，所有分数周期性乘以衰减因子（如 0.95）。这让"最近频繁卷入冲突"的变量优先被决策——把搜索压力自动导向瓶颈区域。

EVSIDS（指数 VSIDS）用对数域实现，把每次乘法变成一次加法，避免浮点下溢。

相位保存（phase saving）：变量赋值被撤销时记住它最后的相位，下次决策优先采用该相位。这个看似微不足道的技巧，在多数实例上能带来 2 倍以上的加速，因为它保留了"上一次在这个子空间里哪个方向更可能成功"的局部记忆。

七、在processing：vivification 与子句消去

现代求解器的求解循环里还穿插着化简：

• 子句包含（subsumption）：若子句 A 的 literals 是 B 的超集，B 冗余，可删 A。
• 有界变量消去（BVE）：对变量 x，把所有含 x 和 ~x 的子句两两消解；若消解后子句总数不增加，就消去 x。这是 Davis-Putnam 的消去法在现代求解器中的复活版本。
• 阻塞子句消去（BCE）：若子句 C 含文字 l，且所有含 ~l 的子句与 C 消解的结果都是重言式，则 C 是阻塞子句，可直接删除——它不影响可满足性。
• Vivification：对子句 C，临时假设 C 中文字全为假，跑一次传播；若某文字被蕴含为假，说明它可从 C 中删去（子句被"强化"）。这是最有效的在processing 技术之一，通常能缩短 10%~30% 的子句。

def vivify(clause, solver):
    """返回强化后的子句，或 None 表示子句已恒真"""
    assume = [~l for l in clause]
    out = []
    for i, l in enumerate(clause):
        if solver.propagate_under(assume[:i] + assume[i+1:]) == CONFLICT:
            pass                      # l 在此假设下被蕴含为假 -> 可从子句中移除
        else:
            out.append(l)
    return out

八、可信性：DRAT 证明检查

求解器说 UNSAT，凭什么信？现代求解器会输出 DRAT（Deletion Resolution Asymmetric Tautology） 证明轨迹：一系列子句添加/删除操作，每步都可被独立检查器以多项式代价验证。SAT 竞赛自 2013 年起强制要求 UNSAT 结果附带 DRAT 证明。

这在工程上的意义被严重低估：形式验证的结论如果不可独立复现，就没有价值。DRAT 让求解器变成一个"证明生成器"而非"神谕"，检查器代码量只有几千行，可以形式化验证（已有用 ACL2/Coq 验证的检查器实现）。

九、生产落地：从 EDA 到依赖求解

• EDA 形式验证：等价性检查（EC）、属性检查（model checking 的有界部分）、ATPG 测试向量生成，全部归约为 SAT。工业界最大的实例来自这里，也是所有核心启发式的来源。
• SAT Sweeping：电路综合中用 SAT 判定两个节点是否功能等价，从而合并冗余逻辑。它在 AIG（And-Inverter Graph）上迭代运行，是逻辑综合里最强的化简手段之一。
• 包管理器依赖求解：Debian/apt、openSUSE 的求解器、以及不少语言的包管理器（如 Eclipse 的 p2）把版本约束编码成 SAT/Pseudo-Boolean 问题。这解释了为什么某些依赖错误提示像"逻辑证明"而不是"找不到包"。
• 调度与规划：作业车间调度、FPGA 布线、航线排班，通常编码成 SAT 或 SMT。
• 符号 AI 与神经符号：约束满足、程序合成、神经网络鲁棒性验证（把 ReLU 编码成子句）都在用 SAT 后端。

一个实用建议：不要手写 SAT 编码再自己写求解器。正确做法是先用 Tseitin 编码把问题转成 CNF（注意 Tseitin 编码保持公式大小线性增长，而 naive 的 CNF 转换可能指数爆炸），然后调用现成求解器：

from pysat.formula import CNF
from pysat.solvers import Cadical195

cnf = CNF()
cnf.append([1, -2])        # x1 or not x2
cnf.append([-1, 2, 3])

with Cadical195(bootstrap_with=cnf.clauses) as s:
    if s.solve():
        print('SAT', s.get_model())
    else:
        print('UNSAT')

生产选型的经验：CaDiCaL 和 Kissat 是当前通用 SAT 的第一梯队，前者代码可读性极高（学习 SAT 实现的最佳教材），后者是近年 SAT 竞赛的霸主。若你的约束里有基数约束（"恰好 k 个为真"），用 Pseudo-Boolean 或 Cardinality 编码而非朴素两两编码，子句数从 O(n²) 降到 O(n log n)。

十、结论

CDCL 求解器的设计取舍非常清晰，几乎每一处都是"用空间换确定性剪枝"：

• 2-watched literals：用惰性数据结构换取 O(1) 传播与 O(1) 撤销；
• 1UIP 学习 + 非时序回溯：用内存（子句库）换取搜索空间的永久剪除；
• VSIDS + 相位保存：用统计记忆换取决策质量；
• 重启 + LBD 缩减：用策略性放弃换取对重尾分布的免疫；
• DRAT：用可检查性换取结论的可信度。

真正值得带走的不是这些技巧本身，而是它们背后的范式：当一个搜索问题的失败是结构化的、可归因的，那么把失败编译成约束，永远比换一条路重走更划算。 这个思路同样适用于约束求解之外的领域——从分布式系统的一致性冲突消解，到编译器的反例制导抽象精化（CEGAR），内核都是同一件事。