« JSR-331 is now an official standard | Main | G12 MiniZinc version 1.5 released »

Tom Schrijvers, Guido Tack et.al: Search Combinators - paper and implementation

A paper and an implementation of Search Combinators - a framework to define application-tailored search strategies - has been available.

Paper

The paper is:
Tom Schrijvers, Guido Tack, Pieter Wuille, Horst Samulowitz, Peter J. Stuckey: Search Combinators (ArXiv). Abstract:
The ability to model search in a constraint solver can be an essential asset for solving combinatorial problems. However, existing infrastructure for defining search heuristics is often inadequate. Either modeling capabilities are extremely limited or users are faced with a general-purpose programming language whose features are not tailored towards writing search heuristics. As a result, major improvements in performance may remain unexplored. This article introduces search combinators, a lightweight and solver-independent method that bridges the gap between a conceptually simple modeling language for search (high-level, functional and naturally compositional) and an efficient implementation (low-level, imperative and highly non-modular). By allowing the user to define application-tailored search strategies from a small set of primitives, search combinators effectively provide a rich domain-specific language (DSL) for modeling search to the user. Remarkably, this DSL comes at a low implementation cost to the developer of a constraint solver.
The article discusses two modular implementation approaches and shows, by empirical evaluation, that search combinators can be implemented without overhead compared to a native, direct implementation in a constraint solver.

Implementation

An implementation using MiniZinc and Gecode is available from Gecode's FlatZinc page. The README file describes the tools as:
These two tools [minizinc-to-minizinc pre-compiler and FlatZinc interpreter], together with the G12 mzn2fzn translator, comprise a complete toolchain for solving MiniZinc models using search combinators. The pre-compiler translates a slightly extended version of MiniZinc to standards-compliant MiniZinc. The FlatZinc interpreter was modified to understand search combinators expressed as annotations.

In order to use the tools, you will need the standard mzn2fzn compiler from the G12 MiniZinc distribution, which can be downloaded at http://www.g12.cs.mu.oz.au/minizinc/download.html

Example

Two examples are included in the distribution: golomb.mzn and radiation.mzn. The golomb.mzn is shown here, where the specific changes has been marked:
include "globals.mzn";
include "searchcombinators.mzn";

int: m;
int: n = m*m;

array[1..m] of var 0..n: mark;
array[1..(m*(m-1)) div 2] of var 0..n: differences =
    [ mark[j] - mark[i] | i in 1..m, j in i+1..m];

constraint mark[1] = 0;
constraint forall ( i in 1..m-1 ) ( mark[i] < mark[i+1] );
constraint alldifferent(differences);

% Symmetry breaking
constraint differences[1] < differences[(m*(m-1)) div 2];

solve :: dicho(print(mark,int_search(mark,input_order,assign_lb)),
            mark[m],
            0,200)
            satisfy;
The result using the included data file golomb-10.dzn (m=10) is
{0, 1, 3, 7, 12, 20, 30, 44, 65, 80}
{0, 1, 3, 11, 17, 29, 36, 51, 56, 60}
{0, 1, 6, 10, 23, 26, 34, 41, 53, 55}
I have just started to experiment with this and might return with a longer report.