" /> My Constraint Programming Blog: April 2009 Archives

« March 2009 | Main | May 2009 »

April 26, 2009

Learning constraint programming (languages) - part I

While preparing for My talk at SweConsNet Workshop 2009: "Learning Constraint Programming (MiniZinc, JaCoP, Choco, Gecode/R, Comet, Gecode): Some Lessons Learned", I plan to blog about summarizations, findings etc.

This part is a description of the problems I tend to start modeling in a new constraint programming system.

First run
The first model to run is probably SEND+MORE=MONEY or n-queens, since either one of them are distributed in the package. This is to make sure that the system works, environment variables are correct, compilation works, how is the constraints and search strategies stated in the system, what to expect in terms of output, etc.

First models
If either SEND+MORE=MONEY or n-queens is not in the distribution (which would be a surprise), I start with that model.

The models
The models below are all the first problems I start with, sorted in the way they usually are implemented. Also there is a a short explanation what is learned about the system. After all these models are done, or a larger part of them, I publish them at a My [CP System] Page..

The list is very personal and may not be suited for everybody (if anyone, except me). One reason is that my goal has been to learn about modeling problems using constraint programming, and not so much about implementing propagators etc (and that is why I tend use decompositions a lot). However, lately I have somewhat shifted the focus to more gory details.

Also, I think it is important that when learning new stuff (especially by oneself) is to use examples that are well known, fun, and perhaps even with a personal history. Some examples of this "personal attachment" of a problem:
  • The Least Diff problem was a problem in a company competition 1998 and was actually one of my inspiration to start learning constraint programming. The first version was programmed in a Prolog system, SICStus Prolog.
  • Seseman problem: this was a problem stated by a fellow blogger in 2005, and I blogged about (in swedish) in Sesemans matematiska klosterproblem samt lite Constraint Logic Programming).
  • de Bruijn sequences is a personal favorite problem since long time.
  • etc.
The implementations are sorted in (approximately) the order I start to learn the systems.
  • MiniZinc (feb 2008)
  • Choco (first "touch" in 2006, and then more in september 2008)
  • JaCoP (august 2008)
  • Gecode/R (january 2009)
  • Comet (local search module 2007, constraint programming module: january 2009)
  • Gecode (march 2009)
Note: Before 2008 I have sporadically studied (played) with some Prolog systems with support for constraint logic programming, e.g. ECLiPSe and SICStus Prolog, and also with some other CP-systems (e.g. OPL, XPress, ESSENCE'/Tailor/Minion) but not at all that systematic as with the systems mentioned in the list above. Later on, the following problems has been useful and rewarding to model early. Note: The two problems Crosswords and Word square has not been published before, and I plan to blog more about the findings when modeling these "non-trivial Element" models.

Posted by hakank at 08:54 AM | | Comments (2)

Comet: version 1.2-rev2 released and a facelift of the site

Two things that is new this weekend.

1) Version 1.2-rev2 has been released. To cite the release note: It contains a number of bug fixes and significant improvement in performance on a variety of benchmarks..

Download this version here.

2) The Dynadec site was also updated this weekend. Now it is more organized and contains things as:

Also, I have forgot to say that the Forums are now quite active (and the mailing list is practically closed). Fortunately there is an option of geting a mail whenever a new message is written.

Posted by hakank at 08:52 AM |

April 13, 2009

Regular expressions in Gecode

Using regular expressions for constraint programming is not new. The following examples from the Gecode distribution uses regular expressions in some way (the links are to the Gecode site): I have now started to learn more about Gecode's support for regular expression. The following operations are supported (from Gecode::REG Class Reference:
  • =: Assign to regular expression r.
  • +: Return expression for: this expression followed by r.
  • +=: This expression is followed by r.
  • |: Return expression for: this expression or r.
  • |=: This expression or r.
  • *: Return expression for: this expression arbitrarily often (Kleene star).
  • +: Return expression for: this expression at least once.
  • (unsigned int n, unsigned int m): Return expression for: this expression at least n and at most m times.
  • (unsigned int n): Return expression for: this expression at least n times.
See below for some examples.

Global contiguity

For a simple use of regular expressions to implement a global constraint is global contiguity which is explained is Global constraint catalog as:
Enforce all variables of the VARIABLES collection to be assigned to 0 or 1. In addition, all variables assigned to value 1 appear contiguously.
The model global_contiguity.cpp implements this by the simple regular expression: 0*1*0*, i.e. 
REG r0(0), r1(1);
extensional(*this, x, *r0 + *r1 + *r0);
Note that the operators are before the REG element.

