Main

September 27, 2013

Charles Prod'homme blogs about developing Choco

One week ago, Charles Prod'homme (one of the main developers of the Choco CP system) started the blog Within a Constraint Solver. His first blog post was this:
With this blog I would like to share the good and bad ideas we've had (and have) while developing our constraint solver. As we almost started from scratch, there could be articles about every part of the solver. If you don't know what Constraint Programming is, wikipedia is a good start point.

Since 2008, I've been working on Choco, a Java library for constraint programming. Articles from this blog will mostly talk about the choices made from the version 2 to version 3, but not only.
Welcome to the CP blog sphere, Charles!

A side note: Some days before Charles started his blog, I held a talk at CP-2013 Workshop CP Solvers: Modeling, Applications, Integration, and Standardization, and one of the things I mentioned was that it would be great if there where more CP bloggers to explain what Constraint Programming is and why we are so fascinated by it. I'm not sure is there is some cause and effect here or just a happy coincidence. :-)

If you are interested, here is my talk: CP Solvers/Learning Constraint Programming, and here's Charles' talk at the workshop: Choco3: an Open Source Java Constraint Programming Library.

December 19, 2009

Choco's new site

Soon the website for Choco constraint programming solver will be changed to a this site (will replace the old one). There are some broken links and missing information, but it seems to be well organized.

Some links: For anyone not familiar with Choco, here is a short description (from the new site):
choco is a java library for constraint satisfaction problems (CSP), constraint programming (CP) and explanation-based constraint solving (e-CP).
It is built on a event-based propagation mechanism with backtrackable structures.

choco can be used for:

* teaching (a user-oriented constraint solver with open-source code)
* research (state-of-the-art algorithms and techniques, user-defined constraints, domains and variables)
* real-life applications (many application now embed choco)

August 23, 2009

Java Specification Requests JSR 331: Constraint Programming API

The Java Specification Request JSR 331: Constraint Programming API is a request for consolidating the Java constraint solvers.
This specification defines a Java runtime API for constraint programming. The CP API prescribes a set of fundamental operations used to define and solve constraint satisfaction and optimization problems.

The request

2.1 Please describe the proposed Specification:

This specification defines a Java runtime API for constraint programming. The standardized CP API aims to make CP technology more accessible for business software developers. It intends to create CP Standards that will define unified business interface(s) for modeling and solving real-world decision support problems as Constraint Satisfaction and Optimization Problems. Having unified interfaces will allow commercial application developers to model their problems in such a way that the same model can be tried with different CP Solvers. This will minimize vendor dependence without limiting vendor's innovation. At the same time the CP API will help to bring the latest research results to real-world business applications. The CP API prescribes a set of fundamental operations used to define and solve constraint satisfaction and optimization problems. The sets of operations will allow a user to express its decision support problem in terms of:
- Decision Variables defined as constrained integer, real, and set variables
- Constraints defined on these variables using the standardized unary, binary and global constraints.
Clearly separating the problem definition from problem resolution, the sets of operations will allow a user to apply standardized search strategies to find feasible and optimal solutions of the problem. The CP API will also allow a user to create custom constraints and search strategies in a unified way making them independent from a particular CP solver.

...

2.6 Why isn't this need met by existing specifications?

Today CP is a proven optimization technique and many CP solvers empower real-world business applications in such areas as scheduling, planning, configuration, resource allocation, and real-time decision support. However, the absence of standards still limits the acceptance of CP by the business world.

While dissimilar vendor-specific CP API specifications exist, their syntactic and semantic differences are significant enough to cause costly difficulties for application builders and platform vendors.

The development schedule

2.13 Please describe the anticipated schedule for the development of this specification.

1. Early Draft Review: November 20, 2009

2. Complete the Specification, Public Draft/Final Release: April 15, 2010

3. Maintenance Review: June 30, 2010

2.14 Please describe the anticipated working model for the Expert Group working on developing this specification.

The JSR Specification Lead has already contacted major CP vendors and well-known CP experts and involved them in a preliminary discussion at www.cpstandards.org. We will invite them to join the Expert Group right after the initial JSR Review and acceptance. We plan to have an kick-off meeting during the oncoming major CP conference CP-2009 that will take place at Portugal on 20-24 September 2009. A preliminary Java CP API that will become a basis for the JSR is being discussed by CP experts at the Discussion Forum at www.cpstandards.org. During the first 3 months we plan to finalize the Expert Group that will include the most active contributors to the Early Draft.

Related

Other pages of interest:
* JSR #331 Constraint Programming API - JSR Review Ballot * Public forum for JSR 331.
* Standardization of Constraint Programming (www.cpstandards.org), forum with some discussion about the JSR

Also, see:
* My Choco page
* My JaCoP page
* My constraint programming page

June 24, 2009

My old swedish blog posts about constraint programming translated (via Google)

Before starting this blog (i.e. My Constraint Programming blog) late December 2008, I blogged about constraint programming in my Swedish blog hakank.blogg). Translations of those Swedish blog post has not been collected before, and now it is time.

So, here are links to most of the blog posts from the category Constraint Programming, translated via Google's Language Tools. Most of the translation is intelligible, but if you have some questions about some particular, please feel to mail me: hakank@bonetmail.com for more information.


November 4, 2005
Swedish: Sesemans matematiska klosterproblem samt lite Constraint Logic Programming
Translated: Sesemans kloster mathematical problems and little Constraint Logic Programming ("kloster" means "convent").


April 18, 2006
Swedish: Choco: Constraint Programming i Java
Translated: Choco: Constraint Programming in Java


The two post above was written when I had just a cursory interest in constraint programming. From about February 2008 and onward, it became my main interest.


April 5, 2008
Swedish: Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc,
Translated: Constraint Programming: Minizinc, Gecode / flatzinc and ECLIPSE / minizinc.


April 14, 2008
Swedish: MiniZinc-sida samt fler MiniZinc-exempel
Translated: MiniZinc-page and multi-MiniZinc example.


April 21, 2008
Swedish: Applikationer med constraint programming, lite om operations research samt nya MiniZinc-modeller
Translated: Applications of constraint programming, a little of operations research and new MiniZinc models


