Status: Superseded by ADR-270 — its D1-D11 are D9, D10, D11, D5, D12-D18 there, its D12 is D8
Amended by: ADR-268 — the search is free: D7’s checkpoints, D8’s result cache and lemma rule, D11’s parallel rules and D12’s criteria resting on them give way to a committed nikaia.proofs that every build reads and --locked compares
Date: October 2, 2026
Answers: the owner’s question how the solver ADR-265
provides for becomes a universal one that is fast by the world’s measure, not
only for the queries the compiler asks today — and what has to be decided
before any algorithm is built: the workload, the representation, the numbers,
the proof format, the search skeleton, theory combination, the strategy layer,
the database, the memory layout and the measuring rod
Supersedes: ADR-265 D8 in its order only: the engine is
built in Rust behind interfaces made for the port, and the port (D8 step 4)
follows this record’s step 3 (D12) instead of preceding the further theories
Related: ADR-265 D1-D7 (three layers; terms by u32 id;
self-contained queries; an answer depends on the query and a budget counted
in work, never on time or threads; a certificate makes a solver usable
without trusting it; SMT-LIB and Alethe at the edge), ADR-264
D9-D10 (what the prover asks), ADR-252 (no i128 in the
language), ADR-009 (SIMD lives behind std, a SWAR baseline
first), ADR-021 (a build is keyed on content),
ADR-257 D3 (a representation is chosen by measuring),
ADR-258 (the four weights). The method and every table behind
the numbers here: docs/solver-workload.md
ADR-265 cut the prover into a frontend, a logic and a solver, and fixed what a query and an answer are. The solver behind it is Fourier-Motzkin with integer tightening and case splitting on demand: right for nearly every query the compiler asks (D1 names the ones it misses), and exponential in the number of variables and in the disjunctions a proof needs. The goal is a solver that wins the QF_LIA division of SMT-LIB against z3 and cvc5 and then widens, written so that it can become Nikaia, and parallel where Nikaia is strong.
Which architecture is that solver built on, and what is decided before the first algorithm — so that each later engine is a part that fits, and not a rewrite?
Two conditions are fixed and not weighed here: ADR-265 D4 holds everywhere (deterministic, a budget counted in work, never time), and the checker stays small: every strategy, engine and theory produces the same proof format.
| Solver | Its answer | What it costs there | Source |
|---|---|---|---|
| z3 | CDCL(T); a general simplex over rationals with bound propagation for arithmetic (Dutertre and de Moura), branch-and-bound, Gomory and GCD cuts for integers; model-based theory combination; tactics composed into strategies, some with time limits; rationals with a small-integer fast path | Answers can depend on the time limits of tactics; parallel mode is a portfolio whose result depends on timing; proofs exist but are not the default and are not small | from memory, not checked |
| cvc5 | CDCL(T); simplex with a “theory of linear arithmetic” that switches between several solvers; theory combination by a care graph; proofs in Alethe, LFSC and its own format, checked by external checkers | A proof checker for every rule it can emit is large; proof production costs a measurable factor | from memory, not checked |
| Yices 2 | CDCL(T) with a fast simplex for linear arithmetic, MCSAT for non-linear arithmetic | No proofs; MCSAT is a second search architecture | from memory, not checked |
| MathSAT 5, SMTInterpol | CDCL(T); for integers branch-and-cut, “cuts from proofs” (Dillig, Dillig and Aiken, CAV 2009) and Diophantine equality handling | Interpolation drives the design; SMTInterpol is on the JVM | from memory, not checked |
| Kissat, CaDiCaL (SAT) | Clause arena with 32-bit references, blocking literals in watch lists, binary clauses held apart, inprocessing, mode switching (focused / stable) at conflict counts; LRAT proofs from CaDiCaL | Not an SMT solver; the techniques are the floor for the Boolean core | from memory, not checked |
| Mallob, Painless (parallel SAT) | Clause sharing between many solver instances, portfolio and divide-and-conquer | Results and run time depend on timing; not reproducible by construction | from memory, not checked |
| Local search for LIA (Cai et al., CAV 2022) | Critical moves over integer assignments find models fast on satisfiable instances | Proves nothing unsat; complements CDCL(T) | from memory, not checked |
What does not transfer:
nikaia-logic has no dependencies
(ADR-265 D1): the big numbers are its own.The ten points are decided in §4, each with its rejected alternatives. Here the one choice that frames the others: the search architecture.
What is built today. Exact, certificates are Farkas combinations by construction. Its elimination grows doubly exponentially in the variables; the measurement (§4 D1) shows the cost already on twelve.
The structure every leading SMT solver shares. The Boolean search learns from conflicts; the simplex is incremental and backtracks by restoring bounds, not by recomputing; a conflict’s explanation is a row, which is a Farkas certificate.
Model-constructing search assigns theory variables as decisions. Strong for non-linear arithmetic; for linear integer arithmetic it does not beat B, and its proofs are less settled.
Fast today. A dependency (ADR-265 D1), a time-based answer (D4), and no road to a solver in Nikaia.
| D1 the special case pays | D2 the compiler works | D3 no cost for the common case | D4 consistent | If it is wrong | |
|---|---|---|---|---|---|
| A | No: one hard query with many variables costs the build | Yes | Yes for tiny queries | Yes | The hard queries stay unknown: a check at run time, not a wrong answer |
| B | Yes: work goes where conflicts are | Yes | Only with a fast path (D5): a CDCL(T) set-up costs more than a 2-atom query | Yes: one proof format | A rewrite of the engine, not of the interfaces |
| C | Yes | Yes | Same as B | Two architectures if B is still needed for proofs | A second skeleton beside B |
| D | Yes | Yes | No: about 1.5 ms per query through z3’s API, several hundred times today’s solver | No: time decides | Undoing a dependency |
B is chosen. A lost on D1, C on D4 for linear arithmetic (kept for non-linear arithmetic, §6), D on D3 and D4.
The queries are those the prover asks while the compiler’s test suite runs,
dumped as SMT-LIB and replayed in-process against an instrumented copy of the
solver; the stress set adds four families the suite does not reach (guards,
unrelated disjunctions, +1 or +2 paths, parity). Method, machine and every
table: docs/solver-workload.md.
Two sets: the 353 recorded queries every solver change has been replayed against since 0.0.357, and all 1 697 queries the compiler’s test suite asks at 0.0.368.
| per query | 353: median | p90 | p99 | max | 1 697: median | p90 | p99 | max |
|---|---|---|---|---|---|---|---|---|
| variables | 1 | 2 | 3 | 4 | 1 | 3 | 3 | 4 |
atoms lin <= 0 |
2 | 8 | 10 | 12 | 2 | 5 | 8 | 12 |
| disjunctions | 0 | 1 | 3 | 3 | 0 | 1 | 2 | 3 |
| branches searched | 1 | 3 | 5 | 5 | 1 | 2 | 3 | 5 |
| solve time, µs | 2.8 | 13.5 | 22.4 | 34.7 | 2.6 | 8.3 | 15.5 | 34.0 |
x - y). Every coefficient is 1 or
nikaia lower on examples/calc and 6 % on examples/inventory, before
rustc has run at all.blank = 2·n, blank = 1). 56 of
them are provable: Fourier-Motzkin eliminates n over the rationals and
loses the parity of 2·n. The other 36 are satisfiable, and
back-substitution lands on x = 1/2. z3 agrees with every answer that was
given..nika tools contain no
assert today.What the numbers decide: the compiler’s workload is tiny and almost all intervals, so it decides the fast paths and the rule that the common case pays nothing (D5, D9); it does not decide the core, which is sized by SMT-LIB (D10). Two of the owner’s build steps are weighed against them in D12.
Rejected: designing from the benchmark literature alone (the compiler’s queries would pay a general engine’s set-up on every one of them); designing from the compiler’s queries alone (four variables decide nothing about a core that has to win QF_LIA).
u32; rows are sparse; small problems run dense.A variable, a term, a clause and a literal are u32 indices into arenas
(ADR-265 D2). A row - an atom, a tableau row, a derived bound - is sparse:
two parallel arrays, column indices (u32, ascending) and coefficients
(D3’s numbers). A query whose variables fit one vector register - eight or
fewer; every one of the 1 697 the compiler asked has at most four - runs on
a dense kernel
of fixed width instead, chosen by the strategy layer (D7), not by the engine.
Why sparse is the representation: the compiler’s atoms hold 1.05 non-zeros each; the stress set’s chains hold two of 33 variables (6 %); SMT-LIB’s linear problems are sparse by construction (from memory, not checked: tableau densities of a few per cent are typical). A dense row of a problem with ten thousand variables would be all zeros and all bandwidth.
Why a dense kernel at all: below eight variables the bookkeeping of a
sparse row (indices, merge on combination) costs more than the arithmetic,
and eight i64 lanes are one AVX-512 register or two AVX2 ones (D9).
Rejected: dense everywhere (fails every large problem); BTreeMap<String,
i64> as today (each combination compares strings; it is what makes
Fourier-Motzkin’s 60 % above); a hash map per row (iteration order would have
to be fixed by hand for D4, and it is slower than a sorted merge at these
sizes).
i64 fast path, and a deterministic fall-back to big integers and fractions.Σ aⱼxⱼ / d), so the inner
loop is integer multiply-add; the row is reduced by its gcd after a pivot.i64 while it fits in 32 bits,
so one product fits 63 bits and one combination a·x + b·y cannot overflow;
the result is checked against the 32-bit range, and a coefficient that
leaves it promotes that one number to a big integer. Promotion is a
function of the values, so it happens at the same operation on every run
and every machine: D4 holds without a rule of its own.u32 limbs with u64 products, which
Nikaia can express (ADR-252 keeps i128 out). A number is a tagged word:
small inline, or a u32 reference into a big-number arena (D9). A
52-bit-limb kernel using the multiply-add instructions of AVX-512 IFMA is a
kernel behind the same type (ADR-009), not a second representation.δ for strict bounds (Dutertre and de Moura).Rejected: i64 only (ADR-265 D2 today: a proof lost to overflow is a
check at run time, acceptable for the compiler, not for SMT-LIB); i128
(ADR-252); floating point with exact repair (fast LP solvers do it, but every
answer and certificate must be exact anyway, and keeping IEEE results equal
across targets with fused multiply-add is a constraint on every kernel for a
gain the measurement has not shown); full rationals everywhere (a gcd per
operation in the inner loop).
A proved answer’s certificate is one proof log, append-only, that every engine and strategy writes into. Its steps:
¬a₁ ∨ … ∨ ¬aₖ justified
by a Farkas combination of the atoms’ bounds: non-negative multipliers
for inequalities, any sign for equalities, rational multipliers (written
as integers over one common denominator), ending in 0 < 0 or c <= 0
with c > 0; strict bounds carry their strictness.Tighten.L <= k ∨ L >= k + 1 for an integer form L with
integer coefficients and an integer k: valid by itself, checked by
looking at L and k. Branch-and-bound is a split and a resolution.q defined by
0 <= L - m·q <= m - 1 for an integer form L and an integer m > 0:
q is the floor of L / m, which exists for every value of L, so the
definition cannot make a satisfiable problem unsatisfiable. SMT-LIB’s
div and mod by a constant are exactly this, and it is what keeps some
proofs short: twelve numbers that are each -1 or 1 never sum to 1,
which splits take 2¹² cases to show and which q = ⌊(x + 1) / 2⌋ per
number, a two-case lemma each (x + 1 - 2q = 0) and one rounding show in
linear size.Which cuts are allowed: every cut that is a Chvátal-Gomory derivation (a combination and a rounding) - Gomory’s fractional cuts, the GCD test on an equality, Hermite-normal-form cuts on equality rows - and every split cut (a cut valid on both sides of a split: Gomory mixed-integer, mixed-integer rounding, lift-and-project, cuts from proofs), written as the split, one derivation per side and the resolution. A heuristic may find a cut by any means, floating point included; it is written as one of these, exactly, or it is not used.
Small means: the checker replays, it never searches. Its rules are the
five above plus one per further theory (D6), each a replay; the checker for
linear integer arithmetic and clauses stays under 1 500 lines, and a rule
that would push it past needs a record. Alethe (ADR-265 D6) stays an export:
each step above has an Alethe counterpart (resolution, la_generic with
integer strengthening), which is how the format is checked by a checker this
crate did not write.
Rejected: extension with arbitrary definitions (a definition that is not satisfiable for every value would be unsound; the floor is the one form needed and the one that is always satisfiable); Alethe as the internal format (a large rule set, ADR-265 D5); a certificate per engine (one checker per engine is not small); no certificate for cuts, trusting the cut generator (the most error-prone code of an integer solver would be trusted).
The search is a CDCL loop over Boolean literals - decisions, unit propagation, conflict analysis to a first-UIP clause, backjumping, restarts, clause-database reduction - and every theory sits behind one interface:
| call | what it does |
|---|---|
assert(lit) |
a literal became true at the current level; the theory takes its bound or equality, and may answer with a conflict at once (two bounds that cross) |
propagate() |
literals the theory implies cheaply (bound propagation), each explained later on demand |
check(final: bool, budget) |
consistency of what is asserted: consistent, a conflict (a clause and its certificate step), or lemmas to add (a split, a cut) |
explain(lit) |
the clause and certificate step behind a literal it propagated |
backtrack(level) |
forget what was asserted above level; the simplex keeps its basis and restores bounds |
model() |
values that satisfy what is asserted, checked by evaluation (ADR-265 D3) |
shared() |
the terms and equalities it shares with other theories (D6) |
The simplex is built against this interface from its first line: general simplex with bounds on variables, one slack variable per distinct linear form (atoms on the same form share it), pivoting by a deterministic rule with Bland’s rule as the fall-back that guarantees termination.
Fast paths are the same interface, cheaper: a query with no Boolean choice skips the CDCL loop; interval atoms (68 % of the compiler’s queries hold nothing else) are decided by bounds on single variables; difference atoms (a further 15 %) by negative-cycle detection, whose certificate is the cycle - a Farkas sum with every multiplier one. Fourier-Motzkin stays as the cross-check (every answer of the new engine is compared with it on everything it can decide) and as an engine the strategy may pick for tiny dense problems (D7). No fast path allocates for a query below the dense width: the common case pays nothing for the skeleton (ADR-258 D3).
Rejected: CDCL as a later step (the simplex would be built against Fourier-Motzkin’s interface and rebuilt); offline DPLL - enumerate Boolean models, ask the theory each (exponential in the disjunctions, as the case splitting before 0.0.368 was); MCSAT as the skeleton (§3, C).
The architecture takes further theories - equality with uninterpreted functions, bit-vectors, arrays - by one procedure, decided now although only linear integer arithmetic is built first:
Rejected: Nelson-Oppen with eager equality propagation (needs convex, stably infinite theories, which bit-vectors and integers are not); Shostak (needs canonisers and solvers per theory); a care graph as cvc5 builds it (a refinement of the same idea, open to measurement later, not a different architecture).
A strategy chooses before the start and switches during the search; it is not inside an engine:
Rejected: strategies inside the engines (no engine could be measured alone, and none could be replaced); a strategy that reads the clock (D4); user-written tactic scripts (a language to maintain for a choice the features already make).
Measured: 105 of the 1 697 queries are distinct up to renaming, so a result cache would answer more than nine in ten in the test suite - an upper bound, because the suite compiles similar programs many times. A hit saves today’s solve (4.2 µs on average) minus the re-check (1.9 µs for a certificate): for the compiler’s queries the cache is worth little per query, and it is built for the hard ones and for SMT-LIB runs, where one hit saves seconds.
Rejected: a lemma store written during builds (the answer would depend on build order); a cache trusted without re-checking (a stale or corrupt entry would drop a check).
u32 words: a header (size, flags, the
learned clause’s glue) followed by the literals; a clause reference is a
u32 word index. Literals are u32 (variable << 1 | sign).std with a SWAR baseline and multiversioning per target (ADR-009). The
same split holds after the port to Nikaia.Rejected: pointer-based clauses (Box, Rc: twice the memory and no
compaction); hashing with a random seed anywhere (iteration order would vary
between runs; a fixed seed is the rule).
Rejected: measuring on the compiler’s queries alone (they are 4 µs each, D1); comparing at different machines or with time-limited strategies on our side.
Parallel across queries is a fixed partition by index with answers in index order. Cube-and-conquer splits by a deterministic look-ahead and combines by a fixed rule (proved when every cube is; refuted by the first refuted cube by index). Clause sharing happens only at epochs fixed by work counts. These are ADR-265 D4’s rules; this record adds only that the strategy layer’s checkpoints (D7) and the epochs are the same points, so that a switch and a share never interleave differently.
| Step | What | Measured by |
|---|---|---|
| 1 | u32 variables and sparse rows (D2), the numbers of D3, the proof steps of D4 and their checker, the theory interface of D5 - with Fourier-Motzkin moved behind it, and equalities eliminated exactly before it |
The 92 unknown queries of D1 answered (56 proved, 36 refuted); every other recorded, suite and stress query answered as today, every certificate checks, z3 agrees; the overflow test answered instead of unknown; the compiler’s queries no slower (today 4.2 µs to solve, mean over the 1 697, and 1.9 µs to check a certificate, mean over the 649 proved); big numbers agree with an independent implementation on randomised operations; the checker under 1 500 lines |
| 2 | Parallel across queries (D11), the result cache (D8), the features and measurements (D7, D8) | Answers and certificates identical at 1 and n threads; on a batch of SMT-LIB-sized queries a speed-up of at least 0.7 × threads; no slow-down on the compiler’s batch (work below a threshold stays on one thread); a cache hit equals recomputation, byte for byte |
| 3 | The CDCL(T) core with the simplex as its first theory; preprocessing; interval and difference fast paths (D5) | All of step 1’s sets; the compiler’s queries at or under step 1’s time; on QF_LIA, the solved count against z3’s and cvc5’s on the same machine is recorded, and every proved checks |
| 4 | Cuts (D4’s forms), local search for models, the strategy layer (D7) | Parity with twelve variables proved in linear size (D4’s extension, a two-case lemma per variable, one rounding); on QF_LIA, more solved than z3 and cvc5 single-threaded, then a lower PAR-2; the strategy beats the best single configuration on a held-out half of the set |
| 5 | Cube-and-conquer and clause sharing at epochs (D11) | Answers identical at every thread count; on QF_LIA’s hard unsatisfiable instances, solved count and PAR-2 against z3 and cvc5 in their parallel modes |
Where this differs from the order the owner gave, and why:
u32 indices, no Rc, no trait objects in inner loops, u32
limbs). Porting first would port Fourier-Motzkin. The port needs one thing
the language does not have: arithmetic that reports overflow instead of
aborting (§6).nikaia-logic’s certificate type changes again in step 1 (the proof log of
D4); verify keeps its signature. The Alethe export follows each step.checked_add and its kin, or
a wider multiply - which the port needs; a language record.Real sort in terms and in the SMT-LIB reader, for QF_LRA, and
whether δ-rationals are a number type of the crate or of the simplex
alone.push/pop): ADR-265 D3 keeps queries
self-contained; whether the solver offers an incremental interface for
SMT-LIB’s incremental track is decided when that track is a goal.