冲突驱动子句学习

DPLL 只记得“这条路失败”，CDCL 试图回答“哪些较早选择共同造成失败”。冲突子句是终点，reason clauses 是可追溯的因果边；把当前层的中间后果逐个消去后，剩下的学习子句直接描述一组不能再次同时成立的边界条件。回跳由这条子句的层级结构决定，而不是固定退回一层。

学习的价值在复用。一个冲突可能发生在很深的位置，但导出的子句可在另一条搜索路径上提前传播。它把原本树形重复的局部证明保存成 DAG 中可共享的引理。子句越短不必越好：推导成本、传播频率、活动决策层数和数据库占用共同影响效益，而逻辑有效性只是不可让步的底线。

考虑子句

决策 $p=1@1$ 传播 $q=1@1$；决策 $r=1@2$ 只满足 $C_2$；决策 $a=1@3$ 依次传播 $b,c,d,e,f$，最后 $C_8$ 冲突。对应的CDCL 蕴含图公理库CDCL 蕴含图CDCL implication graph · Conflict implication graph把一次 CDCL trail 中的决策、传播原因和冲突表示成按时间有向的无环依赖图。显示 $d$ 是离冲突最近的当前层必经点。采用First-UIP 学习公理库First-UIP 子句学习First-UIP clause learning · First unique implication point · 1-UIP learning在冲突图中选取离冲突最近的唯一蕴含点，归结得到 asserting clause 并确定回跳层。，先以 $e$ 归结 $C_8,C_6$ 得

再与 $C_7$ 以 $f$ 归结，得到

$L$ 中 $d$ 在层 3，$q$ 在层 1，所以回跳到层 1，越过无关的层 2；此时 $q=1$，$L$ 立即传播 $d=0$。每一步都能用两个父子句复算，学习结果不是从图形直觉猜出的剪枝条件。

边界之一是预处理和理论推理。若 reason 来自变量消去、异或模块或 SMT theory lemma，最终证书必须包含相应可检查依据；“求解器内部说它有效”不能替代蕴涵证明。子句删除不会损害可靠性，因为删除已学引理只减弱数据库，但可能破坏某个依赖保留全部学习信息的终止论证。

高性能实现常用双监视文字公理库双监视文字Two-watched-literals scheme · Two literal watching · Watched literals每个非单位子句监视两个文字，只在监视文字变假时扫描并维护单位传播状态。维护传播队列，用VSIDS公理库VSIDS 分支启发式VSIDS branching heuristic · Variable state independent decaying sum · VSIDS按近期冲突中变量的指数衰减活动度选择 CDCL 决策变量的分支启发式。选择下一决策变量，并按SAT 重启策略公理库SAT 求解器重启策略SAT solver restart strategy · Restart policy in SAT solvers · SAT restarts在保留有效学习信息的同时周期性撤销非根决策，以重新组织 CDCL 搜索的策略。周期性清空非根 trail。这三者分别改变索引、搜索顺序和搜索阶段，不参与学习子句可靠性的证明；换掉其中任何一个，CDCL 的逻辑内核仍可成立。

CDCL 是增量验证的重要后端。assumption literals 允许多次查询共享一份子句数据库，同时把某次查询的临时前提限制在可撤销层；unsat core 可从依赖这些 assumptions 的冲突证明中提取。共享必须遵守作用域：含已撤销局部定义的子句若未正确提升，可能污染下一次查询。证明日志与独立 checker 把“学习均有效”的巨大信任面压缩成逐步验证。