The harness is DPLL(T) with the LLM as a fallible theory solver

Parent: recursive-harness

Background: how SMT plugs semantics into SAT (DPLL(T))

SMT = SAT + theories (arithmetic, arrays, …): atoms like x+y<5, not just Booleans. Architecture:

a SAT core (CDCL) handles the Boolean skeleton, treating each theory-atom as an opaque Boolean;
a separate theory solver checks whether the currently-true theory-atoms are consistent in the theory;
loop: SAT core proposes a Boolean model → theory solver checks T-consistency → if inconsistent, it returns a small explanation (a tiny conflicting subset, e.g. x>3 ∧ x<2) → fed back as a learned clause → CDCL backjumps. Plus theory propagation (the theory can force atoms).
Requirement: the theory solver must emit a small conflict/explanation, or the SAT core can't learn a useful no-good.

The mapping

The LLM-judged semantic constraints = a "theory"; the LLM = the theory solver. So the recursive harness (csp-formalization) is DPLL(T) — only the theory solver is fallible and heuristic, not an exact decision procedure.

Two consequences that fall straight out

Design requirement (not optional): the LLM must explain its incompatibility verdicts. To get CDCL's payoff (learning + backjumping, conflict-learning-and-backjumping), a "these two methods are incompatible" verdict must come with a reason / the small set of atoms responsible = a theory explanation. A bare yes/no forces you to learn the whole path as the no-good → near-zero pruning → back to thrashing → non-convergence. So "the LLM must surface why a world collapsed" is derived from the DPLL(T) mapping, not a nice-to-have.
It's DPLL(T) with a fallible theory solver. Real theory solvers are sound + complete decision procedures; the LLM mis-judges (misses or invents incompatibilities). This is exactly deducible-not-known (the LLM is a heuristic for intractable deduction) and it's why the implication graph for semantic constraints is approximate — built from LLM-given reasons that may be wrong.

Revisited — under the theory layer

"Fallible" now has a price tag: the solver's per-call error is the ε of inexact-contraction — tolerable iff the surrounding loop contracts, with permanent floor ε/(1−k). Fallibility is safe under contraction and fatal without it.
"Must explain" and "checks emit gradients" are the same principle from both sides (coupling-to-the-learner): the gate must give the solver a legible gradient, and the solver must give the coordinator a small explanation — both exist so that conflict analysis stays cheap and localized.
The SAT core's seat is now specified: it is the mechanical kernel of coordinator-not-arbiter — no-good/cut store, provenance graph, ledgers — never an LLM.

One line

Mechanical constraints → exact propagation (real CDCL). Semantic constraints → the LLM as a fallible theory solver (DPLL(T)). Either way, conflict explanations are mandatory — without a small "why it collapsed," there's no short no-good, no backjump, no convergence. The LLM must explain, not just judge.