MiniSearch Documentation

  1. What is MiniSearch?
  2. A quick example
  3. Downloading MiniSearch
  4. Running MiniSearch
  5. Getting a FlatZinc solver
  6. Built-in meta-searches
  7. Writing your own meta-search in MiniSearch
  8. MiniSearch examples
  9. Reporting a MiniSearch bug



  1. What is MiniSearch?

    MiniSearch is a language for specifying meta-search in a MiniZinc model. Meta-search includes high-level (heuristic) searches such as Large Neighbourhoud Search (LNS). With MiniSearch you can now solve your MiniZinc model using any of the built-in meta-searches or your own handwritten meta-search.

    MiniSearch is also solver-independent, which means that you can run your meta-search with any FlatZinc solver, such as choco, chuffed, gecode or or-tools.


  2. A quick example: Solving a MiniZinc model with LNS

    Let's consider a sample MiniZinc model that consists of an array of decision variables x and an objective variable obj that should be minimized (we omit constraints for simplicity):

    array[int] of var int: x;                  % classical MiniZinc model
    var int: obj;
    % constraints omitted
    
    solve minimize obj;
    

    When running the model above in a backend solver, it will be solved with the standard optimisation technique of the solver (for instance, branch-and-bound for CP solvers). With MiniSearch we can run other meta-searches, even heuristic search, in the backend solver. Let's solve this model using Large Neighbourhood Search (LNS):

    include "minisearch.mzn";                   % MiniSearch model
    array[int] of var int: x; var int: obj; % constraints omitted int: iterations = 100; float: destructionRate = 0.3; solve search lns_min(obj, x, iterations, destructionRate);

    The changes in the model are highlighted in yellow. First, we need to include minisearch.mzn which defines the built-in meta-searches (and MiniSearch keywords), including LNS. Then, instead of calling solve minimize obj we use the MiniSearch built-in lns_min that takes the following parameters:

    • obj: the objective variable that is minimized
    • x: the array of decision variables on which LNS is performed
    • iterations: the number of LNS iterations
    • destructionRate: the percentage (between 0 and 1) of the variables x that will be 'destroyed' (whose value-assignment from the last solution will be lifted). In the example above, the destruction rate of `0.3' means that 30% of the variables in array x will be randomly reset in each iteration.

    You can execute the above MiniSearch model using the executable minisearch by typing the following into your terminal:

    minisearch model.mzn data.dzn

    In the above case, minisearch will use the default FlatZinc solver, fzn-gecode, for solving the problem. However, you can use any of your favourite FlatZinc solvers, such as fzn-chuffed:

    minisearch --solver fzn-chuffed model.mzn data.dzn

    Note that if the solver executable is not in the PATH, then you must specify the path to your solver. At the moment, we only provide a command line version for MiniSearch, but an IDE-version is in the works.


  3. Downloading MiniSearch

    The most recent source code is available on github, on the 'feature/minisearch' branch of libminizinc. To get the source code, use:

    git clone -b feature/minisearch https://github.com/MiniZinc/libminizinc.git


  4. Running MiniSearch

    We currently only provide a command-line version of MiniSearch, however, we are working on the integration of MiniSearch into the MiniZinc IDE, which we plan to release soon.

    After downloading the binary package of MiniSearch, you will find the MiniSearch executable, minisearch, in the bin/ folder. minisearch works similarly to the minizinc executable, and takes a model and data file as input, where the model may contain a MiniSearch specification:

    minisearch model.mzn data.dzn

    MiniSearch directly executes the FlatZinc solver, so if no solver is given as argument, MiniSearch uses fzn-gecode, assuming it is in the PATH. Alternatively, you can specify a FlatZinc solver with the --solver option, for instance the FlatZinc solver fzn-ortools:

    minisearch --solver fzn-ortools model.mzn data.dzn

    If the FlatZinc solver binary is not in the PATH, you need to specify its full path:

    minisearch --solver /path/to/fzn-ortools model.mzn data.dzn

  5. Getting a FlatZinc solver

    A FlatZinc solver is any solver that can read and solve FlatZinc models. Many popular CP solvers provide a FlatZinc solver. Below we give a list of solvers that provide a FlatZinc solver and that we have tested with MiniSearch.

    • Choco is a CP solver written in Java. It provides a FlatZinc solver fzn_choco here.

    • Chuffed is a CP solver using lazy-clause generation (LCG) written in C++. Its FlatZinc solver fzn_chuffed can be found in the trunk of its git repository. To obtain the executable of fzn_chuffed you need to compile and install the trunk which will create fzn_chuffed in the install directory.

    • Gecode is a CP solver written in C++. It ships FlatZinc solver fzn-gecode as part of its binary packages.

    • or-tools is Google's software suite for optimisation problems written in C++. Obtain the or-tools source code from or-tools' github page and after compilation, you will find the or-tools FlatZinc solver fz in the bin/ directory.

    Let us know if your FlatZinc solver is missing and you would like to promote it here.


  6. Built-in meta-searches in MiniSearch

    MiniSearch provides some builtin meta-searches.
    1. Branch-and-Bound Search

    2. The simplest meta-search is CP-based branch and bound (BAB): after each newly found solution, a constraint is added to find a solution with a better bound on the objective. In MiniSearch there exist minimize_bab for minimisation and maximize_bab for maximisation.

      include "minisearch.mzn";
      var int: obj;
      % some constraints and other variables

      solve search minimize_bab(obj);

      Note that for most solvers the behaviour will be almost the same as when writing solve minimize obj.

    3. Lexicographic Branch-and-Bound Search

    4. Lexicographic BAB can be used for solving multi-objective optimisation problems, if the different objectives can be ranked according to their importance. Then the array of objectives is minimised (or maximised) lexicographically.

      include "minisearch.mzn";
      array[int] of var int: obj_array;
      % some constraints and other variables

      solve search minimize_lex(obj_array);
    5. Randomised Large Neighbourhood Search (LNS)

    6. Randomised Large Neighbourhood Search (LNS) iteratively 'destroys' a random part of a previously found solution, while fixing the remaining part, and resolves the problem to optimality (or until a better solution has been found).

      Therefore, the MiniSearch random LNS built-in lns_min (or lns_max for maximisation) takes the following arguments: objective variable obj, the array of variables x of which a part will be randomly destroyed, the number of iterations and the destructionRate (a value between 0 and 1) which states the percentage of the variables in x that should be destroyed in each iteration. lns_min (and lns_max) find the next better solution in each iteration.

      include "minisearch.mzn";
      array[int] of var int: x;
      var int: obj;
      % some constraints and other variables

      int: iterations = 100;
      float: destructionRate = 0.3;
      solve search lns_min(obj, x, iterations, destructionRate);

      There also exists an extended version of lns_min (and lns_max) that searches the neighbourhood to optimality in each iteration. Because this can be costly in time, this version takes a timelimit time_ms in milliseconds for exploring the neighbourhood. If no time limit is required, time_ms can be set to zero.

      include "minisearch.mzn";
      array[int] of var int: x;
      var int: obj;
      % some constraints and other variables

      int: iterations = 100;
      float: destructionRate = 0.3;
      int: time_ms = 5*1000; % timeout of 5 secs for searching the neighbourhood
      solve search lns_min(obj, x, iterations, destructionRate, time_ms);
    7. Simple Adaptive LNS

    8. Adaptive LNS is an extension of randomised LNS where the destruction rate is adapted over the iterations. In the simple version that MiniSearch provides, the destruction rate is increased by 1% in each iteration where no better solution has been found.

      include "minisearch.mzn";
      array[int] of var int: x;
      var int: obj;
      % some constraints and other variables

      int: iterations = 100;
      int: initRate = 20; % start with destroying 20%
      int: time_ms = 5*1000;
      solve search adaptive_lns_min(obj, x, iterations, initRate, time_ms);

  7. Writing your own meta-search - The MiniSearch Language

    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.

    MiniSearch built-in Description
    s1 /\ s2 run search s1 and iff successful, run s2
    s1 \/ s2 run search s1 and iff it fails, run s2
    c := v assign parameter c the value v
    break break within a repeat
    commit() commit to the last found solution in the function scope
    fail return 'failure'
    hasSol() returns true if a solution has been found, false otherwise
    if s then s1 else s2 if search s is successful, run s1, otherwise run s2
    next() find the next solution
    print() print last found solution according to the model's output specification
    print (str) print MiniZinc output string str
    post (c) post MiniZinc constraint c in the current scope
    repeat (s) repeat search s until break is executed
    repeat (i in 1..N) (s) repeat search s for N times, or until break is executed
    scope (s) open a local scope containing search s
    skip return 'success'
    sol(x) return solution value of variable x
    time_limit (m,s) run s until time-limit m (in milliseconds) is reached

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


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



    3. 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
         );
      



    4. 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
           )
        );
      


    5. 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 twe 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.


  8. MiniSearch Examples

    Here we show some examples for using MiniSearch that we build up step-by-step. They have different difficulty levels, depending on the required experience.

    1. Finding the first k solutions (beginner)

      We start with an easy example for beginners: finding the first k solutions of a problem. Let's begin with the (empty) body of our MiniSearch function:

      function ann: k_solutions(int: k) =
        % empty function body
      ;
      

      We will repeatedly call next() until we reached the threshold k. This means we will need to introduce a local constant to count the number of found solutions:

      function ann: k_solutions(int: k) =
       repeat (i in 1..k) (
            % actual search
       );
      

      Now let's include the repeated call of next(): if next() is successful, then we commit to the solution and print it. Otherwise, we break and print an error message, since we found less than k solutions.

      function ann: k_solutions(int: k) =
       repeat (i in 1..k) (
          if next() then
             commit() /\ print("Solution "++show(i)++":\n") /\ print()
          else 
             print("No more solutions found.\n") /\ break
          endif
       );
      

      An alternative formulation would use a counter i for each found solution:

      function ann: k_solutions_2(int: k) =
        let { int: i = 0; }
        in (
          repeat (
            if i == k then break else skip endif  % check if we already reached k solutions
            /\
            if next() then 
               i := i+1 /\
               commit() /\ print("Solution "++show(i)++":\n") /\ print()
            else 
               print("Only found "++show(i)++" solutions.\n") /\ break
            endif
         )
        );
      

      Check out the n-queens problem that uses MiniSearch for finding the first k solutions: queen_k_sols.mzn. You can run it directly in MiniSearch.

    2. More examples will come soon.