Stable pair-matching

We now consider another constraint problem, called stable pair-matching problem. We will understand through this example another two new features of DJ: array indexes can be variables and arrays can be unified.

The problem is described as follows: There is a group of women and a group of the same number of men. Each person has expressed his/her ranking for the members in the opposite group. The problem is to find a matching between the two groups such that the marriages are stable. A marriage between a man m and a woman w is said to be stable provided that:

• whenever m prefers another woman o to w, o prefers her spouse to m.
• whenever w prefers another man o to m, o prefers her spouse to w.

The problem is taken from [#!HEN99!#]. The following shows the code:

 class Person {
     dj Label name;
     dj int ranking[Marriage.N];
     dj int spouse in 0..Marriage.N-1;
 }

 class Marriage {
     static final int N=5;
     dj Person man[N];
     dj Person woman[N];

     initialize(man,woman);

     for (i in 0..N){ // be couples
         woman[man[i].spouse].spouse==i;
         man[woman[i].spouse].spouse==i; 
     }
     for (m in 0..4, w in 0..4){ // stable
         man[m].ranking[w] < man[m].ranking[man[m].spouse] ->
           woman[w].ranking[woman[w].spouse] < woman[w].ranking[m];

         woman[w].ranking[m] < woman[w].ranking[woman[w].spouse] ->
           man[m].ranking[man[m].spouse] < man[m].ranking[w];
     } 
     grid(array({man[i],woman[man[i].spouse]},i in 0..N));
 }

 constraint initialize(Person[] man, Person[] woman){
     man[0].name.text=="Richard";
     man[0].ranking=={5,1,2,4,3};
        ...
}

A person has a name, a ranking for the persons in his/her opposite group, and a spouse. Only name is graphic that can be displayed in the panel.

In the class Marriage, the array man and woman represents the two groups, respectively. The constraint initialize initializes the name and the ranking of every person. The first for constraint ensures that the solution is a matching: if a man is married to a woman, then the woman must be married to the man too, and vice versa. The second for constraint specifies the stability requirement. For each man m, if m could not be married to a woman w that he preferred more to his spouse, then the woman w must be happier with being married to her spouse than being married to m. The same case applies to every woman, too.

The grid constraint places the labels in a tabular form such that each couple takes a row.

This example illustrates two features of DJ: First, indexes of arrays can be variables, as in woman[man[i].spouse].spouse == i. This is a powerful feature. Without this feature, we would have to write the constraint as follows:

 for (j in 0..N-1)
     man[i].spouse==j -> woman[j].spouse == i;

which is hard to read and inefficient because many entailment constraints have to be generated.

The second feature is unification of arrays. We have seen examples of unifications of integers, strings, and objects. In DJ, it is also possible to unify two arrays, as in man[0].ranking=={5,1,2,4,3}. Two arrays are unifiable if their lengths are the same and the elements are pair-wisely unifiable.