(This model also implements global contiguity by a variant of the slide constraint.)

Generating names via regular expressions

In April 2004 Geoffrey K. Pullum (at Language Log) wondered about the many spellings of the swedish author Henning Mankell in The mysteries of... what's his name?.

I then wrote an Icon program for generating all the different versions of the names, and presented the program and solutions in the (swedish) blog posts: It was a fun problem and I have now implemented a version in Gecode: all_regexp.cpp.

There are two names (regular expressions) which are generated.

Henning Mankell
This uses the regular expression [hm][ea](nk|n|nn)(ing|ell|all), which in Gecode is stated as 
extensional(*this, X, 
            (h|m) +                            // [hm]
            (e|a) +                            // [ea]
            ((n+k) | n | (n+n) ) +             // (nk|n|nn)
            ( (i+n+g) | (e+l+l) | (a+l+l))     // (ing|ell|all)
            );
In the original both the first and last name was generated; here we just generate the first name (or the last name).

Here are all 36 solutions:
Total: 36 solutions:
hanall
hanell
haning
henall
henell
hening
manall
manell
maning
menall
menell
mening
hankall
hankell
hanking
hannall
hannell
hanning
henkall
henkell
henking
hennall
hennell
henning
mankall
mankell
manking
mannall
mannell
manning
menkall
menkell
menking
mennall
mennell
menning
kjellerstrand
This is my last name and I have seen a lot of misspellings of this name. The regular expression for some of the variants is k(je|ä)ll(er|ar)?(st|b)r?an?d which in Gecode is implemented as: 
extensional(*this, X, 
            k +                  // k
            (j+e|auml) +         // (je|ä)
            l+l +                // ll
            ((e+r)|(a+r))(0,1) + // (er|ar)?
            ((s + t)|b) +        // (st|b)
            r(0,1) +             // r?
            a+                   // a
            n(0,1) +             // n?
            d                    // d
            );
