Solvers, certificates, and export

This chapter covers what surrounds an extraction: the solvers and their limits, the number range of each solver, certificates, listing the terms of a cost band, and the two JSON files Semper writes. It ends with the alternatives considered and the limits. Examples run from doc/book/examples/cost-models/; those in its manual/ directory need RoundingSat or end in an error, so the book test does not run them.

Solvers

:solver chooses how the problem is solved. The default is internal.

Cycles in the e-graph are excluded by Semper for every solver. An ASP model with a solver other than asp, a MiniZinc model with a solver other than minizinc, and a minizinc solver with any other model are sort errors naming the model (The extract command).

The internal solvers on the ladder program’s problem:

(sort IntervalSort) (function Interval (i64 i64) IntervalSort) (sort MLTL) (function Var (String) MLTL) (function And (MLTL) MLTL :assoc-comm-idem) (function Global (IntervalSort MLTL) MLTL) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (extract e :cost memory :rung splits :solver internal) (extract e :cost memory :rung splits :solver dpw) (extract e :cost memory :solver greedy)

; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 39 greedy at rung selection
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))

dpw sums its weights in 64 bits. An objective whose weights total more is refused with an error that names internal and roundingsat, which are exact.

roundingsat is looked up as $ROUNDINGSAT, then ~/.local/bin/roundingsat, then on the PATH, and run with --print-sol=1 --verbosity=0. (opb "prog" ...) runs prog with the given arguments and the OPB file’s path appended. The program must print competition output: s OPTIMUM FOUND or s UNSATISFIABLE, and v lines.

A script also runs on clingo, as its formula written as ASP:

(sort IntervalSort) (function Interval (i64 i64) IntervalSort) (sort MLTL) (function Var (String) MLTL) (function And (MLTL) MLTL :assoc-comm-idem) (function Global (IntervalSort MLTL) MLTL) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (extract e :cost memory :rung splits :solver (asp “clingo”))

