Here we describe the MiniSearch language and how to write your own search.
Also have a look at the MiniSearch examples or at
our MiniSearch paper.
MiniSearch is a high level meta-search language based on MiniZinc 2.0 with
special built-ins for specifying the search. All MiniSearch built-ins are
typed as functions returning annotations. Semantically, however, every
MiniSearch built-in returns a value that represents either `success' or
`failure', with respect to finding a solution.
The table below shows
all MiniSearch builtins in alphabetical order. Below we will discuss the different
built-ins or 'combinators' in more detail.
A Starting Example: Formulating Branch-and-Bound Search
Let's start with a simple example: formulating Branch-And-Bound Search (BAB). In BAB,
after each found solution, we post a constraint on the objective variable to assure that
the next solution has a better objective value than the currently found solution.
include "minisearch.mzn";
var int: obj; % other variables and constraints not shown
solve search min_bab(obj);
output ["Objective: "++show(obj)];
function ann: min_bab(var int: obj) =
repeat (
if next() then
commit() /\ print() /\ post(obj < sol(obj) )
else break endif
);
|
The first few lines outline the basic MiniZinc model (where we omit constraints and further variables for
simplicity). We include the minisearch.mzn
library and call our user-defined MiniSearch
function min_bab
in line 3, using the new search keyword.
The second part defines the MiniSearch function min_bab
.
The specification can be read as follows: repeatedly try to find the next solution; and if that is successful,
commit to the solution, print it and add the constraint that the objective must have a lower value
than the current solution. If unsuccessful, break out of the repeat.
Have a look at the Golomb Ruler example with a user-defined branch-and-bound search: golomb_mybab.mzn. You can run this example as it is with MiniSearch.
Built-ins involving the solver
Communication with the solver is restricted to three forms: invoking the solver (to find a new solution), adding constraints/variables to the model, and when creating scopes for temporary variables and constraints.
Invoking the solver with next()
The MiniSearch instruction for finding the next solution is next()
.
It is successful if a solution has been found, and fails otherwise.
The variable/value labelling strategy for the CP tree search (such as first-fail on the smallest domain value)
can be set by annotating the solve
item (as in standard MiniZinc). This sets the labelling
globally, for every call to next()
.
Adding constraints with post()
Constraints are added by calling the post (c)
built-in with a constraint c
as argument.
Constraints can be formulated using the same MiniZinc constructs as in the model, which includes global
constraints, user-defined functions and predicates.
NOTE: In the current beta implementation it is recommended to put all constraints into one call of post. This
means, it is preferred to write post (c1 /\ c2)
instead of post(c1) /\ post(c2)
.
Adding local variables
Variables can be dynamically added during search too, using the MiniZinc let
construct.
This construct can be used for adding both constants/parameters as well as decision variables.
The example below demonstrates how to add local constants and decision variables.
function ann: my_search(int: N) =
let {
int: i = 0; % adding a local constant
array[1..N] of var 1..N: x; % adding a local variable array
} in (
repeat (
i := i + 1 /\ % change the value of the constant
post(alldifferent(x)) /\ % post a constraint on local variables
% some other search
)
);
|
NOTE: In the current beta implementation we recommend to use 1-dimensional arrays instead of
multi-dimensional arrays, because there are still some problems with the latter.
Search scopes
Search scopes define the lifespan of constraints and variables in the model. MiniSearch has an implicit
global search scope that contains all variables and constraints of the model. A new search scope can be
created by using the scope(s)
built-in that takes a MiniSearch specification s
as an argument. When entering a scope, search is assumed to start from the root again. This means that
in the example below, both calls of next will return the same solution.
function ann: my_search() =
next() /\ print() /\ % prints first solution in search space
scope ( % opens a new search scope where search starts at root
next() /\ print() % prints first solution in search space
)
/\
next() /\ print() /\ % prints second solution in search space
|
Whenever the execution leaves a search scope, all constraints and variables that were added in the
scope are removed from the model and the solver. Execution in the enclosing scope resumes from the
point where it left off. This is best illustrated on the example of randomised Large Neighbourhood
Search (LNS) below.
function ann: lns_min (var int: obj, array[int] of var int: x,
int: iterations, float: d) =
repeat (i in 1..iterations) (
scope (
post(neighbourhoodCts(x,d)) /\ % fix neighbourhood in the local scope
next() /\ % find next solution in neighbourhood
commit()
) /\
post(obj < sol(obj)) % post BAB constraint in the global scope
);
|
The yellow part is the local scope, that searches a random neighbourhood in each
iteration: the posted neighbourhood constraints are removed from the model at the end of the local
scope. In contrast, the BAB constraint that tries to find a better solution in the next iteration,
is posted in the global scope and is therefore not removed.
User-defined functions and function scope
A MiniSearch strategy is defined as MiniZinc function that can take any argument
but must return an annotation (ann
in short). This is necessary to
conform with the MiniSearch type system (and every MiniSearch builtin returns the
type ann
).
Below is an example of a user-defined function with empty body:
function ann: my_search() =
% some search
;
|
Function scope return values and commit()
Recall that MiniSearch functions implicitly return SAT (true/success) or UNSAT (false/failure).
How to achieve this in your function when the return type is ann
? This is done
by calling the
built-in commit()
.
commit()
is used to commit to the last found solution.
If commit
has been executed at least once in the scope of the function
(which represents the whole function body and is therefore different
from the search scope!) then the function will return SAT, and UNSAT otherwise.
Let's consider an example for illustration. In the first function below, we never execute
commit
, so this function will ALWAYS implicitly return UNSAT. In the
second function however, we commit to a solution after each successful call of next()
,
so if at least one solution has been found the function implicitly returns SAT, and UNSAT otherwise.
% this function will always return UNSAT because we don't commit to a solution
function ann: my_search_without_commit() =
repeat (
if next() then
print()
else break endif
);
% this function will return SAT if commit() is executed
function ann: my_search_with_commit() =
repeat (
if next() then
print() /\ commit()
else break endif
);
|
MiniSearch control built-ins
As noted above, all MiniSearch built-ins have an implicit return value that represents either `success'
(true) or `failure' (false). Using this concept, we introduce MiniSearch control built-ins.
All built-ins execute their arguments in order.
/\
and \/
The /\
-built-in (`and-built-in') runs its arguments in order and stops to return false as soon as one of
its arguments fails.
Similarly, the \/
-built-in (`or-built-in') stops and returns success as soon as one of its arguments
succeeds. Existing control mechanisms of MiniZinc such as if then else endif
expressions can be
used as well.
function ann: my_search_and() =
next() /\ print("Found a solution\n"); % executes print statement only if next() was successful
function ann: my_search_or() =
next() \/ print("No solution found\n"); % executes print statement only if next() failed
|
Looping with repeat()
The repeat(s)
built-in takes a MiniSearch specification s
and repeats it until
a break
built-in is executed. It returns false if a break
occurred,
otherwise returns what s
returned.
The delimited variant repeat(i in 1..N)(s)
will execute s
for N
iterations (or until break
is executed).
In the example below, my_search
searches for all solutions:
repeat
is executed until no more solutions can be found, in which
case break
is executed.
function ann: my_search() =
repeat (
if next() then
print("Found a(nother) solution\n") /\ commit()
else break endif
);
|
Limiting search time with time_limit()
The built-in time_limit(ms,s)
imposes a time limit ms
in milliseconds on any
MiniSearch specification s
. This way, s
stops whenever the time limit is reached,
returning its current status. Time-limits are handled transparently by the MiniSearch kernel as an exception.
Let's extend the example from above and extend it with a time-limit built-in: the search now finds all solutions
that can be found within 5 seconds. As soon as it takes longer than 5 seconds, next()
will fail
and break
will be executed.
function ann: my_search() =
repeat (
if time_limit(5*1000, next()) then % if a solution is found within 5 seconds
print("Found a(nother) solution\n") /\ commit()
else break endif
);
|
Time-limits can be put everywhere, also on the main call of your model. This makes it easy to control
the time-limit for your search via data files:
% ----- problem model omitted ----- %
int: timeout; % timeout is specified in data file
solve search
time_limit(timeout, my_search());
|
Assigning values to constants
In standard MiniZinc constant parameters such as int: N=10;
cannot change their value.
However, in MiniSearch we often want to change constants across different iterations. For this purpose,
we added the assignment operator ':=
' which may only be used inside a MiniSearch specification.
It overwrites that constant's current value by the value supplied.
As an example, consider using constant i
to count the number of found solutions:
function ann: my_search() =
let {
int: i = 0; % a local constant
} in (
repeat (
if next() then
i := i + 1 /\ % increase the constant's value for each new solution
commit() /\
print("Found solution "++show(i)++"\n")
else break endif
)
);
|
Solution Management built-ins
The strength of any meta-search language lies in using intermediate solutions to guide the remaining search.
For instance, branch-and-bound needs to access the objective to post further constraints, and a Large
Neighbourhood Search thaws some of the variables in a solution to continue in that neighbourhood.
sol()
and hasSol()
To facilitate working with solutions, the most recently found solution is always accessible in MiniSearch
using the sol
built-in, where sol(x)
returns the value of x
in the
last solution. MiniSearch also provides a hasSol()
built-in to test whether a solution exists.
In the example below, we first try to find the best possible solution within a timeout of t
milliseconds. Then we test if a solution has been found with hasSol()
: if yes, we print
the solution value, otherwise we print a simple message.
solve search
time_limit(t, minimize_bab(obj)) % find the best solution in t milliseconds
/\
if hasSol() then
print("Found solution with objective "++show(sol(obj))++" in "++show(t)++" milliseconds\n")
else print("No solution found\n") endif
;
|
Printing Solutions and Debugging
The print()
function without any arguments prints the last found solution in the format specified
in the model's output
item. Alternatively, print(s)
provides more fine-grained control
over the output. It prints the string s
, which can be constructed dynamically from values in the
solution using calls to sol
.
In the example below, if we find a solution within the time limit
t
we print the solution according to the output using print()
. Otherwise, if no
solution could be found, we print a message.
function ann: my_search(int: t) =
if time_limit(t, next()) then
print() % print the solution according to output model
else print("No solution found in "++show(t/1000)++" seconds.\n") % print message
endif;
|
MiniSearch can be debugged using print()
and MiniZinc's trace()
function to display
values of parameters, variables, and arbitrary expressions during search. trace
is a MiniZinc
built-in predicate that prints its string argument on stdout and simply returns true.
The example below shows a
'debug-version' of branch-and-bound search (BAB), where every BAB constraint is also printed on stdout
using trace
.
function ann: bab_min_debug(var int: obj) =
if next() then
commit() /\
post(
obj < sol(obj) /\ % the BAB constraint
trace("obj < "++show(sol(obj))++";\n") % prints the BAB constraint for debugging
)
else break
endif;
|
Furthermore, the MiniSearch
interpreter uses the C++ stack, so C++ debuggers can be used to follow the meta-search.