Economics v8

Charles Dana · Monce SAS · April 2026

The principle

v8 meters every call in characters of CNF. One byte = one token. The tier router maps tokens_in to an engine mix; the watchdog maps budget to a wall-clock ceiling; the envelope returns total_ms and cost_usd on every response. Cost scales with engines actually used — local reducer runs are free above fixed infrastructure.

Per-engine cost

Observed cost per status

SATLIB crowdsource game (live)

Push mode — spot a laptop's worth of compute

Monthly ceiling: $50. Per-call ceiling: $12. Refused at the service level before any Lambda fires. Live status: /satlib/push_status.

Reference point: snakebatch.aws.monce.ai had a single $5 call in its history — that's the ballpark of serious compute spending here.

Budget shapes the mix

budget = 1 s      -> local_reduce + kissat.   $0 marginal.
budget = 5 s      -> + v6 race.               < $0.001.
budget = 60 s     -> + v7 swarm (up to ~200). < $0.05.
budget = 240 s    -> push:laptop (up to 300). < $12.00.
budget = 70 s     -> push:extreme (up to 1 000 workers). < $12.00.

Why it stays cheap

The local reducer absorbs easy instances before any Lambda fires. Kissat closes out small hard instances on-host. v6 only sees instances big enough to benefit from parallel branch; v7 only sees instances too big for a single payload. Each tier "charges" for the complexity it deserves. Push mode exists for the cases where none of that is enough.

Playground (/playground) — cost envelope

The inverse calculator runs entirely on the EC2 host: Tseitin encoding in Python, Kissat as a subprocess. No Lambda fans out, no S3 round-trip in the hot path. Cost is strictly EC2-seconds × rate. Public measured runs:

Basis: t3.medium on-demand in eu-west-3 is $0.0496/hr = $1.38×10⁻⁵/s. A 100k-variable inversion costs about one thousandth of a cent. Factoring a 64-bit verified semiprime on the public API costs about one hundred-thousandth of a cent. You hit the multiplier wall (Θ(n²) clauses) long before you hit the budget wall.

What is expensive: factoring at crypto scale. A 256-bit RSA multiplier would compile to ~2.5M clauses; Kissat alone will not close it in any tractable budget. For those, the playground is a compilation front-end only — the CNF would route through v8 + push mode and accept the $12-per-call ceiling.

npdollars vs AUMA — when each dollar pays for what

Both services are billed per-second of compute on EC2, both on the same region (eu-west-3, t3.medium). The economic question is what kind of answer your dollar buys:

Cost of certainty. npdollars charges more per problem because it returns a certificate (SAT with model, or UNSAT with resolution proof). AUMA charges less because it returns a number — which is fine when "close enough" suffices. On a 1 000 001 factoring, AUMA's 97 ms sweep costs ~$1.3×10⁻⁶ and returns nothing exact; npdollars' 126 ms costs ~$2×10⁻⁶ and returns 101 × 9 901. The certainty delta is 50%, the correctness delta is infinite.

Fixed infrastructure

.ncnf endpoints — cost per call

Every call runs on the EC2 t3.medium host (no Lambda). Cost is strictly EC2-seconds × rate = $1.38×10⁻⁵/s.

One-liner: proving a 3.2-million-clause SAT theorem about 10k integer additions, on our public API, costs roughly one hundredth of a cent.

.ncnf — dollars become capital

The /ncnf pipeline adds a new economic regime. Every UNSAT proof the swarm produces is lifted into a quantified taboo and appended to the input. Cost paid once, amortized across every future instance of the same structural family.

The taboo library is capital, not expense. Every dollar spent on a novel family writes structure that costs nothing to re-use. The more you solve, the cheaper the next solve gets.

Polynomial wall-clock on small/medium instances. On hard instances, the budget dial controls dollars and the REDUCED contract ensures you always get a formula back that is strictly easier than the one you sent.

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