从 CDCL 到 MCTS：非确定性与无限分支
经典的 SAT/CSP 框架（csp-formalization、conflict-learning-and-backjumping）假设有限、确定性、可靠（sound）三条同时成立。agent harness 把这三条全部打破，这就把算法推入了一个不同的范式（regime）。
保留的与打破的
- 保留的（结构）： worlds 对应 configurations，collapse 对应 pruning，收敛对应收窄到
P×C残差，记录 collapse 信息对应 provenance，backjump 到真正的元凶。 - 打破的（保证）： CDCL 的收敛性建立在有限、确定性、可靠三者之上；agent 把这三条全部违反了。
差异一——非确定性 ⇒ 一个不可靠的 theory solver ⇒ no-good 可能是假的
经典的传播（propagation）/冲突检测是确定性且可靠的（学到的 no-good 永远为真）。LLM 对不兼容性的判断则是随机的，并且可能出错：
- 假冲突（false conflict）→ 一个错误的 no-good → 永久剪掉一个好的 world；漏检的冲突 → 走入一个死 world。
- 比 deducible-not-known（不完备）更糟：这是不可靠的（断言了错误的蕴含关系）。
- → "知识单调增长"这条收敛保证被打破——学到一个错误的 no-good，在真值意义上是非单调的（你删掉了一个真实解）。
修复： no-good 不能是硬性的、永久性的子句（clause）。把它们变成软性的／加权的／可修正的：先验证再固化（commit）（多次采样／对抗式复核后再固化）；对不确定的不兼容关系降权，而不是直接消除。范式（regime）从硬 CSP 滑向加权 CSP／Max-SAT／概率推断（信念传播，belief propagation）——collapse 变成一次信念更新（belief update），而不是硬性删除。
差异二——（实质上）无限分支 ⇒ 采样而非枚举 ⇒ MCTS，而非 DFS/BFS
经典的 DFS/BFS/CDCL 在一个有限的定义域上枚举子节点。agent 的定义域是无限的（"标题该怎么写"）：
- 只能采样少量候选（LLM 作为 policy），再加一个价值估计（value estimate）来判断哪个更有希望；
- 在一棵被采样、被随机评估的树上搜索＝蒙特卡洛树搜索（Monte Carlo Tree Search）：select（UCT ＝ value ＋ exploration bonus）→ expand → evaluate → backprop。（AlphaGo/AlphaProof。）
- 完备性没有了： 无限分支加采样意味着你无法证明 UNSAT（无法枚举所有 world）→ 你只能satisfice（满足即止），停在
P×C。
形式化归宿的转移：SAT/CSP → MCTS + 软约束
| 经典 CDCL | agent harness | |
|---|---|---|
| 分支 | 有限，枚举 | 无限，采样（LLM＝policy） |
| 传播／冲突 | 确定性，可靠 | 随机，不可靠 |
| no-good | 硬子句，永久 | 软性／加权／可修正的信念 |
| 搜索 | DFS ＋ 学习 ＋ backjump | MCTS（价值引导 ＋ 探索/利用） |
| 终止 | 完备（可证明 UNSAT） | 仅satisfice 到 P×C |
这正是LLM ＋ 树搜索这个前沿方向：Tree of Thoughts、LATS（Language Agent Tree Search）、AlphaProof 那种由 MCTS 引导的推理。
一句话
结构（worlds／collapse／provenance／backjump）继承自 CSP；但非确定性（no-good 可能为假 → 把它们软化为加权的、可修正的信念）和无限分支（无法枚举 → 只能采样 → 用 MCTS，而非 DFS/BFS；没有完备性，只有 satisfice）把算法从 CDCL 推向了"LLM 同时充当 policy 与 value 的 MCTS ＋ 软约束 ＋ P×C satisficing"。