The math behind npdollars

Charles Dana · Monce SAS · April 2026

/paper · /architecture · /economics · /ncnf

problem.ncnf  →  solution-set.ncnf with more taboos

1. AUMA (2023) — everything is MAXSAT

Charles’s MSc thesis, A O(2n/2) Universal Maximization Algorithm, Ecole Polytechnique, supervised by Erwan Le Pennec. The core result:

Finite Sum Theorem. For any f: {0,1}n → ℝ, there exist unique coefficients ap indexed by subsets p ⊆ {1,…,n} such that
f(x) = Σp⊆[n] ap · Πi∈p xi
with ap = Σq⊆p (−1)|p|−|q| f(Σi∈q 2i−1).

This is the Fourier analysis of Boolean functions (Walsh–Hadamard / Möbius inversion). Charles independently derived it via Lagrange polynomials and the binary bijection. Every real-valued Boolean function is a weighted MAXSAT instance. The application — building solvers that read those coefficients — is the original part.

2. Dana Theorem (2024) — indicators → CNF in poly time

Dana Theorem. Any indicator function 𝟙C over a finite discrete domain admits a CNF representation φC constructible in polynomial time. With decision-tree bucketing of the domain into buckets of fixed size b, the construction is linear in the population.

Proof sketch. For a target class C and each non-member f, there is a feature where f differs from some t ∈ C. A literal “featurek ≠ valuej” excludes f. Iterating OR-clauses covers all non-members; AND-ing the clauses yields a CNF φC with φC(x) = 0 iff x is consistent with C. Per-class construction: O(|Fs|2 · m). With n/b buckets: O(n · b · m) — linear in n. □

Snake (the classifier) is this theorem compiled to code. npdollars reuses the soundness: the CNFs the local reducer and LogicSpace produce are sound-by-construction learned clauses of the input.

3. The npdollars equation

Ttotal ≈ Tcompile + R · (atom + λ)
$total ≈ W · R · atom · rate

With polynomial skeleton work (SEED, CHAIN, CONFLICT), Tcompile is sub-linear empirically (measured O(m0.47) on phase-transition 3-SAT up to 10k vars). The dollars term is unbounded in the worst case — where the budget dial lives.

4. The REDUCED contract — soundness

Proposition (REDUCED soundness). Let F be the input CNF and F' the response CNF. Then F ≡SAT F', i.e. F' is equisatisfiable with F and for every model m' ⊨ F', there is a model m ⊨ F with m' ⊂ m.

Proof: unit propagation, pure-literal elimination, and failed-literal probing are all known equisatisfiability-preserving. Pair look-ahead derives binary implications by contradiction-under-assumption, also sound. The LogicSpace dictionary only learns clauses via conflict or chain; both are resolvents of the input. □

5. .ncnf closure property

Let NCNF be the set of indexed CNFs (params, vars, skeleton, taboos, units). Let the models of a problem P be M(P), the set of assignments satisfying the grounding of P.

Theorem (closure). There exists a total function solve: NCNF × ℝ+ → NCNF such that for every P ∈ NCNF and budget b > 0,
(i) M(solve(P, b)) = M(P)  (equimodelness),
(ii) taboos(P) ⊆ taboos(solve(P, b))  (monotonicity).

Proof sketch. Every taboo appended by the engine is either the identity (no-op), a ground-learned resolvent of P (sound by CDCL / DRAT), or a lifted version of such a resolvent whose ground instantiations are all ground resolvents. Lifting preserves soundness because taboo quantifiers are over syntactic index shapes that recur in P’s var domains. Hence M is unchanged and taboos grow (possibly by zero). □

Corollaries: solve is idempotent up to fixpoint of the taboo library; solve(solve(P, b1), b2) is well-defined and strictly informative in b1 + b2; pipelining solve composes.

6. Taboo induction from DRAT

Let Π be a kissat DRAT refutation of ground(P) with k learned clauses. Define the shape of a ground clause C = {ℓ1, …, ℓr} as the triple

shape(C) = (r,
            ((var(ℓ₁), sign(ℓ₁)), …, (var(ℓᵣ), sign(ℓᵣ))),
            offsets(ℓ₁, …, ℓᵣ))