April 26, 2008
Swedish: Ett litet april-pyssel
Translated: A small-craft in April (a better translation would be "A small April puzzle")


April 27, 2008
Swedish: Mitt OpenOffice Calc-/Excel-skov
Translated: My Open Office Calc-/Excel-skov (better translation: My Open Office Calc-/Excel period).


May 26, 2008
Swedish: Några fler MiniZinc-modeller, t.ex. Smullyans Knights and Knaves-problem
Translated: Some more MiniZinc models, eg Smullyans Knights and Knaves-problem Smullyans Knights and Knaves problem


June 2, 2008
Swedish: MiniZinc/FlatZinc version 0.8 släppt
Translated: MiniZinc / FlatZinc version 0.8 released


June 2, 2008
Swedish: Nya MiniZinc-modeller, flera global constraints, däribland clique
Translated: New MiniZinc models, several global constraints, including Clique


June 5, 2008
Swedish: Mats Anderssons tävling kring fotbolls-EM 2008 - ett MiniZinc-genererat tips
Translated: Mats Andersson racing around championship in 2008 - a MiniZinc-generated tips (it is about a competition how to predict Soccer World Cup 2008 using MiniZinc)


June 24, 2008
Swedish: Tre matematiska / logiska pyssel med constraint programming-lösningar: n-puzzle, SETS, M12 (i MiniZinc)
Translated: Three mathematical / logical craft with constraint programming solutions: n-puzzle, SETS, M12 (in MiniZinc) ("craft" should be translated to "puzzles")


June 24, 2008
Swedish: MiniZinc-nyheter
Translated: MiniZinc news


June 29, 2008
Swedish: Gruppteoretisk lösning av M12 puzzle i GAP
Translated: Group Theoretical solution of the M12 puzzle in GAP (well, this is not really a constraint programming solution, but it is another way of solving the M12 puzzle blogged about in June 24)


June 30, 2008
Swedish: Gruppteoretisk lösning av M12 puzzle i GAP - take 2
Translated: Group Theoretical solution of the M12 puzzle in GAP - take 2


July 4, 2008
Swedish: Martin Chlond's Integer Programming Puzzles i MiniZinc
Translated: Martin's Chlond Integer Programming Puzzles in MiniZinc


July 7, 2008
Swedish: Fler MiniZinc modeller kring recreational mathematics
Translated: More MiniZinc models on recreational mathematics


July 20, 2008
Swedish: Fler constraint programming-modeller i MiniZinc, t.ex. Minesweeper och Game of Life
Translated: More constraint programming models in MiniZinc, eg Minesweeper och Game of Life Minesweeper and the Game of Life


August 17, 2008
Swedish: JaCoP - Java Constraint Programming solver
Translated: JaCoP - Java Constraint Programming solver


September 14, 2008
Swedish: Constraint programming i Java: Choco version 2 släppt - samt jämförelse med JaCoP
Translated: Constraint programming in Java: Choco version 2 released - and comparison with JaCoP


September 28, 2008
Swedish: Constraint programming: Fler MiniZinc-modeller, t.ex. Martin Gardner och nonogram
Translated: Constraint programming: More MiniZinc models, eg Martin Gardner och nonogram Martin Gardner and nonogram


December 27, 2008
Swedish: Constraint programming-nyheter samt nya MiniZinc-modeller
Translated: Constraint programming, news and new MiniZinc models


December 29, 2008
Swedish: My Constraint Programming Blog
Translated: My Constraint Programming Blog


After that, entries about constraint programming at my swedish blog posts where just summaries of the stuff written here at My Constraint Programming blog.

June 13, 2009

Miscellaneous news

Here are some miscellaneous news.

Choco

Version 2.1

I have forgot to mention that Choco have released version 2.1 . Download this version via the download page. The Sourceforge download page is here.

Changed models for version 2.1

I have changed some of my Choco models for version 2.1. The biggest change was the use of cumulative in FurnitureMoving.java where the call to the cumulative constraint have changed and now use TaskVariable.

I added the following
// Create TaskVariables
TaskVariable[] t = new TaskVariable[starts.length];
   for(int i = 0; i < starts.length; i++){
      t[i] = makeTaskVar("", starts[i], ends[i], durations[i]);
   }
and changed the call to cumulative to:
 
m.addConstraint(cumulative(null, t, constantArray(_heights), constant(NumPersons)));
Also, the line
durations[i] = makeConstantVar("durations" + i, durationsInts[i]);
was changed to
durations[i] = makeIntVar("durations" + i, durationsInts[i], durationsInts[i]);
For some of the other models (compiled for version 2.0.*), I just recompiled the source and it worked without any change in the code.

MiniZinc

List of global constraints

At the MiniZinc site, there is now a list of the supported global constraints in MiniZinc: MiniZinc: Global Constraints.

MiniZinc Library

MiniZinc Library is a great collections of problems, examples, and tests. (For some reason is not linked from the main MiniZinc site.)

Output in Minizinc

I wrote here about the change of output in MiniZinc version 1.0 . Only the distributed solver minizinc supports the output statement (for some kind of "pretty printing" of the output), but the solvers using the FlatZinc format has no such support. Since I want to see matrices presented in a normal way for all solvers, I wrote a simple Perl program to show matrices more pretty than just a single line. Also, single arrays are shown without array1d(...).

The Perl program is mzn_show.pl and it simply takes the result from a solver and reformats the result.

An example: The output from the debruijn_binary.mzn from a solver using FlatZinc file, such as Gecode/FlatZinc and MiniZinc's fdmip is:
bin_code = array1d(1..8, [0, 0, 0, 0, 1, 0, 1, 1]);
binary = array2d(1..8, 1..4, [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0]);
x = array1d(1..8, [0, 1, 2, 5, 11, 6, 12, 8]);
When filtering this with mzn_show.pl it will be shown as:
bin_code: 0 0 0 0 1 0 1 1
% binary = array2d(1..8, 1..4, [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0]);
binary:
  0 0 0 0
  0 0 0 1
  0 0 1 0
  0 1 0 1
  1 0 1 1
  0 1 1 0
  1 1 0 0
  1 0 0 0
