10.55.4 Annotations

10.55.4.1 Solve Annotations

Following are the currently supported solve annotations:

bool_search(array[int] of var bool: x, ann: a1, ann: a2, ann: a3)

int_search(array[int] of var int: x, ann: a1, ann: a2, ann: a3)

seq_search(array[int] of ann: s)

restart_constant(int: scale)   since release 4.10.0

restart_geometric(float: base, int: scale)   since release 4.10.0

restart_linear(int: scale)   since release 4.10.0

restart_luby(int: scale)   since release 4.10.0

relax_and_reconstruct(array[int] of var int: x, int: p)   since release 4.10.0

Described in the MiniZinc documentation.

lex_minimize(array[int] of var int: x)   since release 4.10.0

lex_maximize(array[int] of var int: x)   since release 4.10.0

An annotation of this form supersedes any solve objective (satisfy, minimize expr, or maximize expr) with a lexicographic minimize or maximize objective, as described in Enumeration Predicates.

pareto_minimize(array[int] of var int: x)   since release 4.10.0

pareto_maximize(array[int] of var int: x)   since release 4.10.0

An annotation of this form supersedes any solve objective (satisfy, minimize expr, or maximize expr) with a Pareto minimize or maximize objective, as described in Enumeration Predicates.

To illustrate how lexicographic and Pareto objectives work, suppose you have a model with variables x to minimize and y to maximize. One way to express that is with the objective minimize x - y:

include "globals.mzn";

var 0..10: x;
var 0..10: y;

constraint y <= x+5;
constraint y <= 15-x;

solve minimize x-y;

Let’s run it:

$ minizinc --solver sicstus demo.mzn 
x = 0;
y = 5;
----------
==========

Another way to express it is to minimize x, breaking ties by maximizing y, i.e., by lexicographic minimization. Let’s change the solve statement to:

solve :: lex_minimize([x,-y]) satisfy;

and rerun:

$ minizinc --solver sicstus demo.mzn 
x = 0;
y = 5;
----------
==========

The solution was the same, but that is not generally the case for less trivial models. Let’s investigate what happens if we swap the priorities, i.e., maximize y, breaking ties by minimizing x:

solve :: lex_maximize([y,-x]) satisfy;

where satisfy is superseded but required for syntax correctness, and rerun:

$ minizinc --solver sicstus demo.mzn 
x = 5;
y = 10;
----------
==========

Finally, let’s investigate the relation between the two objectives by collecting the set of solutions where no solution is dominated (x is not smaller and y is not greater) by another solution. Such a set of solutions is known as a Pareto front.

solve :: pareto_minimize([x,-y]) satisfy;

where satisfy is superseded but required for syntax correctness, and rerun:

$ minizinc --solver sicstus demo.mzn 
x = 5;
y = 10;
----------
x = 4;
y = 9;
----------
x = 3;
y = 8;
----------
x = 2;
y = 7;
----------
x = 1;
y = 6;
----------
x = 0;
y = 5;
----------
==========

Variables not included in any solve or is_defined_var annotation are labeled with a default heuristic that corresponds to labeling/2 of library(clpfd) with the option list [dom_w_deg,bisect].

Heuristics that involve randomization depend on a random seed. The seed is the same in each run, meaning that the same sequence of values will be tried in each run. This behavior can be changed by setting a specific random seed using clpfd:fd_setrand/1.

10.55.4.2 Constraint Annotations

Constraint annotations of the form domain, bounds, and value are recognized by the FlatZinc interpreter. Any other constraint annotation is ignored.

10.55.4.3 Variable Annotations

The following variable annotations are recognized. Any other variable annotation is ignored:

output_var   since release 4.2

the variable may be written on the current output stream.

output_array   since release 4.2

the variable array may be written on the current output stream.

is_defined_var

the variable will not be considered in any default labeling (such as when the search annotations do not include all variables)