The Symbolic Core: Clew, Minos & Palimpsest

V8 (Ariadne — the self-authoring detective universe) is built on one decision: the LLM proposes; a constraint solver disposes. A fair, solvable mystery has a symbolic skeleton — ground truth, clue logic, and a machine-checked uniqueness proof — that is authoritative, and an experienced surface — prose, dialogue, art, voice — that agents realize from that skeleton and regenerate on failure. The symbolic core is the half that has to be provably correct, not merely plausible, and it is where the real, deterministic, CPU-only code concentrates. Three subsystems make it up. Clew is the generative case engine: it picks the answer first, weaves a self-consistent world around it, and derives the player-facing clues backward from the facts that distinguish the culprit. Minos is the solvability verifier: a real constraint solver (two of them — a finite-domain CSP and a propositional DPLL SAT solver) that proves the player-visible clues admit exactly one solution and that it is the intended one. Palimpsest is the canon graph: the persistent, content-hashed continuity world that grounds generation and remembers what the player did. Everything else in the pipeline — the writers' room, the asset fabric, the compiler — hangs off these three. This page is the deep companion to ../V8_ARCHITECTURE.md; the eleven-stage narrative and the data contracts live in its §2–§4.

What ships, honestly#

The solver logic is real and tested against known-correct answers, not a boolean stub. The finite-domain CSP (libs/v8/case-csp) is a genuine backtracking search with node consistency, minimum-remaining-values ordering, and forward checking (csp-solver.ts:212); its spec proves the canonical Zebra puzzle — exactly one solution, "the Norwegian drinks water, the Japanese owns the zebra" (csp-solver.spec.ts:168) — so the engine is anchored against a result it cannot fake. The propositional path (libs/yemaya/case-verifier) is a real Davis–Putnam–Logemann–Loveland SAT solver with unit propagation and pure-literal elimination (sat/dpll.ts:124), proven on a UNSAT pair and a five-variable implication chain (minos.test.ts:51,:68). Clew generates deterministically from (seed, canon) — the same inputs reproduce the same case (clew.ts:41) — and the LLM "proposer" is an injectable seam that defaults to a NullProposer and fails loud if a wired provider errors rather than fabricating flavor (clew.ts:204). Palimpsest's graph, hybrid retrieval, G7 consistency check, outcome write-back, and content-hash snapshots are all real and tested (libs/yemaya/canon-graph).

What is a seam, not a fabrication: the media providers a case needs (Stability/Flux portraits, Hunyuan3D/Meshy 3-D, Suno music, ElevenLabs VO) are injected CaseMediaGenerator boundaries; an absent provider yields a status: 'not-configured' asset slot — never a fabricated asset (case-bundle.ts:66,:262). clingo is an optional accelerator: when no binary is on PATH the in-process DPLL decides the same question and returns the same verdict (asp.ts:77), and the sidecar honestly reports backend: 'dpll' (minos.test.ts:93). The embedding signal in retrieval is feature-hashing, a real, documented approximation — not a neural model. The graph that ships is the in-memory typed property graph plus its content hashing; Postgres+pgvector/Neo4j persistence is the deployment target named in V8_ARCHITECTURE.md §4.3, not a dependency these libs hide.

Clew — the generative case engine#

Clew implements the EXAG backward-generation pattern (sota§1): choose the answer, then derive the self-consistent world around it. It runs in two passes and emits two artifacts — the player-facing MysterySession IR that Minos and Daedalus consume, and the hidden CaseGroundTruth (ground-truth.ts:156) that is never shown to the player.

Solve-first ground truth#

buildBlueprint (truth-weaver.ts:45) drives everything off a SeededRng so the construction is reproducible. It picks a culprit index, builds N suspect "plans," and — this is the solve-first guarantee — gives the culprit hasMeans ∧ atScene ∧ ¬alibiVerified while each innocent gets exactly one fair exoneration from a rotating set: a verified alibi, demonstrable absence (no-opportunity), or no access to the weapon (no-means). Innocents usually keep a motive (a 75% roll, truth-weaver.ts:111) so they read as plausible suspects — fair red-herring characters cleared by a single discoverable fact. The timeline is then materialized and run through real conflict detection: no person in two places at once, and the culprit present at the scene across the window; a bilocation triggers repairConflicts, and a culprit-absent conflict is a construction error that throws rather than shipping a broken case (truth-weaver.ts:220).

