CDCL 蕴含图

Trail 告诉我们“先后发生了什么”，蕴含图进一步说明“后一个赋值为什么不得不发生”。一个传播节点可能有多个父节点，因为只有若干前提同时为真时，reason clause 才只剩它一个出口。冲突节点则把一条被完全关闭的子句变成共同终点。

Cut 像在因果网络上截取边界。边界内的传播细节可以通过归结消去，边界外只保留足以再次触发同类冲突的条件。选择不同 cut 会得到不同学习子句；因此图不自动指定“最好”的学习结果，它只使候选结果与原始原因之间的证明路径可见。

沿一次 CDCL 轨迹，设 $p=1@1$ 由 $(\mathrm{\neg }p\vee q)$ 传播 $q=1@1$；$r=1@2$ 是与冲突无关的决策；$a=1@3$ 分别由 $(\mathrm{\neg }a\vee b)$、$(\mathrm{\neg }a\vee c)$ 传播 $b,c$，再由 $(\mathrm{\neg }b\vee \mathrm{\neg }c\vee d)$ 传播 $d$。子句

传播 $e,f$，而 $(\mathrm{\neg }e\vee \mathrm{\neg }f)$ 产生冲突。边集为

$r$ 在图中是没有通往冲突的孤立决策。把 $q,d$ 及其所有前驱留在 reason side、把 $e,f,\kappa$ 放到 conflict side，cut frontier 为 $\{q,d\}$。先将冲突子句 $\mathrm{\neg }e\vee \mathrm{\neg }f$ 与 $e$ 的 reason 归结，得到 $\mathrm{\neg }q\vee \mathrm{\neg }d\vee \mathrm{\neg }f$；再用 $f$ 的 reason 消去 $f$，得到 $\mathrm{\neg }q\vee \mathrm{\neg }d$。两次归结明确展示了学习子句的来源。

该子句中 $q$ 在层 1、$d$ 在层 3。回跳到层 1 后，$q$ 仍真而 $d$ 已撤销，学习子句立即传播 $\mathrm{\neg }d$；层 2 的 $r$ 与层 3 的其他赋值一起撤销。若误把学习子句写成 $q\vee d$，它在原冲突赋值下反而已经满足，既不能排除冲突，也没有上述归结证明。

若另外由 $(\mathrm{\neg }r\vee z)$ 传播 $z$，并把 $z$ 放到 conflict side，完整前沿就增加了 $r$，但 $z$ 没有通往冲突的路径。前面的两次归结仍只得到 $\mathrm{\neg }q\vee \mathrm{\neg }d$；要写成 $\mathrm{\neg }q\vee \mathrm{\neg }d\vee \mathrm{\neg }r$，须补弱化。这条更长子句是可靠的，却保留了无关条件，通常不如原子句有用。

“蕴含图”一名也用于 2-SAT 中由每个二元子句静态建立的图；那张图的顶点是正负文字、边表达材料蕴含，并用于强连通分量判定。这里的图只描述一次动态 trail，含决策层、reason 和冲突节点，二者不能共享未限定的结论。理论传播还可能引入来自理论解释的超边式原因，必须先将解释写成有效子句再接入此图。

CDCL公理库冲突驱动子句学习Conflict-driven clause learning · CDCL · Clause-learning SAT solving从传播冲突中推导原公式蕴涵的新子句，并据此非时序回跳和继续搜索的 SAT 算法。用蕴含图定位非时序依赖：若冲突只依赖层 1 与层 3 的前沿，层 2 决策就不应阻止算法直接回到层 1。图也支持可视化诊断，显示哪些原子句和传播链真正参与了失败，而不是把整条 trail 都误报为核心。

唯一蕴含点是 cut 的一种结构化选择。First-UIP 让学习子句恰含一个当前层文字，从而在回跳后立即传播；其他 cut 仍可可靠，却可能不具 asserting 性。归结证书可记录父子句与 pivot，而无须保存整张图；如果最终子句还用了弱化，证书和检查器也必须支持并记录这一步。