By default in MiniZinc there is no declaration of how we want to search for solutions. This leaves the search completely up to the underlying solver. But sometimes, particularly for combinatorial integer problems, we may want to specify how the search should be undertaken. This requires us to communicate to the solver a search strategy. Note that the search strategy is not really part of the model. Indeed it is not required that each solver implements all possible search strategies. MiniZinc uses a consistent approach to communicating extra information to the constraint solver using annotations.
2.5.1. Finite Domain Search¶
Search in a finite domain solver involves examining the remaining possible values of variables and choosing to constrain some variables further. The search then adds a new constraint that restricts the remaining values of the variable (in effect guessing where the solution might lie), and then applies propagation to determine what other values are still possible in solutions. In order to guarantee completeness, the search leaves another choice which is the negation of the new constraint. The search ends either when the finite domain solver detects that all constraints are satisfied, and hence a solution has been found, or that the constraints are unsatisfiable. When unsatisfiability is detected the search must proceed down a different set of choices. Typically finite domain solvers use depth first search where they undo the last choice made and then try to make a new choice.
int: n; array [1..n] of var 1..n: q; % queen in column i is in row q[i] include "alldifferent.mzn"; constraint alldifferent(q); % distinct rows constraint alldifferent([ q[i] + i | i in 1..n]); % distinct diagonals constraint alldifferent([ q[i] - i | i in 1..n]); % upwards+downwards % search solve :: int_search(q, first_fail, indomain_min) satisfy; output [ if fix(q[j]) == i then "Q" else "." endif ++ if j == n then "\n" else "" endif | i,j in 1..n]
A simple example of a finite domain problem is the \(n\) queens
problem which requires that we
place \(n\) queens on an \(n \times n\) chessboard so that none can
q[i] records in which row the queen in column
is placed. The
alldifferent constraints ensure
that no two queens are on the same row, or diagonal.
A typical (partial) search tree
n = 9 is illustrated in Fig. 2.5.1.
We first set
q = 1, this removes values from the domains of other
variables, so that e.g.
q cannot take the values 1 or 2.
We then set
q = 3, this further removes values from the domains
of other variables. We set
q = 5 (its earliest possible value).
The state of the chess board after these three decisions is shown in
Fig. 2.5.2 where the queens indicate the position
of the queens fixed already and
the stars indicate positions where we cannot place a queen
since it would be able to take an already placed queen.
A search strategy determines which choices to make. The decisions we have
made so far follow the simple strategy of picking the
first variable which is not fixed yet, and try to set it to its least
possible value. Following this strategy the next decision would be
q = 7.
An alternate strategy for variable selection is to choose the variable whose
current set of possible values (domain) is smallest.
Under this so called first-fail
variable selection strategy the next decision would be
q = 4.
If we make this decision, then initially propagation removes the additional
values shown in Fig. 2.5.3. But this leaves only one value for
q = 7, so this is forced, but then this leaves only one
possible value for
q, that is 2. Hence a constraint must be
violated. We have detected unsatisfiability, and the solver must backtrack
undoing the last decision
q = 4 and adding its negation
q != 4
(leading us to state (c) in the tree in Fig. 2.5.1)
q = 8. This removes some values from the domain
and then we again reinvoke the search strategy to decide what to do.
Many finite domain searches are defined in this way: choose a variable to constrain further, and then choose how to constrain it further.
2.5.2. Search Annotations¶
Search annotations in MiniZinc
specify how to search in order to find a solution to the
problem. The annotation is attached to the solve item, after the keyword
The search annotation
solve :: int_search(q, first_fail, indomain_min) satisfy;
appears on the solve item. Annotations are attached to parts of
the model using the connector
This search annotation means that we should search by selecting from
the array of integer variables
q, the variable with the smallest
current domain (this is the
first_fail rule), and try setting
it to its smallest possible value
Basic search annotations
There are three basic search annotations corresponding to different basic variable types:
int_search( <variables>, <varchoice>, <constrainchoice> )where
<variables>is a one dimensional array of
<varchoice>is a variable choice annotation discussed below,
<constrainchoice>is a choice of how to constrain a variable, discussed below.
bool_search( <variables>, <varchoice>, <constrainchoice> )where
<variables>is a one dimensional array of
var booland the rest are as above.
set_search( <variables>, <varchoice>, <constrainchoice> )where
<variables>is a one dimensional array of
var set of intand the rest are as above.
float_search( <variables>, <precision>, <varchoice>, <constrainchoice> )where
<variables>is a one dimensional array of
<precision>is a fixed float specifying the \(\epsilon\) below which two float values are considered equal, and the rest are as above.
Example variable choice annotations are:
input_order: choose in order from the array
first_fail: choose the variable with the smallest domain size, and
smallest: choose the variable with the smallest value in its domain.
dom_w_deg: choose the variable with the smallest value of domain size divided by weighted degree, which is the number of times it has been in a constraint that caused failure earlier in the search.
Example ways to constrain a variable are:
indomain_min: assign the variable its smallest domain value,
indomain_median: assign the variable its median domain value (or the smaller of the two middle values in case of an even number of elements in the domain),
indomain_random: assign the variable a random value from its domain, and
indomain_splitbisect the variables domain excluding the upper half.
For backwards compatibility with older version of MiniZinc, the search
annotations can be called with an additional argument that represents the
search strategy to use. The only such strategy that is currently supported is
complete, meaning an exhaustive exploration of the search space. With
the additional argument, an annotation might then look like this:
::int_search(x, input_order, indomain_min, complete).
For a complete list of variable and constraint choice annotations see the FlatZinc specification in the MiniZinc reference documentation.
We can construct more complex search strategies using search constructor annotations. There is only one such annotation at present:
seq_search([ <search-ann>, ..., <search-ann> ])
The sequential search constructor first undertakes the search given by the first annotation in its list, when all variables in this annotation are fixed it undertakes the second search annotation, etc. until all search annotations are complete.
Consider the jobshop scheduling model shown in Listing 2.3.8. We could replace the solve item with
solve :: seq_search([ int_search(s, smallest, indomain_min), int_search([end], input_order, indomain_min)]) minimize end
which tries to set start times
s by choosing the job that can start
earliest and setting it to that time. When all start times are complete
the end time
end may not be fixed. Hence we set it to
its minimal possible value.
Annotations are a first class object in MiniZinc. We can declare new annotations in a model, and declare and assign to annotation variables.
Annotations have a type
You can declare an annotation
parameter (with optional assignment):
ann : <ident>; ann : <ident> = <ann-expr> ;
and assign to an annotation variable just as any other parameter.
Expressions, variable declarations,
solve items can all
be annotated using the
We can declare a new annotation
annotation <annotation-name> ( <arg-def>, ..., <arg-def> ) ;
annotation bitdomain(int:nwords); include "alldifferent.mzn"; int: n; array [1..n] of var 1..n: q :: bitdomain(n div 32 + 1); constraint alldifferent(q) :: domain_propagation; constraint alldifferent([ q[i] + i | i in 1..n]) :: domain_propagation; constraint alldifferent([ q[i] - i | i in 1..n]) :: domain_propagation; ann: search_ann; solve :: search_ann satisfy; output [ if fix(q[j]) == i then "Q" else "." endif ++ if j == n then "\n" else "" endif | i,j in 1..n]
The program in Listing 2.5.2 illustrates the use of annotation
declarations, annotations and annotation variables.
We declare a new annotation
bitdomain which is meant to tell
the solver that variables domains should be represented via bit arrays
The annotation is attached to the declarations of the variables
Each of the
alldifferent constraints is annotated with
the built in annotation
which instructs the solver to use
the domain propagating version of
alldifferent if it has one.
An annotation variable
search_ann is declared and used
to define the search strategy. We can give the value to the search
strategy in a separate data file.
Example search annotations might be the following (where we imagine each line is in a separate data file)
search_ann = int_search(q, input_order, indomain_min); search_ann = int_search(q, input_order, indomain_median); search_ann = int_search(q, first_fail, indomain_min); search_ann = int_search(q, first_fail, indomain_median); search_ann = int_search(q, input_order, indomain_random);
The first just tries the queens in order setting them to the minimum value, the second tries the queens variables in order, but sets them to their median value, the third tries the queen variable with smallest domain and sets it to the minimum value, and the final strategy tries the queens variable with smallest domain setting it to its median value.
Different search strategies can make a significant difference in how easy it is to find solutions. A small comparison of the number of failures made to find the first solution of the n-queens problems using the 5 different search strategies is shown in the table below (where — means more than 100,000 failures). Clearly the right search strategy can make a significant difference, and variables selection is more important than value selection, except that for this problem random value selection is very powerful.
Any kind of depth first search for solving optimization problems suffers from the problem that wrong decisions made at the top of the search tree can take an exponential amount of search to undo. One common way to ameliorate this problem is to restart the search from the top thus having a chance to make different decisions.
MiniZinc includes annotations to control restart behaviour. These annotations, like other search annotations, are attached to the solve item of the model.
Restart search annotations
The different restart annotations control how frequently a restart occurs. Restarts occur when a limit in nodes is reached, where search returns to the top of the search tree and begins again. The possibilities are
<scale>is an integer defining after how many nodes to restart.
<scale>is an integer defining the initial number of nodes before the first restart. The second restart gets twice as many nodes, the third gets three times, etc.
<base>is a float and
<scale>is an integer. The
kth restart has a node limit of
<scale> * <base>^k.
<scale>is an integer. The
kth restart gets
<scale>*L[k]where :mzn`L[k]` is the
kth number in the Luby sequence. The Luby sequence looks like 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 …, that is it repeats two copies of the sequence ending in
2^ibefore adding the number
restart_nonedon’t apply any restart (useful for setting a
annparameter that controls restart).
If two or more restart annotations are used, the solver’s behaviour is undefined.
Restart search is much more robust in finding solutions, since it can avoid getting stuck in a non-productive area of the search. Note that restart search does not make much sense if the underlying search strategy does not do something different the next time it starts at the top. For example the search annotation
solve :: int_search(q, input_order, indomain_min); :: restart_linear(1000) satisfy
does not make very much sense since the underlying search is deterministic and each restart will just redo the same search as the previous search. Some solvers record the parts of the search tree that have already been searched and avoid them. This will mean deterministic restarts will simply effectively continue the search from the previous position. This gives no benefit to restarts, whose aim is to change decisions high in the search tree.
The simplest way to ensure that something is different in each restart
is to use some randomization, either in variable choice or value choice.
Alternatively some variable selection strategies make use of information
gathered from earlier search and hence will give different behaviour, for
2.5.5. Warm Starts¶
In many cases when solving an optimization or satisfaction problem we may have solved a previous version of the problem which is very similar. In this case it can be advantageous to use the previous solution found when searching for solution to the new problem. This is currently supported by some MIP backends.
The warm start annotations are attached to the solve item, just like other search annotations.
Warm start search annotations
Warm start annotations are used to indicate a (potentially partial or even invalid) starting point for solvers which support them.
<vars>is a one dimensional array of integer variables, and
<vals>is a one dimensional array of integer of the same length giving the warm start values for each integer variable in
<vars>is a one dimensional array of float variables, and
<vals>is a one dimensional array of floats of the same length giving the warm start values for each float variable in
<vars>is a one dimensional array of Boolean variables, and
<vals>is a one dimensional array of Booleans of the same length giving the warm start values for each Boolean variable in
<vars>is a one dimensional array of set variables, and
<vals>is a one dimensional array of sets of integers of the same length giving the warm start values for each set variable in
The warm_start_array annotation takes a list of warm_start annotations and can be used to specify an ordering of the warm starts which is maintained in the FlatZinc.
The warm start annotation can be used by the solver as part of value selection. For example, if the selected
v[i] has in its current domain the warm start value
w[i] then this is
the value selected for the variable. If not the solver uses the existing value selection rule
applicable to that variable.
The order of warm_starts, relative to other search annotations, can be
important (especially for CP), so they all might need to be put into a seq_search as below:
array[1..3] of var 0..10: x; array[1..3] of var 0.0..10.5: xf; var bool: b; array[1..3] of var set of 5..9: xs; constraint b+sum(x)==1; constraint b+sum(xf)==2.4; constraint 5==sum( [ card(xs[i]) | i in index_set(xs) ] ); solve :: warm_start_array( [ %%% Can be on the upper level warm_start( x, [<>,8,4] ), %%% Use <> for missing values warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ), warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) ) ] ) :: seq_search( [ warm_start_array( [ %%% Now included in seq_search to keep order warm_start( x, [<>,5,2] ), %%% Repeated warm_starts allowed but not specified warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ), warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) ) ] ), warm_start( [b], [true] ), int_search(x, first_fail, indomain_min) ] ) minimize x + b + xf + card( xs intersect xs );
If you’d like to provide a most complete warmstart information, please provide values for all variables which are output when there is no output item or when compiled with --output-mode dzn.