From CDCL to MCTS: non-determinism + infinite branching
Parent: recursive-harness
The classic SAT/CSP framing (csp-formalization, conflict-learning-and-backjumping) assumes finite + deterministic + sound. The agent harness breaks all three, which pushes the algorithm into a different regime.
Preserved vs broken
- Preserved (structure): worlds = configurations, collapse = pruning, convergence = narrowing to
P×Cresidual, recording collapse-info = provenance, backjump-to-the-real-culprit. - Broken (guarantees): CDCL's convergence rests on finite + deterministic + sound; the agent violates all three.
Difference 1 — non-determinism ⇒ an unsound theory solver ⇒ no-goods can be false
Classic propagation/conflict-detection is deterministic and sound (a learned no-good is always true). The LLM's incompatibility judgment is stochastic and can be wrong:
- false conflict → a wrong no-good → permanently prunes a good world; missed conflict → walk into a dead world.
- Worse than deducible-not-known (incomplete): this is unsound (asserts false entailments).
- → The "knowledge grows monotonically" convergence guarantee breaks — learning a false no-good is non-monotone in truth (you deleted a real solution).
Fix: no-goods can't be hard, permanent clauses. Make them soft / weighted / revisable: verify-before-commit (multi-sample / adversarial re-check before固化); down-weight uncertain incompatibilities instead of eliminating. Regime slides from hard CSP → weighted CSP / Max-SAT / probabilistic inference (belief propagation) — collapse becomes a belief update, not a hard deletion.
Difference 2 — (effectively) infinite branching ⇒ sample, not enumerate ⇒ MCTS, not DFS/BFS
Classic DFS/BFS/CDCL enumerate children over a finite domain. The agent's domains are infinite ("what should the headline be"):
- can only sample a few candidates (LLM as policy) + a value estimate for which is promising;
- searching a sampled, stochastically-evaluated tree = Monte Carlo Tree Search: select (UCT = value + exploration bonus) → expand → evaluate → backprop. (AlphaGo/AlphaProof.)
- Completeness is gone: with infinite branching + sampling you can't prove UNSAT (can't enumerate all worlds) → you can only satisfice, stopping at
P×C.
The formal home shifts: SAT/CSP → MCTS + soft constraints
| classic CDCL | agent harness | |
|---|---|---|
| branching | finite, enumerate | infinite, sample (LLM = policy) |
| propagation / conflict | deterministic, sound | stochastic, unsound |
| no-good | hard clause, permanent | soft / weighted / revisable belief |
| search | DFS + learning + backjump | MCTS (value-guided + explore/exploit) |
| termination | complete (can prove UNSAT) | satisfice to P×C only |
This is exactly the LLM + tree-search frontier: Tree of Thoughts, LATS (Language Agent Tree Search), AlphaProof-style MCTS-guided reasoning.
One line
Structure (worlds / collapse / provenance / backjump) is inherited from CSP; but non-determinism (no-goods can be false → soften them to weighted, revisable beliefs) and infinite branching (can't enumerate → sample → MCTS, not DFS/BFS; no completeness, only satisfice) push the algorithm from CDCL to "LLM-as-policy+value MCTS + soft constraints + P×C satisficing."