.ncnf manifesto

Indexed CNF. Polynomial skeleton + taboos.

Charles Dana · Monce SAS · April 2026

0. The arrow

A SAT solver, traditionally, is a function formula → assignment (or ⊥). That signature is lossy in both directions. The input throws away structure (DIMACS forgets how the formula was generated). The output throws away structure (one witness, no description of the solution set, no explanation of unsatisfiability).

.ncnf fixes both ends with one move: input and output live in the same grammar. A solver is a total function

The output is never a naked assignment and never a naked ⊥. It is an .ncnf file describing all models — as ground units if the model is unique, as residual templates if the solution set is parametric, as a refutation taboo if the problem is UNSAT, as a strictly-reduced .ncnf if the budget ran out. Solutions compose because solutions and problems are the same object.

1. Why DIMACS is not enough

A 9×9 Sudoku in DIMACS is p cnf 729 11988. A 100×100 Sudoku is tens of millions of clauses. But the generator in both cases is ten lines of code. DIMACS discards every bit of that structure the moment it grounds. Modern solvers then spend their life re-discovering symmetry they were never told about.

Symmetry breakers (Shatter, BreakID), lifted input languages (Essence, MiniZinc, ASP), lazy grounding — all of them are trying to claw back, post hoc, the structure that DIMACS threw away. .ncnf is the file format that does not throw it away.

A SAT instance is not a list of clauses. It is a program that emits clauses under an index.

2. What .ncnf brings to the table

1. Compression. Sudoku 100×100 in ~1 KB. PHP(n, n+1) in three lines. Any n. Deterministic expansion.
2. Symmetry for free. The template ∀ i, j: … is the symmetry group. No recovery pass needed.
3. Lifted BCP. One template propagation step absorbs O(n^k) ground steps. Same work, n^k leverage.
4. Exponentially shorter UNSAT proofs. PHP(n, n+1) is 2^Ω(n) in ground resolution (Haken 1985). In .ncnf it is one counting taboo. The proof fits on a napkin.
5. Transfer across sizes. A lifted clause learned on n=9 replays on n=100 without retraining. Ground clauses can never transfer — they reference specific literals. Template clauses reference positions, which exist at every size.
6. Human-readable reasoning. Naked pairs, X-wing, swordfish: these are not heuristics. They are lifted learned clauses that humans discovered by hand. .ncnf lets a solver output them in the same language.

3. The file format (sketch)

p ncnf name=sudoku
param n=9

var x[i:1..n, j:1..n, v:1..n]

# polynomial skeleton (axioms)
∀ i,j:              ∨_v x[i,j,v]                          # a cell has a value
∀ i,j, v<w:          ¬x[i,j,v] ∨ ¬x[i,j,w]                # at most one
∀ i,v, j<k:          ¬x[i,j,v] ∨ ¬x[i,k,v]                # row
∀ j,v, i<k:          ¬x[i,j,v] ∨ ¬x[k,j,v]                # col
∀ br,bc,v, (i1,j1)<(i2,j2) ∈ box(br,bc):
                        ¬x[i1,j1,v] ∨ ¬x[i2,j2,v]              # box

# taboos (learned / asserted)
taboo naked_pair:
  ∀ i, j<k, v<w:
    pair_in_cells(i, {j,k}, {v,w})
    ⇒ ∀ l ∉ {j,k}: ¬x[i,l,v] ∧ ¬x[i,l,w]

# givens
unit x[1,1,5] x[1,2,3] …

Three regions: param, var / skeleton, taboo / unit. A skeleton entry is a quantified clause template. A taboo is a quantified learned clause — a conditional exclusion pattern. Units are ground assertions.

4. PHP(n, n+1) — the catpiss case

p ncnf name=php
param n

var p[i:1..n+1, j:1..n]

∀ i:                ∨_j p[i,j]                           # every pigeon lands
∀ j, i<k:            ¬p[i,j] ∨ ¬p[k,j]                   # hole is exclusive

taboo counting:
  |{ i : ∃j p[i,j] }| = n+1  ∧  |{ j }| = n
  ⇒ ⊥

Three lines. The taboo is the pigeonhole principle. Classical resolution needs 2^Ω(n) ground steps. A lifted solver fires the counting taboo once. The cost of UNSAT drops from exponential to constant.

5. Completion — .ncnf → .ncnf

Closure property. A solver is a transformation from .ncnf to .ncnf. The input describes the problem; the output describes the solution set. Never a single assignment, never just a verdict. Solutions compose because inputs and outputs share the same grammar.

Three solution-shapes, all expressed in the same format:

Completion is a peeling loop that accumulates the output .ncnf and shrinks the residual. Each step is a bounded CNF computation.

