Exhibit · L1_CONSTRAINT

Sudoku, metered.

Same chip. Same problem encoding. Two algorithms. On the left, AC-3 + MRV — the cascade's L1_CONSTRAINT tier. On the right, full brute-force — what an LLM emits when you ask it to write a Python solver. The joule receipts speak for themselves.

Headline · easy 9×9 (Norvig's first example)
Given
5
3
7
6
1
9
5
9
8
6
8
6
3
4
8
3
1
7
2
6
6
2
8
4
1
9
5
8
7
9
Solved
5
3
4
6
7
8
9
1
2
6
7
2
1
9
5
3
4
8
1
9
8
3
4
2
5
6
7
8
5
9
7
6
1
4
2
3
4
2
6
8
5
3
7
9
1
7
1
3
9
2
4
8
5
6
9
6
1
5
3
7
2
8
4
2
8
7
4
1
9
6
3
5
3
4
5
2
8
6
1
7
9
L1_CONSTRAINT · AC-3 + MRV
6.5 µJ
776 µs wall
checks: 37,156
propagations: 9,372
backtracks: 0
Brute-force baseline
33.0 mJ
11.76 s wall
checks: 367,505,360
backtracks: 65,946,190
Energy ratio
5,049×
L1_CONSTRAINT delivers the same solution at 5,049× less energy.

All runs

Five canonical CSP problems. L1_CONSTRAINT path and brute-force baseline where the latter completes in human time. N-queens 4/6/8 is a wash — for trivially small problems, AC-3's propagation overhead dominates. That's the point: the cascade routes by problem size, not ideology.

Problem L1 energy L1 wall Brute energy Brute wall Ratio Verified Hashes
sudoku_easy 6.5 µJ 776 µs 33.0 mJ 11.76 s 5,049× ✓ AC-3 · brute · z3 agree
sudoku_hard 60.8 µJ 5.3 ms — — — ✓ AC-3 · z3 agree
nqueens_4 44.5 nJ 5 µs 7.0 nJ 1 µs 6.3× worse ✓ AC-3 · brute · z3 n/a
nqueens_6 272 nJ 26 µs 53.9 nJ 4 µs 5.0× worse ✓ AC-3 · brute · z3 n/a
nqueens_8 997 nJ 93 µs 307 nJ 19 µs 3.2× worse ✓ AC-3 · brute · z3 n/a
nqueens_12 4.9 µJ 386 µs — — — ✓ AC-3 · z3 n/a

Verified is the load-bearing column: every solver's solution is re-checked against the CSP through mgai_proof::verify_with, independent of which engine produced it. Hashes only need to agree when the puzzle has a unique solution (both Sudoku). N-queens has many valid solutions, so AC-3 and z3 legitimately return different ones — each still verifies. A system that claimed "hashes always match" would be lying about multi-solution problems.

L4.5_PROOF · Verifiable

Verify yourself

Every row carries one ProofReceipt per solver — a blake3 anchor over the canonical problem encoding and the solution. Three solvers run: AC-3 + MRV, full brute-force, and z3 (SMT). Each solver's solution is re-checked against the CSP through the shared verifier. Reproduce locally: 

curl -s https://mathground.ai/exhibits/csp-receipts.json | jq '.runs[0]'
cargo run --release -p mgai-csp-bench -- /tmp/repro.json
# uniquely-solvable puzzles → all solver hashes equal:
jq '.runs[0] | [.smart_proof, .brute_proof, .z3_proof] | map(.solution_hash) | unique' /tmp/repro.json

mgai_proof::Solver is the contract; mgai-csp and mgai-proof-z3 are two implementations. A Lean backend slots in the same way — the receipt shape doesn't change, and the verifier checks satisfaction, not just hash equality.

Method

Both paths solve the identical CSP encoding (variables, domains, binary constraints). The L1_CONSTRAINT path runs AC-3 arc-consistency once, then backtracks with MRV variable selection and re-propagation after each assignment. The brute-force path tries values in order and re-checks every constraint after every assignment — no domain pruning, no propagation.

Energy is a per-op picojoule model: domain_check = 50 pJ, propagate = 500 pJ, backtrack = 200 pJ, select_var = 100 pJ — chip-scale numbers consistent with the cascade's L1_CONSTRAINT band. Wall-time is measured. Both are real receipts, persisted with schema_version 2.

Implementation lives in crates/mgai-csp and the bench harness in crates/bin/mgai-csp-bench. The JSON receipts powering this page are at /exhibits/csp-receipts.json.