« MiniZinc/FlatZinc support in SICStus Prolog version 4.0.5 | Main | My talk at SweConsNet Workshop 2009: "Learning Constraint Programming (MiniZinc, JaCoP, Choco, Gecode/R, Comet, Gecode): Some Lessons Learned" »

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.

Comments

I would guess that the agatha-problem is easier to specify using set variables. The rows in the hates and richer specify sets using the Boolean signature. The rule that Charles hates noone that Agatha hates, for example, is equivalent to an empty intersection between hates[agatha] and hates[charles].

Mikael: Thanks for the suggestion about the Agatha problem. I will give it a try.

Post a comment

(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)