2.6. Search

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.6.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.

Listing 2.6.1 Model for n-queens (nqueens.mzn). ▶

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 attack another. The variable q[i] records in which row the queen in column i is placed. The alldifferent constraints ensure that no two queens are on the same row, or diagonal. A typical (partial) search tree for n = 9 is illustrated in Fig. 2.6.1. We first set q[1] = 1, this removes values from the domains of other variables, so that e.g. q[2] cannot take the values 1 or 2. We then set q[2] = 3, this further removes values from the domains of other variables. We set q[3] = 5 (its earliest possible value). The state of the chess board after these three decisions is shown in Fig. 2.6.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.

Fig. 2.6.1 Partial search trees for 9 queens

Fig. 2.6.2 The state after the addition of q[1] = 1, q[2] = 4, q[3] = 5

Fig. 2.6.3 The initial propagation on adding further q[6] = 4

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[4] = 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[6] = 4. If we make this decision, then initially propagation removes the additional values shown in Fig. 2.6.3. But this leaves only one value for q[8], q[8] = 7, so this is forced, but then this leaves only one possible value for q[7] and q[9], that is 2. Hence a constraint must be violated. We have detected unsatisfiability, and the solver must backtrack undoing the last decision q[6] = 4 and adding its negation q[6] != 4 (leading us to state (c) in the tree in Fig. 2.6.1) which forces q[6] = 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.6.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 solve. 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 (indomain_min value selection).

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 var int, <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 bool and the rest are as above.
set_search( <variables>, <varchoice>, <constrainchoice> ) where <variables> is a one dimensional array of var set of int and the rest are as above.
float_search( <variables>, <precision>, <varchoice>, <constrainchoice> ) where <variables> is a one dimensional array of var float, <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_split bisect 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.9. 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.

2.6.3. Annotations

Annotations are a first class object in MiniZinc. We can declare new annotations in a model, and declare and assign to annotation variables.

Annotations

Annotations have a type ann. 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, and solve items can all be annotated using the :: operator.

We can declare a new annotation using the annotation item:

annotation <annotation-name> ( <arg-def>, ..., <arg-def> ) ;

Listing 2.6.2 Annotated model for n-queens (nqueens-ann.mzn). ▶

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.6.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 of size nwords. The annotation is attached to the declarations of the variables q. Each of the alldifferent constraints is annotated with the built in annotation domain_propagation 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.

n	input-min	input-median	ff-min	ff-median	input-random
10	22	2	5	0	6
15	191	4	4	12	39
20	20511	32	27	16	2
25	2212	345	51	25	2
30	—	137	22	66	9
35	—	1722	52	12	12
40	—	—	16	44	2
45	—	—	41	18	6

2.6.4. Restart

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

restart_constant(<scale>) where <scale> is an integer defining after how many nodes to restart.
restart_linear(<scale>) where <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.
restart_geometric(<base>,<scale>) where <base> is a float and <scale> is an integer. The k th restart has a node limit of <scale> * <base>^k.
restart_luby(<scale>) where <scale> is an integer. The k th restart gets <scale>*L[k] where :mzn`L[k]` is the k th 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^i before adding the number 2^{i+1}.
restart_none don’t apply any restart (useful for setting a ann parameter 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 example dom_w_deg.

2.6.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.

warm_start(<vars>,<vals>) where <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>.
warm_start(<vars>,<vals>) where <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>.
warm_start(<vars>,<vals>) where <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>.
warm_start(<vars>,<vals>) where <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 <vars>.

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 variable 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[1] + b + xf[2] + card( xs[1] intersect xs[3] );

If you’d like to provide a most complete warm start information, please provide values for all variables which are output when there is no output item or when compiled with --output-mode dzn.