Criteria in MiniZinc

A :minizinc cost model is a MiniZinc file: a criterion over arrays and variables that describe the e-graph. This chapter shows how to write one, lists every name Semper defines, and compares the solvers. Every example runs from doc/book/examples/cost-models/ and needs minizinc on the PATH.

How Semper runs a criterion

(extract t :cost m :solver (minizinc "cp-sat")) runs four steps:

1. Semper numbers the classes reachable from t 1..C and their candidates 1..N. It writes the e-graph as data, and the chosen rung as variables and constraints whose solutions are the candidate terms.
2. It appends the criterion file and runs MiniZinc with the named solver. Integers stay integer variables: nothing is order-encoded before the solver sees them.
3. It decodes the last solution into a term.
4. It solves a second time with that term fixed, and reports the objective on it (The reported cost).

Every auxiliary variable is determined by the term, so each term is one solution. The model itself excludes cyclic terms through rank, so the first line of the output reports 0 solves and 0 cycle exclusions. A MiniZinc model runs only with a (minizinc ...) solver, and a (minizinc ...) solver only with a MiniZinc model; any other pairing is a sort error.

A first criterion

The criterion of the first example of Chapter 24, in MiniZinc:

% Every picked node is paid once: `Twice` 3, every other operator 1.
array[1..N] of int: price = [if op[n] = "Twice" then 3 else 1 endif | n in 1..N];
var int: cost = sum(n in 1..N)(price[n] * bool2int(pick[n]));
solve minimize cost;

op[n] is node n’s operator, a string, and pick[n] is the variable that is true when the term takes node n for its class. The file declares its own names, here price and cost, and ends with one solve minimize item.

(sort E) (function V (String) E) (function F (E) E) (function Add (E E) E) (function Twice (E) E) (rewrite (Twice x) (Add x x))

(let e (Twice (F (F (V “a”))))) (run 1)

(cost-model dag :minizinc “27-first.mzn”) (extract e :cost dag :solver (minizinc “cp-sat”))

; cost 4 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 4
(Add (F (F (V "a"))) (F (F (V "a"))))

The cost is 4, as in Roto and in ASP. The second line is the solver’s lower bound on the objective. On a run stopped by a time limit, the bound tells how far the reported term can be from the optimum.

The data Semper writes

For the program above, at the selection rung, Semper writes this data before its variables, its constraints, and the criterion:

% The e-graph.
int: C = 4;
int: N = 5;
int: B = 0;
int: MAXK = 2;
int: MAXL = 1;
int: MAXJ = 1;
int: ROOT = 4;
int: PLAIN = 0; int: COMM = 1; int: SEQ = 2; int: SEQ_LEFT = 3; int: SEQ_RIGHT = 4; int: MSET = 5; int: SET = 6;
array[1..C] of int: class_id = [0, 1, 2, 3];
array[1..N] of int: node_id = [3, 0, 4, 1, 2];
array[1..N] of 1..C: cls = [1, 2, 3, 4, 4];
array[1..N] of string: op = ["V", "F", "F", "Add", "Twice"];
array[1..N] of int: kind = [0, 0, 0, 0, 0];
array[1..N] of set of 1..C: kids = [{}, {1}, {2}, {3}, {3}];
array[1..N] of int: nkid = [0, 1, 1, 2, 1];
array[1..N, 1..MAXK] of 0..C: kid = [| 0, 0 | 1, 0 | 2, 0 | 3, 3 | 3, 0 |];
array[1..N, 1..MAXK] of int: kmult = [| 0, 0 | 1, 0 | 1, 0 | 1, 1 | 1, 0 |];
function int: mult(int: n, int: k) = sum(i in 1..nkid[n])(if kid[n, i] = k then kmult[n, i] else 0 endif);
array[1..N] of int: nint = [0, 0, 0, 0, 0];
array[1..N, 1..MAXJ] of int: ints = [| 0 | 0 | 0 | 0 | 0 |];
array[1..C] of 1..N: first = [1, 2, 3, 4];
array[1..N] of int: nleaf = [0, 1, 1, 1, 1];
array[1..N, 1..MAXL] of 0..C: leaf = [| 0 | 1 | 2 | 3 | 3 |];
% 0 no tree, 1 chains, 2 trees, 3 binary trees, 4 ordered trees, 5 a fold.
array[1..N] of int: family = [0, 0, 0, 0, 0];
array[1..B] of 1..N: bnode = [];
array[1..B] of bool: interval = [];
array[1..B] of int: blo = [];
array[1..B] of int: bhi = [];