x: 0 1 2 5 11 6 12 8
Very simple, but quite useful.

Somewhat related: The NEWS file of the latest ROTD (Release of The Day) states the following:
FlatZinc output processing tool

We have added a new tool, solns2dzn, that can be used to process the output of FlatZinc implementations in various ways. For example, it can extract each individual solution and write it to a separate file.
This program is distributed as source (Mercury), not as an executable, so I have not been able to test it.

Hidato and exists

In the hidato.mzn model I have changed the exists construct
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]
     )
  )
)
to a a version using just var ints:
forall(k in 1..r*c-1) (
    let {
       var 1..r: i,
       var 1..c: j,
       var {-1,0,1}: a,
       var {-1,0,1}: b
    }
    in
    k = x[i, j] % fix this k
    /\
    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]
)
This replacement of exists with int vars, if possible, seems to always be more effective.

However, there is one use of exists where it is harder to replace in this way. As an example, take Pandigital numbers in any base (the model includes a presentation of the problem) where - among other things - we want to find some array indices of the integer array x in order to find the positions of three numbers num1, num2 and res (the result of num1 * num2).
% num1. 
exists(j in 1..x_len) (
   j = len1 /\
   toNum([x[i] | i in 1..j], num1, base)
)

/\  % num2
exists(j, k in 1..x_len) (
   j = len1+1 /\ 
   k = len1+len2 /\ k > j  /\
   toNum([x[i] | i in j..k], num2, base)
)

/\ % the product
exists(k in 1..x_len) (
   k = len1+len2+1 /\
   toNum([x[i] | i in k..x_len], res, base)
)
Using this approach, we have to use exists since indices in a range (e.g. j in 1..j) must not be an int var.

Also

Both Choco and MiniZinc sites now have links to my site, which is quite fun:
* Choco, Users (last)
* MiniZinc and FlatZinc (also last)

Work related page in english

The page Håkan Kjellerstrand, CV and work related interests is a english version of my work related page. (The original, swedish, version is here.)

May 09, 2009

Learning Constraint Programming IV: Logical constraints: Who killed Agatha? revisited

Here is a comparison of how different constraint programming systems implements the logical constraints in the problem Who Killed Agatha?, also known as The Dreadsbury Mansion Murder Mystery.. In Learning constraint programming - part II: Modeling with the Element constraint the problem was presented and showed how the systems implements the Element constraints.

Problem formulation from The h1 Tool Suite
Someone in Dreadsbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only ones to live there. A killer always hates, and is no richer than his victim. Charles hates noone that Agatha hates. Agatha hates everybody except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone whom Agatha hates. Noone hates everyone. Who killed Agatha?
Originally from F. J. Pelletier: Seventy-five problems for testing automatic theorem provers., Journal of Automated Reasoning, 2: 191-216, 1986.

Here we see compare how different constraint programming systems implement the three emphasized conditions in the problem formulation above:
  • the concept of richer
  • Charles hates noone that Agatha hates
  • No one hates everyone
All models defines the concepts of hates and richer as two matrices. The matrix declarations are omitted in the code snippets below.

Models

Here are the different models for the Who killed Agatha? problem. JaCoP and Choco has two version for how to implement the Element constraint, see the link above. Also, there is no Gecode/R version of this problem.

Defining the concept of richer

First we define the concept of richer, which consists of two parts:
  • No one is richer than him-/herself
  • if i is richer than j then j is not richer than i
This is an antisymmetric relation which is explored somewhat more (with an alternative predicate of the concept) in the MiniZinc model antisymmetric.mzn.

The logical concept used here is equivalence (if and only of).

MiniZinc

% define the concept of richer: no one is richer than him-/herself
forall(i in r) (
   richer[i,i] = 0
)

/\ % if i is richer than j then j is not richer than 
forall(i, j in r where i != j) (
   richer[i,j] = 1 <-> richer[j,i] = 0
)

Comet

Note that Comet don't have support for equivalence directly, instead we have to use two implications. Update: equivalence in Comet is written as == (I tested <=> which didn't work). Thanks to Pascal Van Hentenryck for pointing this out.
// no one is richer than him-/herself
forall(i in r)
  m.post(richer[i,i] == 0);

// if i is richer than j then j is not richer than i
forall(i in r, j in r : i != j) {
  /* earlier version: two implications
  m.post(richer[i,j] == 1 => richer[j,i] == 0);
  m.post(richer[j,i] == 0 => richer[i,j] == 1);
  */
  // equivalence
  m.post((richer[i,j] == 1) == (richer[j,i] == 0));
}

JaCoP

//  no one is richer than him-/herself
for(int i = 0; i < n; i++) {
    store.impose(new XeqC(richer[i][i], 0));
}

//  if i is richer than j then j is not richer than i
for(int i = 0; i < n; i++) {
    for(int j = 0; j < n; j++) {
        if (i != j) {
             store.impose(
                          new Eq(
                                 new XeqC(richer[i][j], 1),
                                 new XeqC(richer[j][i], 0)
                                 )
                          );

        }
    }
}

Choco

//   a) no one is richer than him-/herself
for(int i = 0; i < n; i++) {
    m.addConstraint(eq(richer[i][i], 0));
}

//   b) if i is richer than j then j is not richer than i
for(int i = 0; i < n; i++) {
    for(int j = 0; j < n; j++) {
        if (i != j) {
             m.addConstraint(
                             ifOnlyIf(
                                    eq(richer[i][j], 1),
                                    eq(richer[j][i], 0)
                                      )
                             );
        }
    }
}

Gecode

// no one is richer than him-/herself
for(int i = 0; i < n; i++) {
  rel(*this, richer_m(i,i), IRT_EQ, 0, opt.icl());
}

// if i is richer than j then j is not richer than i
for(int i = 0; i < n; i++) {
  for(int j = 0; j < n; j++) {
    if (i != j) {
      post(*this, tt(
              eqv(
                 richer_m(j,i) == 1, // <=>
                 richer_m(i,j) == 0)), 
                 opt.icl());
    }
  }
}

Charles hates noone that Agatha hates