solve(ncnf F, budget B, taboo library L) → ncnf F':

  F' ← empty .ncnf with the same (params, vars) as F.
  residual ← F.

  1. PARSE      F → (params, vars, skeleton S, taboos T, units U).
  2. INSTANTIATE  for chosen n: S, T stay lifted. U is ground.
  3. FOR each region R in S ∪ T, by ascending cost:
       a. MATCH    find occurrences of R’s LHS in residual.
       b. REWRITE  apply R’s RHS — lifted BCP. Accumulate any forced
                   ground literals as new unit entries in F'.
       c. DISCHARGE  emit a DIMACS fragment for R under the current
                     partial model and call Kissat with an atom budget.
                     — forced partial witness : append its units to F'.
                     — region has a free parameter : append the residual
                       template (with narrowed index) to F'. No enumeration.
                     — UNSAT locally : a taboo fires — append the
                       taboo to F' and re-enter step 3.
       d. UPDATE    residual ← residual minus the part of R that was
                    discharged. Residual is monotonically shrinking.
  4. GROUND     what remains of residual — the sub-formula not
                covered by any matched template or taboo — to DIMACS.
  5. SWARM      hand the ground residual to /cnf/solve:
                  kissat direct → v6 race → v7 Lambda swarm.
                  The swarm returns a model or a refutation.
  6. LIFT BACK  translate the swarm’s ground result into .ncnf form:
                — SAT model → unit entries in F'.
                — UNSAT certificate → refutation taboo in F'.
  7. INDUCE     scan F' for patterns the inducer can generalize
                (repeated learned clauses → a single lifted taboo).
                Append to the taboo library L for future instances.
  8. RETURN F'.

Every step is accumulative, not enumerative. Step 3c never has to all-SAT a region — it either forces units, keeps the region symbolic, or fires a taboo. The only place enumeration happens is step 5, which is exactly where npdollars already pays dollars. The output F' is always valid .ncnf: you can feed it back into solve and get a fixpoint.

.ncnf moves the polynomial/exponential frontier as far right as the taboo library permits. Everything left of the frontier is compiled into the output .ncnf for free.

6. Complexity budget

The library L is capital. Each dollar spent on a novel instance pays for a taboo that is free for every future instance at every size. PHP(10, 11) is paid once; PHP(100, 101), PHP(1000, 1001) are catpiss ever after.

7. Divide and conquer via pattern recognition

Classical CDCL branching is exponential in the worst case because it splits on variables. .ncnf splits on structure:

residual = full formula
while residual is non-empty:
    find the template region R ∈ (S ∪ T) that matches the largest
    sub-formula of residual at the lowest cost.
    if match found:
        discharge R (lifted BCP or CNF-check)
        residual ← residual − matched
    else:
        break  # genuinely novel structure
swarm(residual)

This is structural divide-and-conquer. Every peel is polynomial. The swarm only ever touches what the library cannot yet explain. The dictionary of LogicSpace is the ground analogue; .ncnf is the lifted analogue.

8. Connection to the monce stack

• AUMA (2023). Every f: {0,1}ⁿ → ℝ has a sparse Fourier decomposition: low-order skeleton plus high-order corrections. .ncnf is the SAT image of that decomposition — polynomial axioms plus pattern-specific taboos.
• Dana Theorem (2024). Every indicator function on a finite discrete domain has a polynomial CNF representation. Taboos are the explicit, portable version of those clauses.
• npdollars. /cnf/solve is the ground engine. /ncnf/solve (future) peels first, hands the residual to /cnf/solve, and imports whatever the swarm learns back as a new lifted taboo.
• auma.aws.monce.ai. polyauma’s Fourier probe already identifies variable-level structure in polynomial budget. The same probe, lifted, is a taboo inducer.

9. What we commit to building

1. .ncnf grammar (params, vars, quantified clauses, taboos, units) — one page of EBNF.
2. Grounder: .ncnf + n → DIMACS. Dogfoods the format against current /cnf/solve.
3. Seed corpus: Sudoku 9×9, 16×16, 25×25; PHP(n, n+1) for n∈{4, 8, 16}; graph coloring k-COL.
4. Template matcher: a lifted unifier between formula fragments and taboo LHS.
5. Taboo library: a versioned, append-only artifact stored next to the session on S3. Every solve exports the taboos it found.
6. POST /ncnf/solve: parse → peel → /cnf/solve on residual → induce taboos → persist.

9*. The flex — sum of a million bits in 1.2 KB

Want to state “the sum of these N binary variables equals target” as a SAT instance? In DIMACS that’s a ripple adder chain: ~7 · N · ⌈log₂(N+1)⌉ clauses, scaling to ~140 million at N=1M. In .ncnf it’s five templates plus a few unit clauses for the target — constant size, independent of N.

p ncnf name=adder_sum
param N=1000000
param B=20

var b[i:1..N]
var s[i:0..N, k:0..B-1]
var c[i:1..N, k:0..B]

