First-UIP 子句学习

冲突附近可能有多条传播支路，First-UIP 寻找这些支路汇合后、尚未抵达冲突的最后一道闸门。把闸门之后的具体传播全部归结消去，学习子句只保留闸门和较早层条件。于是回跳后，较早条件会立刻把这道闸门推向避免冲突的一侧，而不是重新走完原来的长链。

按 trail 逆序归结是一种无需显式枚举所有 cut 的实现。最近赋值的当前层文字必然是已经发生的传播节点；用其 reason 替换它，相当于把 cut 向前推过该节点。当前层文字数降到一时，cut 正好停在 first UIP 前沿。

设冲突层为 3，较早层已有 $q=1@1$，当前层传播了 $d,e,f$。三个相关子句为

$C_8$ 含两个层 3 文字的否定。先用 $e$ 的 reason $C_6$ 归结：

它仍含层 3 的 $d,f$；再用 $f$ 的 reason $C_7$：

现在仅 $d$ 属于冲突层，first UIP 是 $d$。其余文字只涉及层 1 的 $q$，故从层 3 回跳到层 1，并在 $q=1$ 下传播 $d=0$。若误回到层 2，子句同样会传播，却保留了无关决策；若回到层 0，虽然仍可靠，却丢掉了本可保留的搜索上下文。

First-UIP 不是可靠性的来源：可靠性来自每次归结的父子句有效。它也不保证 learned clause 在文字数、蕴涵强度或未来运行时间上全局最优。若 reason 含理论 lemma，归结仍可使用，但该 lemma 本身必须带可靠理论解释。多个传播顺序还可能产生不同 implication graph 和不同 First-UIP 子句。

First-UIP 子句天然支持非时序回跳，并常具有较少的 decision-level blocks，因此成为现代 SAT 求解器的主流冲突分析方案。LBD 等指标统计子句跨越的决策层数，用于数据库保留或 restart 判断；它们是对未来用途的启发式预测，不改变 asserting clause 的证明。

从证明复杂度看，每份学习记录都可展开成一段归结推导；保留 learned clause 让后续冲突共享这段证明。若最终需要可认证 UNSAT，求解器可输出 resolution-like、DRAT 或 LRAT 日志，使 checker 不必重建当时的 UIP 图，只验证子句加入与删除步骤是否合法。