The decisive output of this pass is the constraint network — the exact object Minos solves. buildStructuralClauses (truth-weaver.ts:337) emits, for each suspect s, the CNF rules that define a culprit:

¬culpritIs(s) ∨ means(s)            (a culprit had the means)
¬culpritIs(s) ∨ atScene(s)          (a culprit had the opportunity)
¬culpritIs(s) ∨ ¬alibiVerified(s)   (a culprit has no verified alibi)

plus exactly-one-culprit (an at-least-one disjunction over culpritIs, and pairwise at-most-one ¬culpritIs(i) ∨ ¬culpritIs(j)). These rules are hidden — their derivedFromClueIds is empty, marking them as the game's known logic rather than player-discovered facts (ground-truth.ts:145). The player learns the per-suspect facts from clues; the rules entail the unique answer.

Backward clue derivation#

The Clue-Smith pass (clue-smith.ts:48) walks the ground truth backward: for every culprit-distinguishing fact it derives the player-facing clue that establishes it, tagging each clue's pointsTo[]/eliminates[] against the solution variables — the "clue inventory tied to solution variables" of sota§1. Each derived clue also emits a fact clause whose derivedFromClueIds names the clue that reveals it, so Minos's proof can include exactly the facts a player can reach. Elimination clues clear innocents (eliminationClue), incrimination clues establish the culprit's means and opportunity, and the late, decisive alibiFlawClue breaks the culprit's alibi (clue-smith.ts:84,:219). Red herrings are emitted with redHerringFairness: 'fair' and a refutedBy pointer — each is guaranteed refutable because the eliminating clue for that suspect is in the inventory (clue-smith.ts:253). Finally buildSolution assembles the ordered deductionPath — Ariadne's thread — eliminations first, then the single-survivor incrimination, then the accusation, each step using only earlier-introduced clues.

The polarity of the alibi literal is load-bearing here, and it is the subtle thing the SAT layer exists to catch (see the sign bug below). An innocent's elimination-by-alibi clue asserts the positive atom alibiVerified(s) (clue-smith.ts:116); the culprit's alibi-flaw clue asserts the negated atom ¬alibiVerified(culprit) (clue-smith.ts:244). Get that sign backward and the case stops being solvable.

The forge output#

In the libs/v8 vertical, Clew's output is bundled by forgeCaseBundle (case-bundle.ts:236), which makes the solve-first discipline executable: it calls proveCaseUniqueness before any generation and throws CaseNotSolvableError on a non-unique skeleton (case-bundle.ts:237) — the spec proves no prose or media is generated for an unsolvable case (case-bundle.spec.ts:169). A missing prose writer throws CaseBundleNotConfiguredError (fail loud, :241); each produced asset is C2PA-stamped by hashing its bytes and Ed25519-signing a canonical manifest (stampAsset, :184), and verifyCaseAssetManifest (:215) flips to false if any signed field is tampered (case-bundle.spec.ts:147). The assembled case is then run through the seven-gate suite. Solvability gates the bundle; provenance and quality gate its release.

Minos — proving solvability & fair play#

Minos is the gate. Its headline obligation is formal uniqueness: with only the clues the player can actually reach, is the culprit the only satisfying answer? Three verdicts matter — zero satisfying suspects means UNSOLVABLE (over- constrained), exactly one means UNIQUE (the answer is entailed), and two or more means AMBIGUOUS (under-constrained). V8 answers this question with two independent, real solvers that decide the same thing, which is itself a cross-check.

Two solvers, one question#