Here is the definitions of the condition Charles hates noone that Agatha hates, which simply mean the implication:
  if Agatha hates X then Charles don't hate X

MiniZinc

When starting to modeling these kind of problems, I tend to follow the order of the conditions, which here means that the Charles part is before the Agatha part. When remodeling in another system the order tends to be fixed (cf the Comet version).
forall(i in r) (
   hates[charles, i] = 0 <- hates[agatha, i] = 1
)

Comet

forall(i in r)
  m.post(hates[agatha, i] == 1 => hates[charles, i] == 0);

JaCoP

for(int i = 0; i < n; i++) {
    store.impose(
                 new IfThen(
                            new XeqC(hates[agatha][i], 1),
                            new XeqC(hates[charles][i], 0)
                            )
                 );
}

Choco

I tend to copy/paste the models for Choco and JaCoP and just change the functions that are different. A consequence of this is that some special feature in one of these two systems is not used.
for(int i = 0; i < n; i++) {
    m.addConstraint(
                    implies(
                            eq(hates[agatha][i], 1),
                            eq(hates[charles][i], 0)
                            )
                    );
}

Gecode

for(int i = 0; i < n; i++) {
   post(*this, tt(
                  imp(
                        hates_m(i,agatha) == 1, 
                        // =>
                        hates_m(i,charles) == 0)), 
                        opt.icl());
}

No one hates everyone

This is the last condition to compare: No one hates everyone. It is implemented by a sum of the number of persons that each person hates, and this sum must be 2 or less. Note that it is possible to hate oneself.

MiniZinc

forall(i in r) (
  sum(j in r) (hates[i,j]) <= 2  
)

Comet

  forall(i in r) 
    m.post(sum(j in r) (hates[i,j]) <= 2);

JaCoP

Note: We could save the XlteqC constraint by restrict the domain of a_sum to 0..2 instead of 0..n (=3) but this explicit use of XlteqC is more clear.
for(int i = 0; i < n; i++) {
    FDV a[] = new FDV[n];
    for (int j = 0; j < n; j++) {
        a[j] = new FDV(store, "a"+j, 0, 1);
        a[j] = hates[i][j];
    }
    FDV a_sum = new FDV(store, "a_sum"+i, 0, n);
    store.impose(new Sum(a, a_sum));
    store.impose(new XlteqC(a_sum, 2));
}

Choco

Note: sum is an operator, which makes the condition somewhat easier to state than in JaCoP.
for(int i = 0; i < n; i++) {
    IntegerVariable a[] = makeIntVarArray("a", n, 0, 1);
    for (int j = 0; j < n; j++) {
        a[j] = hates[i][j];
    }
    m.addConstraint(leq(sum(a), 2));
}

Gecode

In Gecode this condition is quite easy to state by using linear. In order to use this there is a Matrix "view" of the hates matrix hates_m.
Matrix hates_m(hates, n, n);
// ...
for(int i = 0; i < n; i++) {
  linear(*this, hates_m.row(i), IRT_LQ, 2, opt.icl());
}

End comment

The mandatory end comment: There are probably better ways of modeling the problem than shown above, either by changing some details or by model the problem completely different. Maybe this will be done sometime...

May 08, 2009

Learning Constraint Programming III: decomposition of a global constraint: alldifferent_except_0

The series Learning Constraint Programming is a preparation for My talk at SweConsNet Workshop 2009: "Learning Constraint Programming (MiniZinc, JaCoP, Choco, Gecode/R, Comet, Gecode): Some Lessons Learned". Confusingly, the entries is not numbered in any logical order. Sorry about that.

Here are the previous entries:

Introduction

The global constraint alldifferent_except_0 (or the more general variant alldifferent_except_c) is one of my favorite global constraints. It is very handy to use when 0 (or any constant c) is coded as an unknown or irrelevant value. Then we can constraint the rest to be all distinct.

The great Global Constraint Catalog entry alldifferent_except_0) explains this constraint as:
Purpose
Enforce all variables of the collection VARIABLES to take distinct values, except those variables that are assigned to 0.

Example
​(<5,​0,​1,​9,​0,​3>)​
The alldifferent_except_0 constraint holds since all the values (that are different from 0) 5, 1, 9 and 3 are distinct.

Models

I have modeled a decomposition of alldifferent_except_0 in the following models, where the constraint is just tested perhaps combined with some other constraint, e.g. sorted or that there must be at least some zeros:

- MiniZinc alldifferent_except_0.mzn
- Comet: alldifferent_except_0.co
- Gecode/R: all_different_except_0.rb
- Choco: AllDifferentExcept0_test.java
- JaCoP: AllDifferentExcept0_test.java
- Gecode: alldifferent_except_0.cpp

Some models using alldifferent_except_0

And here is some real use of the constraint:

- Nonogram (Comet): nonogram.co. (A faster model using the regular constraint, nonogram_regular.co, is described here and here).
- I wrote about alldifferent_except_0 in Pi Day Sudoku 2009. However, as faster way of solving the problem was found and is described in Solving Pi Day Sudoku 2009 with the global cardinality constraint). Note: the competition is still on, so there is no link to any model.
- Sudoku generate (Comet): sudoku_generate.co
- all paths graph (MiniZinc): all_paths_graph.mzn
- Cube sum (MiniZinc): cube_sum.mzn
- Message sending (MiniZinc): message_sending.mzn

As the first two entries indicates, there may be faster solutions than using (a decomposition) of alldifferent_except_0, but even as a decomposition is a great conceptual tool when modeling a problem.

Implementations

In the implementations below we also see how to define a function (predicate) in the constraint programming systems.

For the Gecode/R model there are different approaches:
- "standard" ("direct") approach where we loop over all different pairs of elements and ensures that if both values are different from 0 then they should be different
- using count
- using global cardinality ("simulated" in Gecode/R, see below)

