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**

**a**baiser

**l**antaca

**b**ittman

**o**samine

**r**ecanes

**g**ranese

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