The split is deliberate. The finite-domain CSP (libs/v8/case-csp) treats the case as variables over finite value-domains (a culprit selector, a weapon selector, …) and is the engine the forgeCaseBundle path proves against. The propositional DPLL (libs/yemaya/case-verifier) treats the case as a Boolean CNF over one variable per (suspect, attribute) atom plus a culpritIs selector, and is the engine the Minos orchestrator and the ASP sidecar use. Both compile only the player-available clauses and both reduce uniqueness to model counting; they are two routes to the same unique | unsolvable | ambiguous answer.

The finite-domain CSP#

solveCsp (csp-solver.ts:212) is a textbook-correct, complete backtracking search. It validates the model, seeds node consistency from the unary constraints (equals/not-equals/in prune domains up front), then searches with minimum-remaining-values variable ordering (selectVar, :260 — always branch on the most-constrained variable, breaking early on a singleton) and forward checking (forwardCheck, :278 — after each assignment, prune neighbour domains that a shared constraint would definitely violate, recording removals to undo on backtrack). The soundness hinge is constraintViolated (:120), which returns true only when a constraint can no longer be satisfied, leaving undetermined constraints alone so the search is both sound and complete; a degenerate 0-ary relation that the incremental checks would never see is still enforced by a full constraint sweep at each leaf (:314, with a dedicated soundness-guard test at csp-solver.spec.ts:68). proveUniqueSolution (:356) asks for up to two solutions: none ⇒ unsatisfiable, one ⇒ unique (with the witness), two ⇒ under-determined.

The mystery layer compiles to this. compileMysteryToCsp (mystery-skeleton.ts:136) turns a MysterySkeleton's clue constraints (is, is-not, one-of, if-then, same, and a general allowed-tuple relation, :33) into CSP constraints, including by default only the presented clues — the model the player can solve from. proveCaseUniqueness (:239) then enforces two things: the presented clues must admit exactly one solution and that solution must equal the ground truth. A case that is under-determined, unsatisfiable, or that proves a different culprit than intended is rejected with an honest reason (:251), and only the all-clear sets the uniqueSolutionProven flag the G2 gate stands on.

The DPLL SAT path and the ASP sidecar#

The propositional route is the one the V8_ARCHITECTURE.md §4.2 design names. The constraint network is compiled to CNF over integer-indexed variables by compileToCnf (sat/cnf.ts:62), whose includeClause predicate is exactly the fairness filter — structural rules plus only the fact clauses whose derivedFromClueIds are all player-available (uniqueness.ts:32). proveUniqueness (uniqueness.ts:47) then tests each suspect by assumption: suspect s is a possible culprit iff CNF ∧ culpritIs(s) is satisfiable, decided by isSat (sat/dpll.ts:129). Count the survivors: 0 ⇒ unsolvable, 1 ⇒ unique, ≥2 ⇒ ambiguous, with every offending culprit returned for the repair loop. The DPLL itself (solveFrom, :98) is the real 1962 algorithm — unitPropagate simplifies clauses and detects conflicts/units (:29), pureLiteralAssign fixes single-polarity variables (:65), and the solver branches on a free variable and backtracks on conflict.

apps/v8/minos-asp-sidecar packages this behind a small HTTP surface so the proof can be offloaded to a clingo container. emitAspProgram (asp.ts:24) writes a real Answer-Set Program in Potassco syntax — 1 { culprit(S) : suspect(S) } 1. for exactly-one-culprit, player-available facts as asserted atoms, and the structural rule as integrity constraints including :- culprit(S), attr(S, alibiVerified). (a culprit must not have a verified alibi). runUniquenessViaAsp (asp.ts:77) uses clingo when clingoAvailable() reports it on PATH and falls back to the in-process DPLL when clingo is absent or its output is unparseable — never fabricating a verdict (asp.ts:93). The sidecar exposes POST /solve and GET /health over node:http (server.ts:24); its test proves a real HTTP round-trip returning status: 'unique', matchesGroundTruth: true on the DPLL backend (sidecar.test.ts).

The alibi-rule sign bug#