Also, in some models we use the slighly more general version alldifferent_except_c where c is any constant (e.g. "Pi" in the Pi Day Sudoku puzzle mentioned above.

MiniZinc:

Model: alldifferent_except_0.mzn.
predicate all_different_except_0(array[int] of var int: x) =
   let {
      int: n = length(x)
   }
   in
   forall(i,j in 1..n where i != j) (
        (x[i] > 0 /\ x[j] > 0) 
        -> 
        x[i] != x[j]
   )
;

// usage:
constraint all_different_except_0(x);

Comet:

Model: alldifferent_except_0.co.
function void alldifferent_except_0(Solver m, var{int}[] x) {
  int n = x.getSize();
  forall(i in 1..n, j in i+1..n) {
    m.post(
           x[i] > 0 && x[j] > 0 
           => 
           x[i] != x[j]
           );
  }
}

// usage
exploreall {
  // ...
  alldifferent_except_0(m, x);
}

Gecode/R

Model:all_different_except_0.rb.

When modeling the constraint in Gecode/R, I experimented with different approaches. The reification variant all_different_except_0_reif is actually quite fast.
# The simplest and the fastest implementation 
# using count for 1..max (poor man's global cardinality)
def all_different_except_0
  (1..self[0].domain.max).each{|i|
    self.count(i).must <= 1
  }
end

# global cardinality version using an extra array with the counts
def global_cardinality(xgcc)
  (self[0].domain.max+1).times{|i|
    xgcc[i].must == self.count(i)
  }
end

#
# The standard approach using reification.
#
def all_different_except_0_reif(x)
  n = x.length
  b1_is_an bool_var_matrix(n,n)
  b2_is_an bool_var_matrix(n,n)
  b3_is_an bool_var_matrix(n,n)
  n.times{|i|
    n.times{|j|
      if i != j then 
        x[i].must_not.equal(0, :reify => b1[i,j]) 
        x[i].must_not.equal(0, :reify => b2[i,j]) 
        x[i].must_not.equal(x[j], :reify => b3[i,j])
        (b1[i,j] & b2[i,j]).must.imply(b3[i,j])
      else 
        b1[i,j].must.true
        b2[i,j].must.true
        b3[i,j].must.true
      end
    }
  }
end

    # ...
    # usage:
    x.all_different_except_0
    # all_different_except_0_gcc(x)
    # all_different_except_0_reif(x)

Choco

Model: AllDifferentExcept0_test.java.

Note that here alldifferent_except_0 is derived from the more general version alldifferent_except_c.
//
// decomposition of alldifferent except 0
//
public void allDifferentExcept0(CPModel m, IntegerVariable[] v) {
    allDifferentExceptC(m, v, 0);
}

//
// slightly more general: alldifferent except c
//
public void allDifferentExceptC(CPModel m, IntegerVariable[] v, int c) {
    int len = v.length;
    for(int i = 0; i < v.length; i++) {
        for(int j = i+1; j < v.length; j++) {
            m.addConstraint(ifThenElse(
                                       and(
                                           gt(v[i], c), 
                                           gt(v[j], c)
                                           ), 
                                       neq(v[i], v[j]),
                                       TRUE
                                       )
                            );
        }
    }    
}

// ...
// usage: 

    m.addConstraint(allDifferent(queens));

JaCoP

Model: AllDifferentExcept0_test.java

This is exactly the same approach as the Choco version.
//
// decomposition of alldifferent except 0
//
public void allDifferentExcept0(FDstore m, FDV[] v) {
    allDifferentExceptC(m, v, 0);
} // end allDifferentExcept0


//
// slightly more general: alldifferent except c
//
public void allDifferentExceptC(FDstore m, FDV[] v, int c) {
    int len = v.length;
    for(int i = 0; i < v.length; i++) {
        for(int j = i+1; j < v.length; j++) {
            m.impose(new IfThen(
                                       new And(
                                           new XneqC(v[i], c), 
                                           new XneqC(v[j], c)
                                           ), 
                                       new XneqY(v[i], v[j])
                                       )
                            );
        }
    }        
} // end allDifferentExceptC


        // ...
        // usage:
        allDifferentExcept0(store, x);

Gecode

alldifferent_except_0.cpp

The Gecode version is very succint since it use overloaded boolean operators. Very nice.
void alldifferent_except_0(Space& space, IntVarArray x, 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] != 0 && x[j] != 0, 
           // =>
           x[i] != x[j])),
           icl
           );
    }
  }
} // alldifferent_except_0


// ...
// usage:
    alldifferent_except_0(*this, x, opt.icl());

May 05, 2009

Learning constraint programming - part II: Modeling with the Element constraint

As indicated last in Learning constraint programming (languages) - part I here are some findings when implementing Crossword, Word square, and Who killed Agatha?. See links below for the implementations.

Spoiled
The first constraint programming system i learned after constraint logic programming in Prolog was MiniZinc. When implemented the problems below I realized that I have been quite spoiled by using MiniZinc. The way MiniZinc (and also Comet) supports the Element constraint, i.e. access of variable arrays/matrices, is very straightforward in these systems and it doesn't matter whether the array to access is an array of integers or of non-variable variable integers. In the Java (Choco, JaCoP) and C++ systems (Gecode), however, this is another matter. Due to different circumstances I have not implemented these models in Gecode/R.

Element in MiniZinc and Comet
Accessing arrays and matrices in MiniZinc and Comet is simply done by using the [] construct, no matter what the type of the array or the index are (I assume integers and variable integers here). For the other systems we must explicitly use the Element constraint (called nth in Choco).

Crossword

This is a standard constraint programming problem, used as a running example in Apt's great book Principles of Constraint Programming. Here is a formulation of the problem (stated differently than in the book):
Place the words listed below in the following crossword. The '#' means a blocked cell, and the numbers indicate the overlappings of the words.

      1   2   3   4   5
    +---+---+---+---+---+
  1 | 1 |   | 2 |   | 3 |
    +---+---+---+---+---+
  2 | # | # |   | # |   |
    +---+---+---+---+---+
  3 | # | 4 |   | 5 |   |
    +---+---+---+---+---+
  4 | 6 | # | 7 |   |   |
    +---+---+---+---+---+
  5 | 8 |   |   |   |   |
    +---+---+---+---+---+
  6 |   | # | # |   | # |
    +---+---+---+---+---+
                         
We can use the following words
* AFT * ALE * EEL * HEEL * HIKE * HOSES * KEEL * KNOT * LASER * LEE * LINE * SAILS * SHEET * STEER * TIE