∀ k                 :   ¬s[0,k]                           # init s
∀ i                 :   b[i] ↔ c[i,0]                    # init c
∀ i, k              :   s[i,k] = s[i-1,k] XOR c[i,k]       # sum
∀ i, k              :   c[i,k+1] = s[i-1,k] AND c[i,k]     # carry
∀ i                 :   ¬c[i,B]                           # no overflow

unit   s[N,*] = target-in-binary                                 # the goal

A SAT instance over 140 million ground clauses fits in 1.2 KB of .ncnf. It is the same instance — grounding recovers every clause exactly. The scaling laws (measured, EC2, April 2026):

POST /ncnf/adder builds the instance live:

curl -X POST https://npdollars.aws.monce.ai/ncnf/adder \
     -H "Content-Type: application/json" \
     -d '{"N": 10000, "target": 3333, "solve": true}'

→ {"result": "SAT", "kissat_ms": ~260,
     "description.syntactic_bytes_estimate": ~1020,
     "compression_vs_dimacs": ~18000 }

That is the principle of .ncnf in one example: the description stays tiny while the ground formula stays exact. SAT solvers have always paid per clause; .ncnf lets you pay per quantifier.

9a. cnf → ncnf — the inverse arrow

Every flat DIMACS can be lifted into a .ncnf given a schema (variable index layout) and an instance size. The lift is polynomial: O(n_clauses × max_arity × orbit_size), with both arity and orbit size bounded by user-supplied caps.

POST /ncnf/lift
  {"dimacs":        "p cnf 42 133\n1 2 3 4 5 6 0\n…",
   "schema":        [{"name":"p","domains":[[1,7],[1,6]]}],   # optional
   "instance_size": {"n": 6},                                 # optional hint
   "max_arity":     4,
   "budget_ms":     5000,
   "verify_round_trip": true}
      |
      v
  ncnf.lift.cnf_to_ncnf
      1. parse DIMACS
      2. pick schema (given, or infer by factoring n_vars with hint)
      3. decode each clause -> (var, idx, sign) tuples
      4. shape-cluster (arity, (var,sign)*, offsets)
      5. for each shape:
           full orbit present?  -> emit template Clause (∀-quantified)
           partial orbit?       -> emit ground clauses as a taboo
  7. round-trip verifier re-grounds the lifted .ncnf and checks the
     clause set matches the input exactly.

Soundness. A clause template is emitted only when every quantifier-valid instantiation of the shape is already present in the input, so the lifted form grounds back to the exact same clause set. Partial orbits become origin:"lifted:partial" taboos — ground clauses kept as-is, still monotone under the closure property.

Measured lift times (single-threaded Python, MacBook M):

All seven round-trip exactly — grounding the lifted .ncnf reproduces the input clause set byte-for-byte. Pure ∀ problems (PHP) lift to 100% templates; mixed problems with index conditions (GT’s i < j, Sudoku’s box cells) split between templates and ground taboos, but round-trip is preserved.

9b. Benchmark — seven problems, real numbers

Running ncnf.solve on seven instances with kissat 4.0.4 as the ground oracle. Baseline = median kissat on the raw skeleton. Enriched = median kissat on the same skeleton after appending the taboos we induced from one prior UNSAT proof. Transfer = the enriched run on a larger instance of the same family that shares the taboo structure.

MacBook M-series, kissat 4.0.4 Python subprocess, median of 3 runs. Full reproducer at ncnf/bench/run_big.py in the repo. POST /ncnf/solve {"problem": "php", "params": {"n": 8}} returns the live envelope.

Reading the numbers honestly:

• SAT instances (Sudoku, Pythagorean) show ~1× as expected. Induction gives nothing to lift when kissat finds a model without a UNSAT proof. The only cost is a tiny overhead from re-grounding — measured at 3–6% and absorbed in noise. This is the honest null-case.
• UNSAT instances show 2.3× to 642× self-speedup. The induced taboos are the short learned clauses kissat’s DRAT proof exposed — we’re handing the next solver its own breadcrumbs.
• PHP transfers to the next size at 31 583×. The baseline on PHP(12, 13) times out at 60 s. The same instance with PHP(10, 11)’s taboos appended solves in 1.9 ms. This is the whole point of the format: structure learned at n replays at n+k.
• Mutilated chessboard transfers at 224×. 17 lifted taboos from the 10×10 instance make the 12×12 instance catpiss.
• Tseitin and Ordering Principle (both classical theorem-proving benchmarks with exponential resolution lower bounds) transfer at 9× and 4× respectively. Modest for a first-pass inducer, but the direction is right and the taboos count (7, 58) shows the inducer is picking up real structure.

10. The claim

problem → solution-set, in the same grammar.

Charles Dana · Monce SAS · npdollars.aws.monce.ai/ncnf · April 2026
Co-Authored-By: Claude (Anthropic)