The V8 audit records that this DPLL layer caught a real alibi-rule sign error during development — and the structure above is exactly why a model-counting solver catches it where a boolean stub would not. The culprit rule ¬culpritIs(s) ∨ ¬alibiVerified(s) (truth-weaver.ts:357) and the alibi-flaw fact clause ¬alibiVerified(culprit) (clue-smith.ts:244) both depend on the negated flag of an alibiVerified literal. Write the rule literal with the wrong polarity — the positive alibiVerified(s) an innocent's elimination clue legitimately uses (clue-smith.ts:116) — and the rule becomes ¬culpritIs(s) ∨ alibiVerified(s), i.e. "a culprit has a verified alibi," the exact opposite of the intent. Now assume the true culprit: culpritIs(culprit) forces alibiVerified(culprit) = true through the inverted rule, while the alibi-flaw clue forces it false — a conflict. DPLL reports the true culprit as not viable, and proveUniqueness returns unsolvable (or a wrong unique answer) instead of unique/matchesGroundTruth. A stub that only returned a boolean "looks fair" would have sailed past it; counting models against the actual CNF surfaces the inverted sign immediately. The fix is the polarity the code now carries, and the regression is pinned by the orchestrator test that the generated culprit proves unique and matches ground truth (minos.test.ts:86).

The full verifier and the seven gates#

verifyCase (minos.ts:25) is the orchestrator: G1 formal uniqueness (via runUniquenessViaAsp), G2 deductive completeness (completeness.ts:15 — every deduction step uses only clues introduced before the reveal, no withheld clues, no forward references, strictly increasing order, and every declared essential clue actually used), G3 fair-play run through the existing Knox/Van-Dine MysteryFairnessValidator unchanged — Minos enforces the repo's authoritative checker rather than reinventing fairness, requiring a rating of exemplary or fair (fairplay.ts:32) — plus investigation-mechanic balance and a difficulty grade. The verdict is a VerifierReport sealed with a SHA-256 content-hash signature so a tampered or stale report is detectable (report.ts:48). On failure, the bounded critique-revise repair loop (repair.ts, default 3 retries) hands the specific violations back to a regenerate strategy and escalates to HITL when retries are exhausted.

Separately, libs/v8/case-gates registers the seven release gates G1–G7 on the shared @oshun/content-release-gates service — fairness, solvability, clue- grounding, voice, misdirection, prose, safety (case-gates/src/index.ts:99). G2 consumes the uniqueSolutionProven flag the CSP produced; the suite is composed from the platform's gate builders, not forked, and its spec asserts that each fault blocks its own gate (case-gates.spec.ts:30).

Palimpsest — the canon & continuity graph#

Palimpsest (@yemaya/canon-graph) is the persistent world every generated case is grounded in, so cases populate one coherent city rather than disconnected vignettes. It is a typed property graph (CanonGraph, graph.ts:17) of characters, locations, factions, timeline-events, prior-case outcomes, and open threads, with deterministic insertion-ordered iteration and out/in adjacency indexes so neighbour queries are O(out-degree) and hashing is reproducible.

SCORE-style hybrid retrieval#

Generation never sees the whole graph; retrieve (retrieval.ts:146) returns a bounded CanonContext — the top-K relevant entities (each carrying its live state and a normalized relevance), hierarchical prior-case summaries, the hard continuity constraints derived from the retrieved sub-graph, and the open threads the Oracle may weave in. Ranking is a genuine hybrid of two independent signals: a from-scratch tf-idf cosine (lexical, tfidf.ts) and a feature-hashing embedding cosine (semantic, embedding.ts), combined by hybrid = wt·tfidfCosine + we·embeddingCosine with renormalized 0.5/0.5 default weights (hybridScore, retrieval.ts:67). Required cast/location ids are force-included with a relevance floor so a hard constraint is never pruned by the top-K cut. This is the "SCORE" pattern — prior-case outcomes are first-class retrievable nodes carrying their current dynamic state, so a new case reuses the city's actual history.