Models


MiniZinc: crossword.mzn
Choco: CrossWord.java
JaCoP: CrossWord.java
Gecode/R: (Not implemented)
Comet: crossword.co
Gecode: crossword.cpp

Note: I have seen more general models for solving crossword problems in Choco, JaCoP, Gecode/R, and Gecode with constructions other that the simple Elements used here. Since I wanted to compare the same way of solving the problem using the same Element-construct this may be an unfair comparison between the systems. Well, this is at least a finding how to implement this problem by Element...

Explanation of variables
The matrix A is the individual chars of the words (Comet variant):
int A[1..num_words,1..word_len] = 
  [
   [h, o, s, e, s], //  HOSES
   [l, a, s, e, r], //  LASER
   [s, a, i, l, s], //  SAILS
   [s, h, e, e, t], //  SHEET
   [s, t, e, e, r], //  STEER
   [h, e, e, l, 0], //  HEEL
   [h, i, k, e, 0], //  HIKE
   [k, e, e, l, 0], //  KEEL
   [k, n, o, t, 0], //  KNOT
   [l, i, n, e, 0], //  LINE
   [a, f, t, 0, 0], //  AFT
   [a, l, e, 0, 0], //  ALE
   [e, e, l, 0, 0], //  EEL
   [l, e, e, 0, 0], //  LEE
   [t, i, e, 0, 0]  //  TIE
];
overlapping is the matrix of the overlapping cells)
This is the Comet version:
[
 [1, 3, 2, 1],   //  s
 [1, 5, 3, 1],   //  s 
  
 [4, 2, 2, 3],   //  i
 [4, 3, 5, 1],   //  k
 [4, 4, 3, 3],   //  e
  
 [7, 1, 2, 4],   //  l
 [7, 2, 5, 2],   //  e
 [7, 3, 3, 4],   //  e
  
 [8, 1, 6, 2],   //  l
 [8, 3, 2, 5],   //  s
 [8, 4, 5, 3],   //  e
 [8, 5, 3, 5]    //  r
 ];
E is the variable array of which the word to use for the different overlappings. This is in fact the only variable (array) that is needed in the problem, apart from the utility/convenience variables.

The main constraint for the crossword example in each system is stated thus:

MiniZinc:
forall(i in 1..num_overlapping) (
   A[E[overlapping[i,1]], overlapping[i,2]] =  A[E[overlapping[i,3]], overlapping[i,4]]
)
Comet:
  forall(i in 1..num_overlapping) {
    cp.post(A[E[overlapping[i,1]], overlapping[i,2]] ==  A[E[overlapping[i,3]], overlapping[i,4]], onDomains);
  }
Choco:
Note that Choco has a special Element which support two dimensional arrays (matrix), which we use.
for(int I = 0; I < num_overlapping; I++) {
  IntegerVariable tmp = makeIntVar("tmp" + I, 1, 26);
  M.addConstraint(nth(E[overlapping[I][0]], W[overlapping[I][1]], AX, tmp));
  M.addConstraint(nth(E[overlapping[I][2]], W[overlapping[I][3]], AX, tmp));
}
JaCoP:
Here we had used some trickery by using a transposed version of the word matrix since JaCoP has no special Element constraint for two dimensional arrays.
for (int I = 0; I < num_overlapping; I++) {
   FDV tmp = new FDV(store, "TMP" + I, 0, num_words*word_len);
   store.impose(new Element(E[overlapping[I][0]], words_t[overlapping[I][1]], tmp));
   store.impose(new Element(E[overlapping[I][2]], words_t[overlapping[I][3]], tmp));
}
Gecode:
This is more complicated compared to the two Java systems since in Gecode we use an array (of length rows*cols) to simulate the matrix. (There is a Matrix "view" in Gecode but the indices must be of type integer, not IntVar, so it can not be used.) Also, the constraints plus and mult takes IntVar as argument.

The first overlapped crossing is "expanded" like this (Gecode is 0-based):
   A[E[overlapping[i,0]], overlapping[i,1]] // MiniZinc/Comet
   =>
   a1 = A[ E[I*4+0] * word_len + overlapping[I*4+1]] // Gecode
Here is the complete code. The comments hopefully explains what is going on.

First we define an utility function for accessing the element according to the above principle.
/**
 *
 * Special version of element for an array version of a "matrix" words,
 * E is an integer variable array, C is an array of IntVars for
 * the offset j in the words "matrix".
 *
 * The call 
 *    element_offset(*this, words, E[i], word_len_v, C[j], res, opt.icl());
 *
 * corresponds to:
 *    res = words[E[i], j] --> words[E[i]*word_len+J]
 *
 */
void element_offset(Space& space,
                   IntArgs words,
                   IntVar e,
                   IntVar word_len,
                   IntVar c,
                   IntVar res,
                   IntConLevel icl = ICL_DOM) {

      element(space, words, 
              plus(space, 
                   mult(space, 
                        e, 
                        word_len, icl), 
                   c, icl), 
              res, icl);
}

The function is then used as follows:
for(int I = 0; I < num_overlapping; I++) {
   IntVar e1(*this, 0, num_overlapping*4);
   IntVar e2(*this, 0, num_overlapping*4);

   IntVarArray o(*this, 4, 0, num_overlapping*4);
   for(int J = 0; J < 4; J++) {
     post(*this, o[J] == overlapping[I*4+J], opt.icl());
   }

   element(*this, E, o[0], e1, opt.icl());      // e1 = E[I*4+0]
   element(*this, E, o[2], e2, opt.icl());      // e2 = E[I*4+2]

   IntVar a1(*this, 0, num_words*word_len);
      
   element_offset(*this, A, e1, word_len_v, o[1], a1, opt.icl());
   element_offset(*this, A, e2, word_len_v, o[3], a1, opt.icl());
}
(The same element_offset function is also used in the word_square problem below.) It took quite a time to get the function and temporary variables (and their domains) right. With training (and the element_offset as a skeleton) similiar problems should be easier to implement.

Note: this is not a bashing of Gecode. Gecode is a great system and it happens that for this specific problem, Gecode does not has the appropriate support. I should also mention that it was a long time since I programmed in C++ and am little rusty.

