Architecture v8

Charles Dana · Monce SAS · April 2026

Request flow

POST /cnf/solve  {dimacs, budget, max_workers}
      |
      v
 +-----------------------------------------------+
 |  v8 Supervisor  (EC2 t3.small)                |
 |                                               |
 |  1. parse header -> (n_vars, n_clauses)       |
 |  2. tier = f(chars)                           |
 |  3. LOCAL REDUCER                             |
 |      - UP to fixpoint                         |
 |      - pure literal elimination               |
 |      - failed-literal probing                 |
 |      - pair look-ahead  ->  2-SAT learns      |
 |     solved? return (local_reduce)             |
 |                                               |
 |  4. Snapshot.seed(local backbones + 2-SAT)    |
 |                                               |
 |  5. SLOW TRAIL: spray 50 async Lambdas        |
 |     (fire-and-forget, keeps learning)         |
 |                                               |
 |  6. Tier dispatch                             |
 |      tier=small  : kissat only                |
 |      tier=medium : kissat || v6  (race)       |
 |      tier=large  : v7 (S3 offload)            |
 |                                               |
 |  7. Watchdog: t0 + budget + 3s                |
 |     harvest late futures -> Snapshot          |
 |     shutdown executors                        |
 |                                               |
 |  8. Build envelope                            |
 |      result ∈ SAT | UNSAT | REDUCED | TIMEOUT |
 |      cnf (audit header + clauses)             |
 +-----------------------------------------------+
      |
      v
 Response: stable JSON envelope

Envelope

{
  "session_id":        "abcd1234ef56",
  "result":            "SAT" | "UNSAT" | "REDUCED" | "TIMEOUT",
  "engine":            "kissat" | "v6" | "v7" | "local_reduce" | "v8_watchdog",
  "tier":              "small" | "medium" | "large" | "xlarge",
  "tokens_in":         25126,            # bytes of request CNF
  "tokens_out":        2147,             # bytes of response CNF
  "n_vars":            400,
  "n_clauses":         1704,
  "total_ms":          8355,
  "cost_usd":          0.000012,

  "assignment":        [1,-2,3,...],     # SAT only
  "partial_backbones": [5,-7,...],       # learned units
  "learned_2sat":      [[-a,-b],...],    # learned binaries
  "cnf":               "p cnf N M\n...",

  "extras": {
    "var_reduction_pct":  6.75,
    "cls_reduction_pct":  14.38,
    "learned_clauses":    292062,
    "workers":            2,
    "engines_tried":      ["v6"],
    "reason":             "race_deadline"
  }
}

Tier routing

Push mode (/satlib/claim?push=...)

Monthly cap: $50. Spend tracker in s3://npdollars/satlib/state/push_budget.json. Every push call records actual cost and refuses further firings once the cap is reached. Account concurrent Lambda ceiling is 20 000 — 1 000 workers is < 5% of that envelope.

Components

Playground — inverse-SAT pipeline

The /playground endpoint is a second entry point into the same Kissat. Instead of accepting raw DIMACS, it takes a list of Python-subset assertions ("x * y == 77", "x > 1", …) and bit-blasts them via Tseitin to CNF.