; cost 37 proved at rung splits (1 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

This backend is slower. On 64 of the MLTL specifications of Johannsen and Rozier (FMCAD 2026), clingo took 15 times longer than the internal solver on the median instance. That measurement was recorded by a tool since removed from the repository, and the current tree does not reproduce it.

Limits on a solve

A limit that runs out after a term was found gives the status bounded. One that runs out before gives the error no term: Bounded.

Keeping the solver’s input

Each variable names an existing directory, in which Semper keeps a copy of every file it gives a solver, numbered call000, call001, and so on:

Number ranges

Semper’s own arithmetic on costs is exact: a script’s IBig and UBig, a Rust cost’s integers, the terms, the objective, the totalizer that bounds it, and the reported cost. Two ranges then decide whether a cost is computed correctly. The first is an optional cap, which Semper enforces. The second is the range of the solver, which Semper enforces on every number it writes for that solver.

The cost width. --cost-bits big (the default) sets no cap. --cost-bits 32 or 64 caps every integer of a script or Rust cost, and the reported cost of any model, at that signed width. A value outside the cap is an error naming the operation, never a wrapped value. This script charges 2^63:

#![allow(unused)]
fn main() {
// 2^62 doubled is 2^63, one past the largest signed 64-bit integer.
fn cost(g: Graph) {
    g.constant(4611686018427387904).scale(2).charge();
}
}

(sort E) (function V (String) E) (let e (V “a”))

(cost-model big :script “28-cost-bits.roto”) (extract e :cost big)

Run from manual/ with no flag, it prints:

; cost 9223372036854775808 proved at rung selection (1 solves, 0 cycle exclusions)
(V "a")

With --cost-bits 64, it stops with:

error: check failed: extract :cost: the cost script's build failed: scale: the value 9223372036854775808 is outside the 64-bit cost range (--cost-bits)

A Roto literal is still 64-bit, because Roto has no larger integer type. A larger constant is written as g.ibig_str("…") (Exact integers).

The solver’s range. Each solver reads integers in its own representation, and several read a value past it wrongly without reporting anything. Before a solver runs, Semper checks every number it writes for that solver against the solver’s range, and refuses one outside it with an error naming the solver. The numbers checked are the coefficients, bounds, and weights of an OPB file or an ASP program, and the integers and multiplicities of the ASP and MiniZinc dumps. A weight of 3,000,000,000 is exact on the internal solver and refused for clingo:

#![allow(unused)]
fn main() {
// A weight of 3,000,000,000: exact for Semper, past clingo's 32-bit integers.
fn cost(g: Graph) {
    g.root().chosen().charge_if(3000000000);
}
}

(sort E) (function V (String) E) (let e (V “a”))

(cost-model heavy :script “28-solver-range.roto”) (extract e :cost heavy) (extract e :cost heavy :solver (asp “clingo”))

; cost 3000000000 proved at rung selection (2 solves, 0 cycle exclusions)
(V "a")
error: check failed: extract :cost: the cost script's build failed: an objective weight 3000000000 is outside clingo's 32-bit integers

A payload integer past clingo’s range, under an ASP model, is refused the same way, and the message says what Semper does not check:

(sort E) (function Num (i64) E) (let e (Num 3000000000))

(cost-model size :asp “../26-first.lp”) (extract e :cost size :solver (asp “clingo”))

error: check failed: extract :cost: the integer of node 0 (Num) 3000000000 is outside clingo's 32-bit integers. Semper checks the numbers it writes for the solver; an overflow inside your ASP or MiniZinc criteria is not checked, and is yours to rule out

What Semper does not check. ASP and MiniZinc criteria compute inside the solver. A criteria file that computes a value its solver cannot represent, such as a #sum past 2^31 in clingo, a product past 2^31 in Chuffed, or a sum past 2^53 in a MIP solver, can give a wrong optimum, and nothing reports it. If you write cost functions that can overflow the solver’s internal number representation, you are on your own. Keep the values your criteria compute inside the range of the solver you run them on, or choose a solver whose range holds them.

What each solver does with a number past its range, measured on 2026-10-06 with the inputs in egraph/tests/data/solver_width/ (the README names the solver versions):

Semper recognizes an OPB solver by its program name: one containing roundingsat is unbounded, one containing clasp or clingo is 32-bit. A MiniZinc solver named chuffed or gecode is 32-bit; coin, cbc, highs, scip, gurobi, cplex, xpress, or mip is exact to 2^53; any other is 64-bit.

Recommended. For costs that can grow large, state the cost in Rust or as a script using IBig and UBig, and solve on internal or roundingsat, the two solvers that take numbers of any size. For MiniZinc criteria use cp-sat, whose 64-bit range the MiniZinc compiler also checks. Use clasp, clingo, Chuffed, Gecode, and the MIP solvers only when every value the criteria compute stays inside their range.

Certificates

:proof "dir" runs a proof-logging pseudo-Boolean solver with --proof-log, RoundingSat’s flag, and keeps each call’s instance and proof in dir, as call000.opb and call000.pbp, and so on. It prints the claim of the final call and the command that checks it. :proof needs :solver roundingsat or (opb ...):

(sort IntervalSort) (function Interval (i64 i64) IntervalSort) (sort MLTL) (function Var (String) MLTL) (function And (MLTL) MLTL :assoc-comm-idem) (function Global (IntervalSort MLTL) MLTL) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “../memory.roto”) (extract e :cost memory :solver roundingsat :proof “proofs”) (extract e :cost memory :rung splits :solver (opb “roundingsat” “–print-sol=1”) :proof “proofs-splits”)

; cost 39 proved at rung selection (0 solves, 0 cycle exclusions)
; certificate Bounds { lower: 38 }: veripb proofs/call000.opb proofs/call000.pbp
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; certificate Bounds { lower: 36 }: veripb proofs-splits/call000.opb proofs-splits/call000.pbp
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

VeriPB checks the first certificate:

Running VeriPB version 3.0.2
Info: Switched to proof version 2.0 (it is recommended to migrate to proof version 3.0).
s VERIFIED BOUNDS 38 <= obj <= 38

The bound is on the objective in the OPB file, which leaves out the cost’s constant part (here the specification wrapper’s 1): the certified cost is 39, the selection optimum, and 37 at splits. The claim is Bounds { lower: L } when the final call found an optimum, and Unsat { below: ... } when it refuted a cheaper term. The certificate covers the solver’s reasoning on the final instance: no model has a lower objective. That every acyclic term has a model whose objective is its cost is a property of the encodings, established by Semper’s tests rather than by the certificate.

Listing terms in a cost band

:band lo hi lists the terms whose cost lies in [lo, hi], at most :count n of them (default 10), instead of the cheapest one. Both bounds are added to the objective before solving, and each term found is excluded by its rung literals, so no term in the band is lost and none is listed twice. A band runs on the internal solver, with a script or Rust model; any other :solver is a sort error. The second command below asks for splits under a budget of 10 clauses, which steps down:

(sort IntervalSort) (function Interval (i64 i64) IntervalSort) (sort MLTL) (function Var (String) MLTL) (function And (MLTL) MLTL :assoc-comm-idem) (function Global (IntervalSort MLTL) MLTL) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) ; Every term whose cost lies in [37, 40], at most 4 of them. (extract e :cost memory :rung splits :band 37 40 :count 4) ; A budget of 10 clauses is below the splits encoding: the rung steps down. (extract e :cost memory :rung splits :budget 10)

; 4 terms with cost in [37, 40] at rung splits
; cost 37 in band at rung splits
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 39 in band at rung splits
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 40 in band at rung splits
(And (And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0"))) (Global 0 9 (Var "a0")))
; cost 40 in band at rung splits
(And (And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Global 0 9 (Var "a0")))
; cost 39 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))

The terms come by increasing cost, then by their text, each with its cost; the order the solver finds them in depends on its version and platform. Standard error carries warning: rung splits estimated above the budget; extracting at selection. With the optimum proved, a band gives equivalent terms at a known gap above it: benchmarks with known answers, variants for differential testing, and pairs of suboptimal and optimal terms.

Writing the term

:file "f.json" writes the extracted term as JSON. It has one entry per class of the term, named c and the class’s number in the extraction graph, with its operator, its children’s entries, and its payload. A multiset node also carries "mults", each child’s count, parallel to "children": a child of multiplicity k is listed once. Under :band, each term goes to f.json.0.json, f.json.1.json, and so on.

(sort IntervalSort) (function Interval (i64 i64) IntervalSort) (sort MLTL) (function Var (String) MLTL) (function And (MLTL) MLTL :assoc-comm-idem) (function Global (IntervalSort MLTL) MLTL) (let e (And (Global (Interval 0 9) (Var “a0”)) (Global (Interval 1 4) (Var “a1”)))) (cost-model memory :script “memory.roto”) (extract e :cost memory :file “28-file.json”)

(sort E) (function V (String) E) (function Plus (E) E :assoc-comm) (let p (Plus (V “a”):2 (V “b”))) (cost-model dag :script “24-first.roto”) (extract p :cost dag :file “28-file-mults.json”)

; cost 18 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 3 proved at rung selection (2 solves, 0 cycle exclusions)
(Plus (V "a"):2 (V "b"))

The first file, 28-file.json:

{
  "nodes": {
    "c0": {
      "children": [
        "c3"
      ],
      "ints": [
        1,
        4
      ],
      "op": "Global",
      "strings": []
    },
    "c1": {
      "children": [
        "c4"
      ],
      "ints": [
        0,
        9
      ],
      "op": "Global",
      "strings": []
    },
    "c2": {
      "children": [
        "c0",
        "c1"
      ],
      "ints": [],
      "op": "And",
      "strings": []
    },
    "c3": {
      "children": [],
      "ints": [],
      "op": "Var",
      "strings": [
        "a1"
      ]
    },
    "c4": {
      "children": [],
      "ints": [],
      "op": "Var",
      "strings": [
        "a0"
      ]
    }
  },
  "root": "c2"
}

The second, 28-file-mults.json, with the count of (V "a"):

{
  "nodes": {
    "c4": {
      "children": [],
      "ints": [],
      "op": "V",
      "strings": [
        "b"
      ]
    },
    "c6": {
      "children": [],
      "ints": [],
      "op": "V",
      "strings": [
        "a"
      ]
    },
    "c7": {
      "children": [
        "c4",
        "c6"
      ],
      "ints": [],
      "mults": [
        1,
        2
      ],
      "op": "Plus",
      "strings": []
    }
  },
  "root": "c7"
}

The exported e-graph

(dump-egraph t :file "f.json") writes the whole e-graph, marking t’s class as the root, for a tool that extracts outside Semper. The format is egglog’s --to-json, plus a colour per class and the kind of each operator:

(sort E) (function a () E) (function b () E) (function F (E) E) (function Plus (E) E :assoc-comm) (let p (Plus (F a) (F a) b)) (dump-egraph p :file “28-dump-egraph.json”)