Different sizes, collecting all solutions
The model actually loops through many models with different sizes (length of the array) and collects all the solutions in a vector that is printed at the end of the program. Here is a the main function: 
int
main(int argc, char* argv[]) {
  SizeOptions opt("AllRegexp");
  opt.solutions(0);
  opt.model(AllRegexp::MODEL_MANKELL);
  opt.model(AllRegexp::MODEL_MANKELL, "mankell");
  opt.model(AllRegexp::MODEL_KJELLERSTRAND, "kjellerstrand");
  opt.parse(argc,argv);
  // default for the mankell model
  int min = 6;
  int max = 7;
  if (opt.model() == AllRegexp::MODEL_KJELLERSTRAND) {
    min = 7;
    max = 13;
  }

  // loop through all the different sizes
  for(int s = min; s <= max ; s++) {
    opt.size(s);
    Example::run(opt);    
  }

  std::cout << "Total: " << all_solutions.size() << " solutions: " << std::endl;
  for(unsigned int i = 0; i < all_solutions.size(); i++) {
    std::cout << all_solutions[i] << std::endl;
  }

  return 0;

Posted by hakank at 12:29 PM |

April 12, 2009

12 more Gecode models. e.g. circuit, clique, and Hidato puzzle

Here are 12 more Gecode models and some comments. Note that more information and references to the problem is always presented is the model. These and other Geode models are collected at My Gecode page.
  • alldifferent_except_0.cpp: Global constraint of alldifferent_except_0 (decomposition), also the slightly more general alldifferent_except_c

    This is one of my first test models how to create (a decomposition of) a global constraint as well as how to call a function. Note the use of imp (implication): 
    void alldifferent_except_c(Space& space, IntVarArray x, int c, IntConLevel icl = ICL_BND) {
  for(int i = 0; i < x.size(); i++) {
    for(int j = i+1; j < x.size(); j++) {
      post(space,
           tt(imp(x[i] != c && x[j] != c, // =>
                  x[i] != x[j])),
           icl
           );
    }
  } 
}
    Just for fun, the model also has the constraint that there should be at least one 0.
  • discrete_tomography.cpp: Discrete tomography

    For more about discrete tomography, see for example Christoph Dürr's Discrete Tomography and the comments in the ECLiPSe code tomo.ecl.txt.

    The coding of the model was quite straightforward. The main lesson learned here is to be able to state (from the command line) which problem to solve. I borrowed the principle used in Gecode's nonogram example.

    First in the model is the global variables for accessing the specific problem: 
    namespace {
  extern const int* problems[];         // List of problems
  extern const unsigned int n_examples; // Number of specifications
}
    And last in the file is the specifications of the problems: 
    namespace {
  // ...
  // Specification for problem 1
  const int p1[] =
    { 11, 12,
      // Rows sums
      0,0,8,2,6,4,5,3,7,0,0,
      // Column sums
      0,0,7,1,6,3,4,5,2,7,0,0
    };
  
  // ...
    To access the problem the following is used (slightly compressed) 
    class DiscreteTomography : public Example {
protected:
  const int* prob;  // Problem to be used
  IntVarArray x;     // Fields of matrix
  int rows(void) const { return prob[0]; } // Return rows of matrix
  int cols(void) const { return prob[1]; } // Return columns of matrix
public:
  DiscreteTomography(const SizeOptions& opt) 
    : prob(problems[opt.size()]),
      x(*this, rows()*cols(), 0, 1)
  {
    // ...
  • labeled_dice.cpp: Labeled dice problem

    Jim Orlin wrote about this puzzle in Colored letters, labeled dice: a logic puzzle and I presented a Comet solution (labeled_dice.co) in Comet: regular constraint, a much faster Nonogram with the regular constraint, some OPL models, and more.

    The Gecode model use one element constraint and a couple of count constraints. It was simpler than I first thought.
  • building_blocks.cpp: Building Blocks (Dell Logic Puzzle)

    This problem almost the same as labeled_dice (see above) and should perhaps be incorporated into that model.
  • young_tableaux.cpp: Young tableaux and partitions

    Young tableaux are described in the Wikipedia article Young tableau and MathWorld article YoungTableau, and is one of my standard comparison models.

    The tricky part here was to calculate the partition (from the Young tableau), especially the following (MiniZinc/Comet) where p is the partition element, and x is the Young tableau matrix. p[i] == sum(j in 1..n) (x[i,j] <= n) The corresponding Gecode was: 
    for(int i = 0; i < n; i++) {
  // p[i] == sum(j in 1..n) (x[i,j] <= n)
  IntVar t(*this, 0, n+1);
  count(*this, m.row(i), n+1, IRT_EQ, t, opt.icl());
  post(*this, p[i] == n-t, opt.icl());
}
    Not very advanced, but it took some time.
  • set_covering_deployment.cpp: Set covering deployment

    Set covering deployment is presented in the MathWorld Set Covering Deployment and uses a small example of placing Roman armies.

    Well, the hardest part was the second requirement: "There should always be an backup army near every city". See the model how I implemented that.
  • subset_sum.cpp: Subset sum problem

    This problem is from Katta G. Murty Optimization Models for Decision Making (PDF) page 340:
    Example 7.8.1

    A bank van had several bags of coins, each containing either 16, 17, 23, 24, 39, or 40 coins. While the van was parked on the street, thieves stole some bags. A total of 100 coins were lost. It is required to find how many bags were stolen.
    Comments The subset sum constraint is simply this constraint where x is the values to choose from and tot is the sum: 
     linear(space, values, x, IRT_EQ, tot,  icl);
    The model is slightly more general, as the total (to sum) can be set from the command line.
  • sonet.cpp: SONET problem

    This is a standard problem in constraint programming. My solution is based on the ESSENCE' (Andrea Rendl's Tailor) model sonet_problem.eprime.

    The biggest problem was to translate the following requirement if there is a demand between 2 nodes, then there has to exist a ring, on which they are both installed which use an exists construct in the ESSENCE' model (as well as my MiniZinc model sonet_problem.mzn. The correspondent Gecode code is: 
    for(int client1 = 0; client1 < n; client1++) {
  for(int client2 = client1 + 1; client2 < n; client2++) {
    if(demand[client1*n+client2] == 1) {
      // ESSENCE' code:
      //   exists ring : int(1..r) .
      //      rings[ring,client1] + rings[ring, client2] >= 2)

      // here we use reification: 
      BoolVarArray bs(*this, r, 0, 1);
      for(int ring = 0; ring < r; ring++) {
        // does this ring satisfy the condition?
        // note: the "~" is needed
        bs[ring] = post(*this, ~(rings_m(client1, ring) + rings_m(client2,ring) >= 2), opt.icl());
      }
      // at least one success is needed
      linear(*this, bs, IRT_GQ, 1, opt.icl());
    }
  }
}
    I really like that Gecode supports this higher level of stating logical operations and reifications.
  • hidato.cpp: Hidato puzzle

    Hidato is yet another grid puzzle. For more about Hidato see the following sources (and games to play): The first source explains the problem as:
    Puzzles start semi-filled with numbered tiles. The first and last numbers are circled. Connect the numbers together to win. Consecutive number must touch horizontally, vertically, or diagonally.


    Conceptually the problem can be modeled as follows (which was done in the MiniZinc model hidato.mzn), e.g. one forall loop and four exists loops. It works but is inefficient: 
      % ...
  forall(k in 1..r*c-1) (
     exists(i in 1..r, j in 1..c) (
        k = x[i, j] % fix this k /\
        exists(a, b in  {-1, 0, 1}
          where 
          i+a >= 1 /\ j+b >=  1 /\
          i+a <= r /\ j+b <= c
          /\ not(a = 0 /\ b = 0) 
        ) 
        (
          % find the next k
          k + 1 = x[i+a, j+b]  
        )
     )
  )
    I started to follow this logic in Gecode with a lot of boolean arrays and reifications, but after some thoughts here is what was used instead. 
        for(int k = 1; k < n*n; k++) {
      IntVar i(*this, 0, n-1);
      IntVar j(*this, 0, n-1);
      IntVar a(*this, -1, 1);
      IntVar b(*this, -1, 1);

      // 1) First: fix this k, i.e.
      //        k == board[i*n+j]
      IntVar inj(*this, 0,n*n-1);
      post(*this, inj == i*n+j, opt.icl());
      element(*this, board, inj, k, opt.icl());

      // 2) Then, find the position of the next value, i.e.
      //     k + 1 == board[(i+a)*n+(j+b)]
      IntVar ai(*this, 0, n-1); // this takes care of the borders of the matrix
      IntVar jb(*this, 0, n-1); // ibid.
      post(*this, a+i == ai,opt.icl());
      post(*this, j+b == jb,opt.icl());
      IntVar ai_plus_jb(*this, 0,n*n-1);
      post(*this, ai_plus_jb == ai*n+jb, opt.icl());
      element(*this, board, ai_plus_jb, k+1, opt.icl());
    }
    Note that the borders of the matrix is handled by the domains of the IntVar's ai and jb.
  • circuit_orbit.cpp: Global constraint circuit (decomposition) using permutation orbits

    circuit is a global constraint I have been fascinated by for a time, and I first implemented a decomposition in MiniZinc (circuit_test.mzn). Gecode has a builtin version of circuit, but I thought it could be fun to implement this decomposition as well.

    It uses some observation I noted about permutation orbits when playing around with another problem.

    Also, it sets the parameter c_d (recomputation commit distance) to size*2 in order to save memory. For example, with the default value of requires 600Mb memory for the problem size=500, but with c-d 1000 requires only 12Mb (for more about this, see the discussion and comments in de Bruijn sequences in Gecode (and other systems)).
  • nadel.cpp: Nadel's construction problem ("soft" version)

    This a construction problem attributed by Rina Dechter "Constraint Processing" (page 5) to B.A. Nadel's article "Constraint satisfaction algorithms" (1989). I not sure about the solution, since I have not been able to find Nadel's article.

    I haven't found any solution that satisfies all the constraints presented in the problem (which may indicate that my model is wrong).

    However this can be used as a study of reifications: this "soft" version minimized the broken constraints, and generates 28 different solutions with 1 broken constraint. The broken constraints are either
    • steep_slopes constraints, or
    • near_dump constraints.
  • clique.cpp: Global constraint clique (decomposition), maximize the cardinality of cliques in a graph

    This decomposition of the global constraint clique for a graph g uses the (obvious) observation that if two different nodes is in the same clique (s) then there must be a connection between the two nodes in the boolean (channeled) representation of s. This actually seems to be enough for use as a constraint (which is an example of the declarative nature of constraint programming). In MiniZinc parlance this is formulated in the model clique.mzn as: 
    link_set_to_booleans(x, x_bool) /\
forall(i,j in 1..n where i != j) (
   (x_bool[i] /\ x_bool[j]) -> ( g[i,j] > 0)
) /\
c = card(s)
    The Gecode variant is slightly more complicated, mainly because the imp function don't accept IntArgs as a second argument. 
    // x_bool is a boolean representation of the clique set x
BoolVarArray x_bool(*this, n, 0, 1);
channel(*this, x_bool, x); // channel the clique to a boolean array
for(int i = 0; i < n; i++) {
  for(int j = 0; j < n; j++) {
    if (i != j) {
      BoolVar b(*this, 0, 1);
      if (g[i*n+j] > 0) {
        post(*this, b == 1, opt.icl());
      } else {
        post(*this, b == 0, opt.icl());
      }
      post(*this, tt(imp(
                        x_bool[i] == 1 && x_bool[j] == 1, // ->
                        b)),
          opt.icl());
     }
  }
}
    The model contains the small example from Global constraint catalog: clique, a graph of 10 nodes, a bigger random graph of 100 nodes, and a graph randomizer. These examples is choosen by re-commenting the source code.

    The included random graph of size 100 finds a maximum clique (size 6) in about 2 seconds. and generates the four size 6 cliques in about the same time.

Posted by hakank at 08:53 PM |

April 07, 2009

My talk at SweConsNet Workshop 2009: "Learning Constraint Programming (MiniZinc, JaCoP, Choco, Gecode/R, Comet, Gecode): Some Lessons Learned"

I'm proud to announce that I will talk at SweConsNet Workshop 2009 on May 27th 2009 in Linköping, Sweden. (See the blog post SweConsNet Workshop 2009 for more info about the workshop.)

The title ot the talk is Learning Constraint Programming (MiniZinc, JaCoP, Choco, Gecode/R, Comet, Gecode): Some Lessons Learned and will be about my findings when learning different constraint programming systems, including comparisons and - perhaps - some wishes.

For more about these systems see the following Also, there are more written in my swedish blog, mostly about MiniZinc, JaCoP, and Choco: category Constraint programming.

Posted by hakank at 05:43 PM |

April 05, 2009

Some new Gecode models

Here are some new Gecode models created since the last week, consisting mostly of two kind of standard problems:
  • simple operations reasearch problems
  • logical problems
When modeling these problems some findings where discovered which also are presented.

  • assignment.cpp
    Simple assignment problem from Winston's "Operations Research, page 393f.

  • organize_day.cpp
    Organizing a day, simple operations research problem (ECLiPSe)

    Findings:
    The function no_overlap was quite easy to write, using reification and booleans. 
    void no_overlap(Space& space, IntVar s1, int d1, IntVar s2, int d2, IntConLevel icl = ICL_BND) {
  post(space, tt((s1 + d1 <= s2) || (s2 + d2 <= s1)), icl);
}
    Note: tt is needed so the logic expressions are interpreted as reifications.
  • coins3.cpp
    Minimum number of coins to pay exactly any amount between 1 and 99 cents. From the ECLiPSe book.

    Findings: One thing I almost always want when modeling optimization problems, is to investigate both the optimimum (maximum/minimum) and also see all solutions for that optimum.

    In this model different search methods can be stated via the command line.
    • BAB (Branch and Bound) and Restart for minimizing the number of coins
    • DFS (Depth First Search) for searching the complete search tree given a value from command line (opt.size()).

    When using the DFS (e.g. coins3.exe -search dfs 8) the value from the command line constrains the model with this condition: 
    if (num_coins_val) {
   post(*this, num_coins == num_coins_val, opt.icl());
}
  • set_covering.cpp
    Set covering problem: placing of firestations (Winston "Operations Research", page 486)
  • zebra.cpp
    The famous zebra problem.

    Findings:
    For the constraint x is next to y the usual approach is to use: abs(x,y) == 1 .

    However, in Gecode we cannot state the abs condition directly, so here is what I did instead (inspired by the Gecode examples all-interval.cpp): 
     void next_to(Space & space, IntVar x, IntVar y, IntConLevel icl = ICL_DOM) {
    post(space, abs(space, minus(space, x, y, icl), icl) == 1, icl); 
}
    Usage: next_to(*this, smoke[Chesterfields], animal[Fox], opt.icl());
  • who_killed_agatha.cpp
    Who killed agatha? (The Dreadsbury Mansion Murder Mystery) is a standard benchmark in theorem proving, and also a good test of how to express logical relations in a constraint programming language.

    Findings:
    In Gecode it is not as easy to state this problem as in MiniZinc who_killed_agatha.mzn or in Comet who_killed_agatha.co; these models can be studied for comparison.

    Gecode has, however, support for implications (imp) and logical equivalence (eqv), which it makes it easier to state these kind of logical relations (than without them).

    One example: The constraint Charles hates noone that Agatha hates. is translated into the following Gecode code (the comment shows the MiniZinc version). Note: hates_m is a Matrix wapper for the IntVarArray hates; the access for rows and columns is hates_m(col, row). 
    for(int i = 0; i < n; i++) {
  // MiniZinc: hates[charles, i] = 0 <- hates[agatha, i] = 1
  post(*this, tt(imp(hates_m(i,agatha) == 1, hates_m(i,charles) == 0)), opt.icl());
}

    The biggest problem was to formulate the constraint A killer always hates, and is no richer than his victim.. In MiniZinc and Comet the first part can be stated directly simply as 
    hates[the_killer, the_victim] = 1
    Since hates is an IntVarArray this is to be reinpreted as hates[the_killer * n + the_victim] = 1 (n is the column size).

    However, since both the_killer and the_victim are IntVars we cannot use the element constraint directly. Well, after some experimentation the following (somewhat hairy) utilily function was created: 
    void element_m(Space & space, IntVarArray m, IntVar x, IntVar y, int rows, int cols, int val, IntConLevel icl = ICL_DOM) {
  IntVar x_n(space, 0, (rows*cols)-1);
  IntVar ix(space, 0, (rows*cols)-1); 
  IntVar e1(space, 0, rows-1);
  post(space, x_n == x*rows, icl); // x_n = x*rows
  post(space, ix==x_n+y, icl);     // ix = x*row + y
  element(space, m, ix, e1, icl);  // e1 = m[x*row +y]
  post(space, e1 == val, icl);     // val = m[x*row +y]
} // end element_m
    The function is then called as: element_m(*this, hates, the_killer, the_victim, n, n, 1, opt.icl());.
    I'm not very proud of this, but it works. The constraint could probably be stated in a more succint way.
  • stable_marriage.cpp
    Stable marriage is also a standard problem in constraint programming, from Pascal Van Henteryck's great OPL book ("The OPL Optimization Programming Language").

    Findings:
    Formulating this problem in OPL, Comet (which is very influenced by OPL), and MiniZinc is quite easy. See stable_marriage.mzn (MiniZinc), stable_marriage.co (Comet).

    In Gecode the real problem was to translate the following OPL constraint to Gecode: 
    forall(m in Men, w in Women)
  rankMen[m,w] < rankMen[m, wife[m]] => rankWomen[w,husband[w]] < rankWomen[w,m];
    Here rankMen and rankWomen are IntArgs and wife and husband are IntVarArrays (m is an integer loop variable).

    As for the Agatha model, a utility function (element_m2) was created, and the corresponding Gecode code became: 
    for(int m = 0; m < n; m++) {
   IntVar rankMen_res = element_m2(*this, rankMen, m, wife, n, opt.icl());
   for(int w = 0; w < n; w++) {
     IntVar rankWomen_res = element_m2(*this, rankWomen, w, husband, n, opt.icl());
     BoolVar b1 = post(*this, ~(rankMen[m*n+w] < rankMen_res));
     BoolVar b2 = post(*this, ~(rankWomen_res < rankWomen[w*n+m]));
     post(*this, tt(imp(b1, b2)), opt.icl());
  }
}
    Note here the usage of the two BoolVars b1 and b2 in the declarations, and also the use of reifications (~) in the post expressions.
Some thought: Maybe one of the cause of the problems I have in formulating Gecode models is that I'm translating the logic from OPL/Comet/MiniZinc, instead of stepping back and think about the problem in a new way.

Posted by hakank at 10:23 AM | | Comments (2)

April 04, 2009

MiniZinc/FlatZinc support in SICStus Prolog version 4.0.5

The other day I downloaded a demo of SICStus Prolog version 4.0.5, with the sole intention of testing the new support for MiniZinc/FlatZinc. The version I downloaded was for Linux 32 bit glibc 2.7 (my machine use glibc 2.6 but it seems to work well anyway).

The support for MiniZinc/FlatZinc in SICStus Prolog is described more in 10.35 Zinc interface - library(zinc). Some restrictions are described in Notes:
  • Domain variables
    Only variables with finite integer domains are supported. This includes boolean variables which are considered finite integer domain variables with the domain 0..1.
  • Optimization problems
    Only variables with finite integer domains can be optimized in minimize and maximize solve items. The int_float_lin/4 expression as described in the FlatZinc specification is thus not supported.
  • Solve annotations
    • The solve annotations currently supported are int_search/4, bool_search/4, and labelling_ff/0.
    • The FlatZinc specification describes several exploration strategies. Currently, the only supported exploration strategy is "complete".
    • When no solve annotation is given, a most constrained heuristic is used on all problem variables (excluding those that have a var_is_introduced annotation, see below). This corresponds to labeling/2 of library(clpfd) with the option ffc.
    • The choice method "indomain_random" as described in the FlatZinc specification uses random_member/2 of library(random). The random generator of SICStus is initialized using the same seed on each start up, meaning that the same sequence will be tried for "indomain_random" on each start up. This behavior can be changed by setting a different random seed using setrand/1 of library(random).
  • Constraint annotations
    Constraint annotations are currently ignored.
  • Variable annotations
    Variable annotations are currently ignored, except var_is_introduced, which means that the corresponding variable is not considered in any default labeling (such as when no search annotation is given or when the labelling_ff search annotation is given).

Testing

For testing the MiniZinc solver I used exactly the same principle as I do for the ECLiPSe solver, so hooking it up into in my system was very easy. All this is done via a Perl script of my own. It consists of generating a Prolog file, here called prolog_file.pl with the content below . model.mzn is the MiniZinc file to run, and number_of_solutions is the number of solutions to generate (an integer, or all for all solutions). 

%
% Generated by mzx.pl
%
:- use_module(library(zinc)).

go :-
   mzn_run_file('model.mzn',
                       [solutions(number_of_solutions)]),
   halt.
And then running the following command (from the Perl program):
sicstus -l prolog_file.pl --goal go.

Findings

Most things works very well and with about the same performance as the ECLiPSe solver. I will investigate some more before (perhaps) buying a private license of SICStus Prolog (or upgrading from my old version 3.9.1 if that is possible). However, I did find some problems.
  • global_cardinality/2
    The support for the builtin global_cardinality/2 is broken. The following error occurs: 
    ! Existence error
! `global_cardinality/2' is not defined
    Example: sudoku_gcc.mzn.

    There is an easy fix which works but is slower that using an builtin support: in the file globals.mzn (in the SICStus Prolog distribution), just use the decomposition variant (the commented) instead.
  • cumulative
    For the model furniture_moving.mzn the following error occurs: 
    ! Instantiation error in argument 2 of user:cumulative/2
! goal:  cumulative([task(_4769,30,_4771,3,1),task(_4777,10,_4779,1,2),task(_4785,15,_4787,3,3),task(_4793,15,_4795,2,4)],[limit(_4801)])
    Note: the model cumulative_test_mats_carlsson.mzn works without problem (this is a simple example from one of Mats Carlsson's lecures).
  • integer overflow
    For the Grocery example (grocery.mzn) an integer overflow error is thrown: 
    ! Item ending on line 3:
! Representation error in argument 1 of user:range_to_fdset/2
! CLPFD integer overflow
! goal:  range_to_fdset(1..359425431,_4771)
    Notes: MiniZinc's solver also overflows, so this is probably not a big thing. The solvers for Gecode/FlatZinc and ECLiPSe ic handles this problems correctly, though.
  • Statistics
    I have not seen any relevant statistics (e.g. number of failures, nodes, propagations etc) for the SICStus MiniZinc solver. The standard SISCtus Prolog predicate statistics/0 is somewhat useful, but is not what is needed when writing MiniZinc models and comparing with other versions and/or solvers.

    What I have in mind is something like the statistics from Gecode (and Gecode/FlatZinc): 
    runtime:       50
solutions:     1
propagators:   8
propagations:  3995
nodes:         249
failures:      124
peak depth:    12
peak memory:   27 KB

Final note

I have contacted the developers of SICStus Prolog about these things. They responsed that the bugs are now fixed and will be included in the next version (4.0.6). They also indicated that more detailed statistics may make it in a later version. That is great!

I have now also added the SICStus Prolog solver on my MiniZinc page.

Posted by hakank at 08:48 AM |