# 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](../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](#the-alibi-rule-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`).

```mermaid
flowchart TD
  SEED[CaseSpec + seed] --> TW[Clew: Truth-Weaver<br/>buildBlueprint solve-first GT]
  PAL[(Palimpsest canon graph)] -->|retrieve CanonContext| TW
  TW -->|structural CNF rules| CS[Clew: Clue-Smith<br/>backward clue derivation]
  CS --> IR[MysterySession IR + CaseGroundTruth]
  IR --> M{Minos: prove uniqueness<br/>player-available clues only}
  M -->|CSP: solveCsp / proveUniqueSolution| V1[verdict]
  M -->|DPLL/ASP: proveUniqueness via sidecar| V2[verdict]
  V1 & V2 --> Q{unique AND matches GT?}
  Q -- no: unsolvable / ambiguous / wrong --> R[repairLoop: regenerate offenders<br/>bounded retries then HITL]
  R --> CS
  Q -- yes --> G[G1-G7 gates: fairness, solvability,<br/>grounding, voice, misdirection, prose, safety]
  G -->|cleared| OUT[verified skeleton to writers' room + Daedalus]
  OUT -.->|commitOutcome write-back| PAL
```

## 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](./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](./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](./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](../V8_ARCHITECTURE.md).