Node 4, Add, has two children, both class 3: kid and kmult list both positions, and kids holds the class once. The names, with n a node, c a class, and b a block:

The payload is integers only: unlike the ASP facts’ str, no string payload is written.

The variables

Blocks exist only for a bracketed node with 3 to 16 leaves (8 at orders for an AC node) at a tree rung, and for a fold at every rung. depth[n, p] is defined for every node n and every p in 1..MAXL; it is 1 for every leaf of a node with no blocks.

Names a criterion must not redefine

The dump also defines the function children and the predicates meet and within. A criterion must not redefine them, nor declare any name of the two tables above; MiniZinc then stops with an error, such as an ambiguous call for a second meet. A parameter-only predicate that an int function uses is declared with test, not predicate, as bounded is in A larger criterion.

Trees

The depth cost of Chapter 25 in MiniZinc:

% The depth of the deepest leaf of any picked node, a leaf directly under its node
% at depth 1.
var 0..MAXL: deepest;
constraint forall(n in 1..N, p in 1..nleaf[n])(pick[n] -> deepest >= depth[n, p]);
solve minimize deepest;

(sort E) (function V (String) E) (function And (E) E :assoc-comm) (let e (And (V “a”) (V “b”) (V “c”) (V “d”)))

(cost-model depth :minizinc “27-depth.mzn”) (extract e :cost depth :rung selection :solver (minizinc “cp-sat”)) (extract e :cost depth :rung levels :solver (minizinc “cp-sat”)) (extract e :cost depth :rung binary :solver (minizinc “cp-sat”))

; cost 1 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 1
(And (V "a") (V "b") (V "c") (V "d"))
; cost 1 proved at rung levels (0 solves, 0 cycle exclusions)
; solver lower bound 1
(And (V "a") (V "b") (V "c") (V "d"))
; cost 2 proved at rung binary (0 solves, 0 cycle exclusions)
; solver lower bound 2
(And (And (V "a") (V "c")) (And (V "b") (V "d")))

The costs are 1, 1, and 2, as in Roto and in ASP. At binary the term differs: CP-SAT returns (And (And a c) (And b d)), where the internal solver and clingo return (And (And a b) (And c d)). Both cost 2. Among terms of equal cost, each solver returns the one it finds, and the reported cost is the same.

A larger criterion

The MLTL monitor memory in MiniZinc:

test bounded(int: n) = (op[n] = "Global" \/ op[n] = "Future" \/ op[n] = "Until" \/ op[n] = "Release") /\ nint[n] >= 2;
function int: lb(int: n) = if bounded(n) then max(ints[n, 1], 0) else 0 endif;
function int: ub(int: n) = if bounded(n) then max(ints[n, 2], 0) else 0 endif;
int: TOP = sum(n in 1..N)(ub(n) + lb(n));

% Worst- and best-case propagation delays over the chosen term.
array[1..C] of var 0..TOP: wpd;
array[1..C] of var 0..TOP: bpd;
constraint forall(n in 1..N)(pick[n] -> wpd[cls[n]] = ub(n) + max([0] ++ [wpd[k] | k in kids[n]]));
constraint forall(n in 1..N)(pick[n] -> bpd[cls[n]] = lb(n) + if card(kids[n]) = 0 then 0 else min([bpd[k] | k in kids[n]]) endif);

predicate counted(int: c) = used[c] /\ op[first[c]] != "Bool";
predicate sibling(int: n, int: p, int: q) =
    parent_leaf[n, p] = 0 \/ exists(b in 1..B where bnode[b] = n)(parent_leaf[n, p] = b /\ bmem[b, q]);