POST /playground/solve
  {"vars": {"x": 20, "y": 20},
   "asserts": ["x*y==1000001", "x>1", "y>1"],
   "no_overflow": true,
   "max_solutions": 1,
   "timeout_s": 10}
      |
      v
  inverse.api.build_cnf  (AST -> CNFModule)
      |  ripple adder / shift-and-add mul / restoring divmod / Tseitin gates
      v
  CNFModule  =  {n_vars, clauses, inputs: {name -> [lit ...]}}
      |
      v
  to_dimacs()  ->  /tmp/*.cnf  ->  kissat  ->  s/v lines  ->  decode()
      |
      v
  {result: "SAT"|"UNSAT", antecedents: [{x: 101, y: 9901}, ...],
   cnf: {n_vars, n_clauses, encode_ms}, solve_ms}

Max bit-width per variable: 256. Max vars: 8. Max asserts: 16. Multi-antecedent enumeration adds blocking clauses over input bits each iteration and re-runs Kissat, up to max_solutions. Every gate is equisatisfiable, so CNFModule.import_module(other, wire_map) splices a pre-built sub-CNF (e.g. a SHA-256 round, AES S-box) with boundary wires mapped to parent literals — the composition seam for larger circuits.

Bit-blast sizing (measured on live API):

The encoder itself is Python, pure, no dependencies. Kissat is the downstream solver; KISSAT_PATH env var points at /usr/local/bin/kissat on-host. The Playground does not go through the v8 tier router (yet); it calls Kissat directly because the CNFs it produces are small-to-medium tier and the encoder already knows the problem is self-contained. Large circuits (SHA-256 preimage, AES) will route through v8 when added.

npdollars vs AUMA — complementary, not competing

npdollars and AUMA are both Dana projects tackling “find x such that f(x) = target.” They take opposite strategies and win on different inputs:

Head-to-head on 9 live problems (harness: tools/vs_auma.py, both APIs in prod, 2026-04-24):

SCOREBOARD    npdollars: 4 exclusive      AUMA: 3 toy-grid + 2 continuous

  factor 77 / 10 403 / 1 000 001          -> npdollars only (AUMA cannot hit exact factor pair)
  Pythagorean c=65 (all 4 triples)        -> npdollars only (exhaustive enumeration)
  modsqrt / 3x+5y=41 / Ramanujan 1729     -> AUMA fastest (toy grid 10-200 pts, both find it)
  x² ≈ 42 continuous                      -> AUMA only (npdollars has no floats)
  |z²+1| = 0 complex                      -> AUMA only

The kind of wins matters more than the count. AUMA's wins are in 10²–10³ integer grids where exhaustive search is essentially free; npdollars' wins are in regimes AUMA cannot enter — exact factoring, UNSAT proofs, multi-solution enumeration. They are complementary tools: AUMA for continuous smooth problems, npdollars for exact discrete ones.

The race loop

t0 = now
deadline = t0 + budget + 3.0   # slack always present

kissat_fut = thread: kissat(budget * 0.35)
v6_fut     = thread: v6(budget - 0.5)

while futures and now < deadline:
   done = wait_first(futures, timeout = deadline - now)
   for f in done:
     if kissat and SAT/UNSAT: winner = kissat
     elif v6 and SAT/UNSAT:   winner = v6
     else: absorb partial state into snapshot

# Harvest any future that finished after wait but before we gave up
for f in futures_still_running:
   if f.done(): snapshot.absorb(f.result())

shutdown(cancel_futures=True)
return winner_envelope OR snapshot.bail()

Slow trail

/cnf/solve  ----->  response (within budget+3s)
     |
     +----- spawn daemon thread:
               upload formula -> S3
               fire npd-logicspace INIT (async)
               fire 8 npd-v6-worker invocations (async)
                 depths: 1,1,2,2,3,3,4,5
               thread exits

[LATER, in AWS]
  LogicSpace and v6-workers run for minutes
  they write learned clauses into
    s3://npdollars/v8/trail/<sid>/
  next query on this sid hits the cache

.ncnf — lifted output for structured problems

A second entry point lives alongside /cnf/solve: /ncnf publishes the manifesto and POST /ncnf/solve accepts a registered problem (php, sudoku, pythagorean, coloring, mutilated_chessboard, tseitin, ordering) and returns an envelope shaped like the .ncnf contract: input is .ncnf, output is .ncnf with more taboos. Monotone, composable, closed under the format.

POST /ncnf/solve  {problem, params, budget, benchmark}
      |
      v
 +-----------------------------------------------+
 |  ncnf.api.solve_request                       |
 |                                               |
 |  1. build skeleton from registered problem    |
 |  2. baseline: median kissat on ground form    |
 |  3. engine.solve:                             |
 |     - ground to DIMACS                        |
 |     - kissat with --binary=false + DRAT       |
 |     - SAT: lift model to unit entries         |
 |     - UNSAT: parse DRAT, pick short clauses,  |
 |              unify index shape, emit Taboo    |
 |     - TIMEOUT: induce from partial proof      |
 |  4. enriched: median kissat on skeleton + T   |
 |  5. envelope: {baseline_ms, enriched_ms,       |
 |               speedup, induced, taboos[...]} |
 +-----------------------------------------------+

Taboo induction reads kissat’s DRAT proof as a list of ground learned clauses, groups them by shape (arity + variable-sign pattern + index-offset signature), and emits a quantified template whenever a shape appears at least min_support times. The template replays across the full index domain, not just the concrete clauses kissat emitted — this is why a single lifted taboo turns PHP(12, 13) from a 60 s TIMEOUT into a 1.9 ms UNSAT.

.ncnf endpoints — the full surface

.ncnf pipeline

┌──────────────────────────────────────────────────────────────────┐
│  ncnf.api                                                        │
│                                                                  │
│  solve_request  ──►  engine.solve                                │
│                        ├─ ground to DIMACS                       │
│                        ├─ kissat --binary=false + DRAT proof     │
│                        ├─ SAT : lift model to units              │
│                        ├─ UNSAT: parse DRAT                      │
│                        │         ├─ canonical shapes             │
│                        │         ├─ support ≥ min_support     │
│                        │         └─ emit quantified Taboo        │
│                        └─ return NCNF (monotone in taboos)       │
│                                                                  │
│  lift_request   ──►  lift.cnf_to_ncnf                            │
│                        ├─ parse DIMACS                           │
│                        ├─ pick schema (given / factor n_vars)    │
│                        ├─ shape-cluster all clauses              │
│                        ├─ full orbit  ─► Clause template         │
│                        ├─ partial     ─► taboo(origin=lifted)    │
│                        └─ round-trip verifier                    │
│                                                                  │
│  scaling_request ──► complexity.scaling_study                    │
│                        ├─ for each n in sizes:                   │
│                        │     build, ground, lift, kissat, solve  │
│                        └─ log-log OLS fit per series (r²)       │
│                                                                  │
│  flex_request   ──►  problems.integer_sum                        │
│                        └─ ripple adder chain + unit pins         │
│                        ──► kissat  ──► decode x[k,j] bits        │
└──────────────────────────────────────────────────────────────────┘

Problem registry

Registered families (used by /ncnf/solve, /ncnf/scaling, and the inducer):

The REDUCED contract

When we return result=REDUCED, the CNF body carries backbones as unit clauses followed by learned binaries. Every one is a proven consequence of the input. Concatenating them with the original preserves equisatisfiability and makes the instance strictly smaller for any subsequent solver — including a re-POST to npdollars.

Charles Dana · Monce SAS · April 2026
Co-Authored-By: Claude (Anthropic)