As mentioned earlier, I have been very spoiled by the MiniZinc (and Comet) constructs. Also: I'm a very 'lazy' person (in the Perl sense of the word lazy) and likes the agile programming languages - Perl, Ruby, Python etc - much for their high level constructs.

Word square problem

The word problem is a cousin to the crossword problem, and is described in Wikipedia's Word_square:
A word square is a special case of acrostic. It consists of a set of words, all having the same number of letters as the total number of words (the "order" of the square); when the words are written out in a square grid horizontally, the same set of words can be read vertically.
An example of order 7 found by the Comet model where we see that the first row word (aalborg) is also the first column word.

aalborg
abaiser
lantaca
bittman
osamine
recanes
granese

Models

Here are the models for solving the Word square problem:
MiniZinc: word_square.mzn
Choco: WordSquare.java
JaCoP: WordSquare.java
Gecode/R: (Not implemented it Gecode/R)
Comet: word_square.co
Gecode: word_square.cpp

It is somewhat easier than the crossword problem. As before, E is the array of the index of the words to use, and words is an matrix of the words. Also, these models is an experiment of how to read a file, the word list /usr/dict/words (standard on Unix/Linux systems).

MiniZinc
forall(I, J in 1..word_len) (
  words[E[I], J] = words[E[J],I]
)
Comet
  forall(i in 1..word_len) {
    forall(j in 1..word_len) {    
      cp.post(words[E[i], j] == words[E[j],i], onDomains);
    }
  }
JaCoP
// 
// The overlappings (crossings).
// Note that we use a transposed word matrix for the Element.
//
for(int i = 0; i < word_length ; i++) {
    for(int j = 0; j < word_length ; j++) {
        // Comet: words[E[i], j] ==  words[E[j],i]
        FDV tmp = new FDV(store, "tmp" + i + " " + j, 0, dict_size);
        store.impose(new Element(E[i], words[j], tmp));
        store.impose(new Element(E[j], words[i], tmp));
    }
}
Choco
// Constants for the nth constraint below
IntegerVariable [] C = new IntegerVariable[dict_size];
for (int I = 0; I < word_length; I++) {
    C[I] = makeIntVar("C"+I, I,I);
}

// The overlappings (crossings)
for(int I = 0; I < word_length ; I++) {
    for(int J = 0; J < word_length ; J++) {
        // Comet: words[E[i], j] ==  words[E[j],i]
        IntegerVariable tmp = makeIntVar("tmp" + I + " " + J, 0, dict_size);
        M.addConstraint(nth(E[I], C[J], words, tmp));
        M.addConstraint(nth(E[J], C[I], words, tmp));
    }
}
Gecode
Note that this model use the same function element_offset that was used in the Crossword problem. It took some time to realize that it also could be used here.
// convenience variables for the element constraints below
// since element, plus, and mult wants IntVars.
IntVar word_len_v(*this, word_len, word_len);
IntVarArray C(*this, word_len, 0, word_len-1);
for(int i = 0; i < word_len; i++) {
  rel(*this, C[i], IRT_EQ, i, opt.icl());
}

for(int i = 0; i < word_len; i++) {
  for(int j = 0; j < word_len; j++) {
    // words[E[i], j] ==  words[E[j],i]

    IntVar tmp(*this, 0, num_words);

    // tmp == words[E[i], j] --> words[E[i]*word_len+j]
    element_offset(*this, words, E[i], word_len_v, C[j], tmp, opt.icl());

    // tmp == words[E[j], i]  --> words[E[j]*word_len+i]
    element_offset(*this, words, E[j], word_len_v, C[i], tmp, opt.icl());
  }
}

Who killed Agatha?

This is a standard benchmark for theorem proving, also known as The Dreadsbury Mansion Murder Mystery.

Problem formulation from The h1 Tool Suite
Someone in Dreadsbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only ones to live there. A killer always hates, and is no richer than his victim. Charles hates noone that Agatha hates. Agatha hates everybody except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone whom Agatha hates. Noone hates everyone. Who killed Agatha?
Originally from F. J. Pelletier: Seventy-five problems for testing automatic theorem provers., Journal of Automated Reasoning, 2: 191-216, 1986.

Models


MiniZinc: who_killed_agatha.mzn
JaCoP : WhoKilledAgatha.java
JaCoP : WhoKilledAgatha_element.java
Choco: WhoKilledAgatha.java
Choco: WhoKilledAgatha_element.java
Comet: who_killed_agatha.co
Gecode: who_killed_agatha.cpp

In Some new Gecode models I wrote about the findings in implemented this problem in Gecode and compared to Comet/MiniZinc.

The models use two 3x3 matrices for representing the two relations hates and richer with 0..1 as domain (i.e. boolean). The Element constraints is used for implementing the condition A killer always hates, and is no richer than his victim. where the_killer is an integer variable; the_victim is in some models replaced by agatha (the integer 0). The interesting thing here is that at least one of the indices are integer variables, which caused the difficulties in the two problems above.

These models also use a lot of boolean constructs. A comparison of how these are implemented in the different CP systems may be described in a future blog post.

MiniZinc
hates[the_killer, the_victim] = 1 /\
richer[the_killer, the_victim] = 0
Comet:
m.post(hates[the_killer, the_victim] == 1);
m.post(richer[the_killer, the_victim] == 0);
Note: In the models below I have simplified the problem by using agatha (defined as the integer 0) instead of the integer variable the_victim. This is not a problem since we know that Agatha is the victim, and is the reason why the Element is easier to use than for Crossword and Word square.

JaCoP variant 1 (no Element):
JaCoP don't have a direct support for the case when the index i (in matrix[i][j]) is an integer variable so the first variant of modeling the condition A killer always hates, and is no richer than his victim. does not use Element at all. In WhoKilledAgatha.java we simply loop over all integers (0..2), check if "this" i equals the_killer and then we can use two integers for accessing the matrices. Also, note the IfThen construct.
for(int i = 0; i < n; i++) {
    store.impose(
                 new IfThen(
                            new XeqC(the_killer, i),
                            new XeqC(hates[i][agatha], 1)
                            )
                 );
    store.impose(
                 new IfThen(
                            new XeqC(the_killer, i),
                            new XeqC(richer[i][agatha], 0)
                            )
                 );
}
This was the first variant I implemented, but then I recall the "trickery" used in Crossword and Word square where the matrices where transposed and Element could be used. The problem with this approach is that all constraints must be rewritten in a way that may be confusing. Come to think of it, maybe the names of the matrices should have been changed to is_hated_by and poorer.