G7 consistency — real per-claim contradiction logic#

checkConsistency(draft, graph) (consistency.ts:227) is the continuity gate, and it is real comparison logic per claim kind, never an always-empty return. A geography claim that re-parents a known location contradicts its recorded located-in edge (HARD); a character-fact claim against a recorded state cell is HARD, while an unrecorded key is SOFT (a plausible new fact surfaced for review); a timeline claim ordering two events against their recorded years is HARD; negating a recorded member-of relationship or flipping a recorded case outcome is HARD. The check is snapshot-relative — it judges a draft against the exact canon version it was grounded on.

Write-back and content-hashed snapshots#

When a verified case is played, commitOutcome (writeback.ts:49) makes the result durable world history: it creates a prior-case-outcome node, chains it onto the campaign succession, updates suspect states (convicted → convicted, accused → cleared), and closes resolved threads. The signature continuity move is the wrongly-accused suspect, whose state becomes freed-vengeful and who opens a vengeance open-thread the Oracle can weave into a future case (writeback.ts:121) — the feedback loop that makes the city remember the player's mistakes. Every commit materializes an immutable, content-hashed snapshot; history is append-only so any case can be re-grounded against the snapshot it was generated from.

That hash is the reproducibility anchor. snapshotHash (snapshot.ts:66) is a SHA-256 over a fully canonicalized serialization — nodes sorted by id with sorted, type-tagged state keys, edges sorted by (from, relation, to) — so the same logical graph always hashes the same and any node/edge/state change flips it. Together with the seed and the model-version ids this forms the (seed, model-versions, canon-hash) key the pipeline records on every case (V8_ARCHITECTURE.md §5), which is what makes a generated case deterministically replayable. The CanonContext contract itself lives in case-contracts (canon-context.ts) so producers and consumers share one shape without a hard lib-to-lib dependency.

Edge cases & failure modes#

• Unsolvable / over-constrained. Zero suspects satisfy the player-available clues. The CSP returns unsatisfiable (proveUniqueSolution), the DPLL returns unsolvable. forgeCaseBundle throws CaseNotSolvableError before generating anything (case-bundle.spec.ts:169); the verifier fails G1.
• Under-determined / ambiguous. Two or more suspects survive — the second solution is enough to reject. The CSP stops at the second model (maxSolutions: 2); the DPLL returns every viable culprit for the repair loop.
• Unique but wrong. The visible clues prove exactly one culprit, but it is not the ground truth — a generation bug the prover surfaces honestly rather than asserting away (mystery-skeleton.ts:263, uniqueness.ts:77).
• A needed clue is withheld. Dropping an essential elimination clue from the available set flips a previously unique case to ambiguous and fails G1 — pinned by minos.test.ts:179. This is the whole point of compiling only player-available clauses: solvability is judged from what the player can actually reach.
• Forward reference in the thread. A deduction step reasoning from a clue that arrives later than a prior step is a G2 violation (completeness.ts:67).
• Absent media / model providers. A kind with no CaseMediaGenerator yields a not-configured slot; a wired LLM proposer that errors propagates (fail loud). Neither is faked.
• No clingo binary. The sidecar and verifier fall back to the in-process DPLL and report backend: 'dpll' — same verdict, honestly labeled (minos.test.ts:93).
• Degenerate constraints. An always-false 0-ary relation is still enforced at the CSP leaf (soundness guard, csp-solver.spec.ts:68); a node-consistency wipeout short-circuits to "no solution."

Related#

• ./canonical-data-contracts.md — CaseSpec, CaseGroundTruth, the MysterySession IR, and the V5 compile target the symbolic core produces and consumes.
• ./anansesem-loom-and-ori-suspects.md — the writers' room, asset fabric, and living suspects that realize the verified skeleton into prose, art, voice, and interrogation.
• ./daedalus-compiler-and-theseus-eval.md — the compiler that emits the V5 pack and the automated playtester that proves the case solvable in game data, end to end.
• Hub: ../V8_ARCHITECTURE.md.