Harness 就是 DPLL(T)：LLM 是一个可能出错的理论求解器

父节点：recursive-harness

背景：SMT 如何把语义接入 SAT（DPLL(T)）

SMT = SAT + 理论（算术、数组，……）：处理的是像 x+y<5 这样的原子，而不只是布尔变量。架构是：

• SAT 核心（CDCL）处理布尔骨架，把每个理论原子当作一个不透明的布尔变量；
• 一个独立的理论求解器检查当前为真的那些理论原子在该理论内是否一致；
• 循环：SAT 核心提出一个布尔模型 → 理论求解器检查 T-一致性 → 如果不一致，它返回一个小的解释（一个很小的冲突子集，例如 x>3 ∧ x<2）→ 反馈回去作为一条学到的子句 → CDCL 回跳。此外还有理论传播（理论可以强制某些原子取值）。
• 要求： 理论求解器必须给出一个小的冲突/解释，否则 SAT 核心学不到有用的 no-good。

这个映射

LLM 判断的语义约束 = 一个"理论"；LLM = 理论求解器。于是这个递归 harness（csp-formalization）就是 DPLL(T)——只不过这个理论求解器是可能出错的、启发式的，不是一个精确的判定过程。

由此直接得出的两个推论

1. 一个设计要求（不是可选项）：LLM 必须对它给出的不兼容判断作出解释。 要拿到 CDCL 的好处（学习 + 回跳，见 conflict-learning-and-backjumping），一条"这两个方法不兼容"的判断，必须附带一个理由 / 一小组要负责的原子——也就是一个理论解释。一个光秃秃的是/否判断，会迫使你把整条路径都当作 no-good 学下来 → 剪枝几乎为零 → 退回到反复试错 → 不收敛。所以"LLM 必须说明一个世界为什么崩溃"这一点，是从 DPLL(T) 这个映射直接推出来的，不是锦上添花。
2. 这是一个理论求解器可能出错的 DPLL(T)。 真正的理论求解器是可靠且完备的判定过程；而 LLM 会误判（漏判或凭空造出不兼容）。这正是 deducible-not-known（LLM 是应对不可解演绎问题的一种启发式手段），也正是为什么语义约束的蕴含图是近似的——它是用 LLM 给出的、可能有错的理由搭建起来的。

再看一遍——放到理论层之下

• "可能出错"现在有了一个明确的代价：求解器每次调用的误差就是 inexact-contraction 里的 ε——只有当外层循环在收缩时，这个误差才是可以容忍的，其永久性下限是 ε/(1−k)。有收缩时，可能出错是安全的；没有收缩时，它是致命的。
• "必须解释"和"检查要产生梯度"是同一个原则的两面（见 coupling-to-the-learner）：gate 必须给求解器一个可读的梯度，求解器也必须给协调者一个小的解释——两者存在的理由相同：让冲突分析保持廉价且局部化。
• SAT 核心的位置现在也定下来了：它就是 coordinator-not-arbiter 的机械内核——no-good/割集存储、来源图、账本——永远不是一个 LLM。

一句话

机械约束 → 精确传播（真正的 CDCL）。语义约束 → LLM 作为一个可能出错的理论求解器（DPLL(T)）。无论哪一种，冲突解释都是强制性的——没有一个简短的"为什么会崩溃"，就没有短的 no-good，没有回跳，也就没有收敛。LLM 必须做出解释，而不只是给出判断。