JaCoP variant 2 (transposed matrices, Element)
This method of transposition and using Element is implemented in WhoKilledAgatha_element.java. The constraint is now much simpler:
int shift = -1;
for(int i = 0; i < n; i++) {
    store.impose(new Element(the_killer, hates[agatha], one, shift));
    store.impose(new Element(the_killer, richer[agatha], zero, shift));
}
Note: the Element in JaCoP defaults to start index as 1, but has support for shifting it to 0, by using -1 as the shift parameter. Choco variant 1 (no Element)
I implemented exact the same principle that was used in the two JaCoP model in the two Choco models. The first - no Element - is WhoKilledAgatha.java:

for(int i = 0; i < n; i++) {
    m.addConstraint(implies(
                            eq(the_killer,i),
                            eq(hates[i][agatha], 1)
                            )
                    );
    m.addConstraint(implies(
                            eq(the_killer, i),
                            eq(richer[i][agatha], 0)
                            )
                    );
}
Choco variant 2 (transposed matrices, nth)
Note: one and zero are integer variables since nth cannot handle plain integers as the last argument.
for(int i = 0; i < n; i++) {
   m.addConstraint(nth(the_killer, hates[agatha], one));
   m.addConstraint(nth(the_killer, richer[agatha], zero)
}

Comments

Here we have seen - not surprisingly - that using the Element constraint is quite different depending of which CP system we use and it can be easy or not so easy. It was my explicit intension to see how to solve the same problem as similiar as possible. We should also note that most (if not all) problems can be modeled in many ways, some not using Element at all.

One last comment: The two Java models of Who killed Agatha? took quite a long time to implement. The main reason for that was not the the handling of Element but was due to a bug of confusing the two matrices in one of the conditions. Sigh.

January 15, 2009

Some models in Gecode/R (Ruby interface to Gecode)

Gecode/R is a great Ruby interface to Gecode (implemented in C++). At last I now have done some modeling in Gecode/R and it's nice.

The models and some other information about Gecode/R can be seen at My Gecode/R page.

Since Ruby is a very high level language, the modelling can be done "high levelish", more so than for example with the Java solvers Choco and JaCoP. And that is a feature I really like.

I'm still learning Gecode/R and have surely missed some stuff. There are not many examples in the package (these are also commented at Examples). Some things have been of great help
* The Sitemap
* The Documentation, especially the RDocs
* The test files in the specs directory.


An example: Survo Puzzle
From Wikipedia's Survo Puzzle


In a Survo puzzle the task is to fill an m * n table by integers 1,2,...,m*n so
that each of these numbers appears only once and their row and column sums are
equal to integers given on the bottom and the right side of the table.
Often some of the integers are given readily in the table in order to
guarantee uniqueness of the solution and/or for making the task easier.

E.g. the puzzle 128/2008 is presented with the following clues:


* * * * * * 30
* * 18 * * * 86
* * * * * * 55
22 11 42 32 27 37

where * marks a digit to find. The number to the right is the row sums which the row must sum to, and the last row is the column sums.

The unique solution of the problem is (by running the program ruby survo_puzzle.rb survo_puzzle_128_2008.txt)


Solution #1
4 1 10 5 3 7 = 30
12 8 18 16 15 17 = 86
6 2 14 11 9 13 = 55
= = = = = =
22 11 42 32 27 37

Statistics:
propagations: 3784
failures: 174
clones: 179
memory: 25740
commits: 461
Number of solutions: 1

The relevant constraint programming code is below (slightly edited). I think it's quite nice.


....
def initialize(clues, rowsums, colsums)
r = rowsums.length # number of rows
c = colsums.length # number of columns
x_is_an int_var_matrix(r, c, 1..r*c) # the solution matrix
x.must_be.distinct # all values in x must be distinct
# values in clues with values > 0 are copied straight off to x
r.times{|i|
c.times{|j|
x[i,j].must == clues[i][j] if clues[i][j] > 0
}
}
r.times{|i| x[i,0..c-1].sum.must == rowsums[i] } # check row sums
c.times{|j| x.transpose[j,0..r-1].sum.must == colsums[j] } # check column sums
branch_on x, :variable => :smallest_size, :value => :min
end

The full program is here: survo_puzzle.rb, and three data files:
survo_puzzle_126_2008.txt
survo_puzzle_127_2008.txt
survo_puzzle_128_2008.txt


The Gecode/R models
Below are the models shown at My Gecode/R page. The selection is mostly for comparison with models implemented in other constraint programming languages, see respectively:
My MiniZinc page (which has a lot more models)
My JaCoP page
My Choco page

The models first written (e.g. diet, least_diff) are very "un-Rubyish" since I wanted to model straight after the MiniZinc models. Maybe I Rubyfi these later.

After a while the modeling went quite easy, and both de Bruijn and Minesweeper was done surprisingly fast. I do, however, miss MiniZinc's sum construct, since it which make some things easier (e.g. the neighbour summing in minesweeper.rb).

The execution time of the models os approximately the same time as the corresponding MiniZinc model with the Gecode/flatzinc solver which is normally quite fast. The big exception of these examples is coins_grid which seems to be slow for the constraint programming systems, but fast with linear programming systems, e.g. with the MiniZinc solvers ECLiPSe/ic and MiniZinc/mip.

References to the problems etc are in the header of the model.

January 05, 2009

Tom Schrijvers: "Monadic Constraint Programming" (in Haskell)

Tom Schrijvers presents in the blog post Monadic Constraint Programming a draft version of the paper Monadic Constraint Programming written by him, Peter Stuckey, and Philip Wadler:


A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming where the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.


Prototype code in Haskell can be downloaded here.