冲突学习与回跳（为什么必须记录坍缩）
当 agent 沿一个子树往下走、撞上死路、再往回追溯时，需要两个机制——它们正是 CDCL（冲突驱动子句学习，Conflict-Driven Clause Learning）的两大支柱，也是现代 SAT/CSP 求解器的引擎。
① 非按时间顺序的回跳（回溯可以落在另一个子树里）
遇到冲突（某个域被清空）时，不要撤销最近的那一步。而应：
- 分析蕴含图（implication graph，哪些决策 + 传播共同产生了这个冲突）→ 算出冲突集（真正应负责的那些决策变量）；
- 回跳到冲突集中最近的那个决策——它可能位于另一个子树。
- 为什么会跨子树：约束本身是跨子树的（子树间相互影响），所以冲突集可以包含其他子树的决策。回跳目标是由冲突算出来的，不是由树结构决定的。
② no-good / 冲突子句学习（"坍缩信息"）
从这次冲突推导出一条 no-good——¬(x₁=a ∧ x₅=b ∧ x₉=c)——并把它永久加入 C。 传播过程再也不会重新进入那个组合：你已经记下了哪些世界已经坍缩了。
为什么"否则就无法收敛"是完全正确的：
没有学习机制时，搜索会反复推导出同样的冲突（thrashing，抖动），在等价的死分支间打转 → 没有单调进展 → 在困难实例上爆炸 / 不收敛。 有了学习机制，no-good 存储会单调增长：每一次冲突都教会系统一些永久性的东西，绝不重复。
关键的化解（化解了之前"单调 vs. 修正"的张力）：
赋值会回溯（非单调），但知识（学到的坍缩信息）是单调的。收敛来自知识的单调性，而不是赋值的单调性。有限域 → no-good 空间有限 → 学习终将停止 → CDCL 收敛；无限域 → 由
P×C界定。
它把"可推导 ≠ 已知"操作化了
deducible-not-known：约束蕴含着答案，但推导出所有蕴含是 NP-hard 的——你无法算出完整的闭包。CDCL 就是可操作的答案：
子句学习 = 惰性的、由冲突驱动的蕴含推导。 你不去计算整个闭包；你只在搜索恰好绊倒的那一点，推导出一条被蕴含的 no-good，记下它，继续前进。
P×C决定你推导出多少条。 于是"可推导但未推导"这道缺口，就被你学到的这些 no-good 惰性地填上了。
它同时也是防止漂移的溯源记录
no-good 存储 = 坍缩历史 = 溯源记录（round-tree-flight-recorder）。没有它 → 你会重新走一遍已经坍缩过的世界，也就是 drift-is-world-wandering 所说的"世界游荡"。"记录坍缩，否则无法收敛" = "保留溯源，否则会漂移"——是同一件事。
一句话
死路 → 分析冲突 → 回跳到真正的元凶（可能在另一个子树里）+ 把一条 no-good 学进 C。赋值以非单调方式回溯，但学到的坍缩信息单调增长——这正是收敛得以保证的原因；它同时也是 deducible≠known 的惰性解法，以及防止漂移的溯源记录。