{
 "nodes": {
  "n0e3163c6ae86c6765650b5b783c0b759-E": {"op": "Plus", "children": ["n0f1448134acd95981b3931e16014521c-E", "nd5ec398aba3e06fa32d7228d5a59cd00-E"], "mults": [2, 1], "eclass": "E-823989c50677dc443bbb3b68e0b57913", "cost": 1, "subsumed": false},
  "n0f1448134acd95981b3931e16014521c-E": {"op": "F", "children": ["n986a608e2ec286cfc5a691e55b30a36f-E"], "eclass": "E-4d6895f531715b14080654f7417251f5", "cost": 1, "subsumed": false},
  "n986a608e2ec286cfc5a691e55b30a36f-E": {"op": "a", "children": [], "eclass": "E-4c4de7d182b2ab841f1155f98333ff02", "cost": 1, "subsumed": false},
  "nd5ec398aba3e06fa32d7228d5a59cd00-E": {"op": "b", "children": [], "eclass": "E-4e661d73fc43b09769cade26489d3916", "cost": 1, "subsumed": false}
 },
 "class_data": {
  "E-4c4de7d182b2ab841f1155f98333ff02": {"type": "E", "colour": "4c4de7d182b2ab841f1155f98333ff02"},
  "E-4d6895f531715b14080654f7417251f5": {"type": "E", "colour": "4d6895f531715b14080654f7417251f5"},
  "E-4e661d73fc43b09769cade26489d3916": {"type": "E", "colour": "4e661d73fc43b09769cade26489d3916"},
  "E-823989c50677dc443bbb3b68e0b57913": {"type": "E", "colour": "823989c50677dc443bbb3b68e0b57913"}
 },
 "op_kinds": {
  "F": "plain",
  "Plus": "ac",
  "a": "plain",
  "b": "plain"
 },
 "root_eclasses": ["E-823989c50677dc443bbb3b68e0b57913"]
}

Every name is a content colour: a hash of the class’s structure, computed by refining over the classes until the partition stops changing. A class is {sort}-{colour} and a node n{colour}-{sort}. Nodes and classes are written in name order, and an AC, ACI, or commutative node’s children in name order too. Two runs that build the same e-graph therefore write the same bytes, whatever node ids they allocated: on the 1,172 MLTL specifications Johannsen and Rozier publish with their FMCAD 2026 paper (Chapter 24), naive and semi-naive saturation write identical dumps. A child entry names one member of the child class, the one whose name sorts first; a consumer reads that member’s eclass. A multiset child of multiplicity k is written once, with k in "mults", parallel to "children", as F under Plus above (count 2). A congruent duplicate node is omitted. op_kinds (plain, comm, a, ac, aci, or lit) tells a consumer which operators’ child order carries no meaning. The design chapter on extraction defines the colouring.

Alternatives considered

• Choosing the nodes, then the grouping. An earlier extractor proved the optimum of the flat cost, with every AC node flat, and then chose each node’s grouping. Sequencing the two is not optimal: on 600 instances of the monitor memory problem it is above the joint optimum on 130 (21.7%), by up to 31% (egraph/tests/ex_paper_claims.rs). The loss comes from the choice among flat optima: the best grouping over every flat optimum reaches the joint optimum on all 600. The splits rung chooses both in one encoding.
• A separate extractor over the dump. That extractor read the exported JSON and took its candidates in the order of the dump’s node names, which were node ids. Its result then depended on the order rules were applied in: naive and semi-naive saturation built the same e-graph on all of those 1,172 specifications, and their extracted terms differed on 50. Extraction now runs inside Semper, and the dump’s names are content colours.
• Breaking ties by a second objective. Making equal-cost terms distinct by a lexicographic second cost changes every benchmark’s encoding and optimality proof, and a rank sum is not a total order on terms. Ties are instead resolved by content: the export orders by colour, and the greedy extractor breaks a cost tie by term height and then by node colour.

The design chapter records the others.

Limits

• A script has no resource bound: it can loop, exhaust memory, or overflow the stack, since Roto compiles to native code without an instruction count.
• Costs are exact, within the cap --cost-bits sets if any, and within the range of the solver they are exported to; what ASP and MiniZinc criteria compute inside the solver is the solver’s arithmetic (Number ranges).
• Roto’s own i64/u64 operators wrap and its division by zero aborts, so a cost script that uses +, -, *, /, or % is refused when the program is checked; scripts compute with the exact methods of IBig, UBig, and the encoded integers (Exact integers).
• Deciding the binary grouping of a flat node with ten or more operands can take CaDiCaL an hour or more.
• A recursive attribute keeps every value it can take per class. A cap can be set through the Rust API (Build::set_attribute_cap); reaching it is an error, never a smaller domain.
• Script, criteria, :file, and :proof paths are relative to the working directory, not to the program file.
• Clingo and MiniZinc run with no time limit from Semper unless the solver’s own arguments set one.