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 }q\vee \mathrm{\neg }d$。逐步归结可核验这条边界确实阻断所有到冲突的路径。

“蕴含图”一名也用于 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，独立检查器就能重放同一消去过程。