array[1..C] of var 0..TOP: queue;
constraint forall(n in 1..N, p, q in 1..nleaf[n] where p != q)(
    (pick[n] /\ sibling(n, p, q) /\ op[first[leaf[n, p]]] != "Bool") -> queue[leaf[n, p]] >= wpd[leaf[n, q]] - bpd[leaf[n, p]]);

% An internal node's queue: its latest outside sibling less its earliest member.
array[1..B] of var 0..TOP: own;
constraint forall(b in 1..B)(own[b] = min([TOP] ++ [if bmem[b, p] then bpd[leaf[bnode[b], p]] else TOP endif | p in 1..nleaf[bnode[b]]]));
array[1..B] of var 0..TOP: iqueue;
constraint forall(b in 1..B, q in 1..nleaf[bnode[b]])(
    (inner[b] /\ not bmem[b, q] /\ (parent_blk[b] = 0 \/ exists(b2 in 1..B where bnode[b2] = bnode[b])(parent_blk[b] = b2 /\ bmem[b2, q])))
    -> iqueue[b] >= wpd[leaf[bnode[b], q]] - own[b]);

var int: cost = 1 + sum(c in 1..C)(bool2int(counted(c))) + sum(c in 1..C)(queue[c])
    + sum(b in 1..B)(bool2int(inner[b])) + sum(b in 1..B)(iqueue[b]);
solve minimize cost;

Each attribute is an array of variables with an explicit domain, 0..TOP, where TOP bounds every delay of an acyclic term. A constraint under pick[n] -> ... defines a node’s value only where the term takes it.

(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 :minizinc “memory.mzn”) (extract e :cost memory :rung selection :solver (minizinc “cp-sat”)) (extract e :cost memory :rung splits :solver (minizinc “cp-sat”))

; cost 39 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 39
(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)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

Choosing a solver

(minizinc "SOLVER" "ARG" ...) runs minizinc --solver SOLVER ARG ... --output-mode json --output-objective -s -i FILE. SOLVER is any name minizinc --solvers lists, such as cp-sat, chuffed, gecode, highs, or coin-bc. Semper sets no time limit; pass MiniZinc’s own, in milliseconds, as an argument:

(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 :minizinc “memory.mzn”) (extract e :cost memory :rung splits :solver (minizinc “chuffed”)) (extract e :cost memory :rung splits :solver (minizinc “gecode”)) (extract e :cost memory :rung splits :solver (minizinc “highs”)) (extract e :cost memory :rung splits :solver (minizinc “coin-bc”)) ; A time limit in milliseconds, passed to minizinc after the solver’s name. (extract e :cost memory :rung splits :solver (minizinc “cp-sat” “–time-limit” “60000”))

; cost 37 proved at rung splits (0 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 (0 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 (0 solves, 0 cycle exclusions)
; solver lower bound 37
(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 (0 solves, 0 cycle exclusions)
; solver lower bound 37
(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 (0 solves, 0 cycle exclusions)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

Every solver proves 37 at splits. HiGHS, COIN-BC, and CP-SAT report a lower bound; Chuffed and Gecode do not, and print no bound line. When a solve stops before it proves its optimum, the status is bounded, and the bound, when printed, limits the distance to the optimum.

Each solver reads integers in its own range, and Semper checks the integers it writes, the payload and the multiplicities, against the range of the named solver: 32 bits for Chuffed and Gecode, exact to 2^53 for the MIP solvers, 64 bits for CP-SAT and any other. The values the criterion computes are the solver’s arithmetic, which Semper does not check. If you write cost functions that can overflow the solver’s internal number representation, you are on your own. CP-SAT, whose 64-bit range the MiniZinc compiler also checks, is the recommended solver for criteria whose values can grow (Number ranges).

EXTRACT_API_KEEP_MZN=dir keeps every model MiniZinc is given in dir, as call000.mzn, call001.mzn, and so on: two per extraction. The directory must exist. egraph/tests/mltl/costs/ holds the three MLTL costs in MiniZinc. The mzn.rs source holds the constraints Semper writes.