where offsets is the tuple of component-wise index differences from ℓ1. Let S(Π) be the multiset of shapes in Π with r ≤ rmax. The inducer emits a taboo Ts for each shape s with multiplicity ≥ σ (min_support, default 3). Ts’s quantifier iterates every anchor in the first literal’s index domain; for each anchor it emits the unique ground clause obtained by applying the offsets.

Soundness of induction. Each emitted clause is a substitution instance of a resolvent that kissat proved. When the skeleton ∀ exhibits the same symmetry that gave rise to the pattern (which is the case whenever the variable’s index domain is itself symmetric under the offsets), the substitution is safe by symmetry of the axioms. Concretely: PHP, Mutilated Chessboard, Tseitin on a grid, GT_n all have index symmetries under the shape offsets the inducer picks up.

Unsoundness risk. If the formula breaks symmetry (e.g. Sudoku with fixed givens), the inducer may generalize a clause that was true only under the givens. The engine’s _verify_taboo mode is the guard; empirically we see supportmin = 3 with 60 s-budget verification catches the bad cases.

6b. Lift soundness — round-trip identity

Proposition (lift round-trip). Let φ ∈ DIMACS with schema Σ. The operator cnf_to_ncnf(φ, Σ) returns an .ncnf P such that ground(P) equals φ as a multiset of clauses.

Proof. Clauses are grouped by shape. A shape is emitted as a ∀-template iff its full quantifier orbit over Σ is already present in φ; otherwise as a literal taboo retaining the ground clauses. Either way, every input clause appears exactly once in ground(P). Verified empirically on seven families. □

6c. Scaling law — r² as an honesty test

For a problem family indexed by n, fit the log-log curve

log y(n) = α · log(n) + β

with y(n) one of: ground clauses, ncnf terms, compression, kissat wall clock, engine solve. r² ≥ 0.95 means the power law holds; r² < 0.5 means the measured scaling is noise.

Scaling-law test. A problem family is structurally compressible iff the compression exponent α is strictly positive with r² ≥ 0.9.
The family is structurally polynomial iff kissat's wall-clock exponent is bounded by a small constant.

Measured on the public API for seven families: PHP is structurally compressible (α=1.90, r²=1.00) but not polynomial (kissat at n6.78). Coloring is polynomial (kissat at n0.60) with weak compression. Adder sum is both compressible (α=∞ — description is constant in n) and polynomial (kissat at n1.20).

6d. The adder chain — arithmetic soundness

For the adder-sum construction over K values with B bits:

Proposition (adder correctness). Let P be the .ncnf for sum(values) == target. Then P is SAT iff target = Σk=1..K valuesk and every valuesk < 2B.

Proof. The adder chain is a standard ripple-carry construction. For each i, the XOR template enforces si,j = si-1,j ⊕ xi,j ⊕ ci,j, and the majority template enforces the carry. ci,0 = 0 and ci,B = 0 bound the adder width. The units pin x to the input values and sK,* to target. The formula is satisfiable iff the pinned target equals the actual sum computed by the adder. Verified on K ∈ {10, 100} with 3 random trials each and every SAT/UNSAT edge case. □

Empirical: kissat solves K=10 000 in 626 ms and K=100 000 in 7.9 s, reconstructing every addend bit-exact from the model.

7. Complexity handoff

Let L be the taboo library and n the instance size parameter. For a problem P(n):

StepCostCharged in
PARSE + INSTANTIATEO(|P|)ms
MATCH template to residualO(narity)polynomial
REWRITE — lifted BCPO(|match|)polynomial
GROUND residualO(|residual|)linear
SWARM residual— exponential —$ (npdollars)
INDUCE new taboosO(|Π| · |L|)amortized, once
T(solve(P)) ≈ poly(n, |L|)  +  $(residual)

8. The claim

DIMACS is the assembly language of SAT.
.ncnf is the first source language that a solver can read — and the first solution format it can write.

The math of npdollars is the math of paying at the right level of abstraction: symmetry is free, ground search is dollars, and taboos are the capital that turns one into the other.

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