Some constraints in Choco
I implemented some filtering algorithms for specific global constraints in
Choco
during my PhD. They have been written and tested with Choco 1.2, and some of them have been included in Choco 2.0.
If you want to use these constraints, either download Choco 2.0, or download them separately below. Anyway, this page also
provides a short description of these constraints, and how to use them in Choco. I hope someone will find this useful.
Sorting constraint
Semantics
Let
x and
x' be two vectors of variables of the same length, and
v be
an instantiation. The sorting constraint
Sort(x, x') holds on the set of
variables being either in
x or in
x', and is satisfied by
v if and
only if
v(x') is the sorted version of
v(x) in increasing order.
This constraint is called the Sortedness Constraint in [BleuzenGuernalec
and Colmerauer 1997] and in [Mehlhorn and Thiel 2000].
References
[BleuzenGuernalec and Colmerauer 1997] 
N. BleuzenGuernalec and A. Colmerauer. Narrowing a block of sortings in
quadratic time. In Proc. of CP'97. Linz, Austria, 1997. 
[Mehlhorn and Thiel 2000] 
K. Mehlhorn and S. Thiel. Faster algorithms for boundconsistency of the Sortedness and
the Alldifferent constraint. In Proc. of CP'00. Singapore, 2000. 
Description of the implementation
We have implemented the algorithm from [Mehlhorn and Thiel 2000], that enforces boundconsistency in
O(n log(n)) in the worst case. Some parts of the code still need to be optimized.
The constructor takes two vectors (corresponding to
x and
x') of
IntDomainVar
instances as parameters.
Download
Example
Here is a simple example using the Sorting Constraint (this example can be downloaded as a
Java file):
import choco.integer.IntDomainVar;
import choco.Problem;
public class SortingExample {
public static void main (String[] args) {
Problem p = new Problem();
IntDomainVar[] u = p.makeEnumIntVarArray("u", 4, 1, 5);
IntDomainVar[] v = p.makeEnumIntVarArray("v", 4, 2, 6);
p.post(new SortingConstraint(u, v));
p.post(p.allDifferent(u));
if(p.solve() == Boolean.TRUE) {
System.out.print("u = [ " + u[0].getVal() + " " + u[1].getVal() + " " + u[2].getVal() + " " + u[3].getVal() + " ]  ");
System.out.println("v = [ " + v[0].getVal() + " " + v[1].getVal() + " " + v[2].getVal() + " " + v[3].getVal() + " ]");
}
while(p.nextSolution() == Boolean.TRUE) {
System.out.print("u = [ " + u[0].getVal() + " " + u[1].getVal() + " " + u[2].getVal() + " " + u[3].getVal() + " ]  ");
System.out.println("v = [ " + v[0].getVal() + " " + v[1].getVal() + " " + v[2].getVal() + " " + v[3].getVal() + " ]");
}
}
}

The previous source code generates a problem with two vectors u and v of four variables, and the two
following global constraints: Sort(u, v) and AllDifferent(u).
The only one admissible solutions are the following ones:
u = [ 2 3 4 5 ]  v = [ 2 3 4 5 ]
u = [ 2 3 5 4 ]  v = [ 2 3 4 5 ]
u = [ 2 4 3 5 ]  v = [ 2 3 4 5 ]
u = [ 2 4 5 3 ]  v = [ 2 3 4 5 ]
u = [ 2 5 3 4 ]  v = [ 2 3 4 5 ]
u = [ 2 5 4 3 ]  v = [ 2 3 4 5 ]
u = [ 3 2 4 5 ]  v = [ 2 3 4 5 ]
u = [ 3 2 5 4 ]  v = [ 2 3 4 5 ]
u = [ 3 4 2 5 ]  v = [ 2 3 4 5 ]
u = [ 3 4 5 2 ]  v = [ 2 3 4 5 ]
u = [ 3 5 2 4 ]  v = [ 2 3 4 5 ]
u = [ 3 5 4 2 ]  v = [ 2 3 4 5 ]
u = [ 4 2 3 5 ]  v = [ 2 3 4 5 ]
u = [ 4 2 5 3 ]  v = [ 2 3 4 5 ]
u = [ 4 3 2 5 ]  v = [ 2 3 4 5 ]
u = [ 4 3 5 2 ]  v = [ 2 3 4 5 ]
u = [ 4 5 2 3 ]  v = [ 2 3 4 5 ]
u = [ 4 5 3 2 ]  v = [ 2 3 4 5 ]
u = [ 5 2 3 4 ]  v = [ 2 3 4 5 ]
u = [ 5 2 4 3 ]  v = [ 2 3 4 5 ]
u = [ 5 3 2 4 ]  v = [ 2 3 4 5 ]
u = [ 5 3 4 2 ]  v = [ 2 3 4 5 ]
u = [ 5 4 2 3 ]  v = [ 2 3 4 5 ]
u = [ 5 4 3 2 ]  v = [ 2 3 4 5 ]
Leximin constraint
Semantics
We define the leximin preorder as follows:
Let
x and
y be two vectors of
n integers, and let
x^{↑} and
y^{↑} be the version of
x and
y rearranged in increasing order.
x and
y are said leximinindifferent if
x^{↑}=y^{↑}.
y is leximinpreferred to
x (written
y>_{leximin}x if and only if
there is an
i< n such that for all
j≤ i:
 the j^{th} component of x^{↑} is equal to the
j^{th} component of y^{↑}
 the i^{th} component of x^{↑} is lower than the
i^{th} component of y^{↑}
Let
x and
x' be two vectors of variables, and
v be an instantiation. The constraint
Leximin(x, x') holds on
the set of variables belonging to
x or
x', and is satisfied by
v if and only if
v(x) <_{leximin} v(x').
References
[Frisch et al. 2003] 
A. Frisch, B. Hnich, Z. Kiziltan, I. Miguel, and T. Walsh. Multiset ordering constraints.
In Proc. of IJCAI'03. Acapulco, Mexico, 2003. 
Description of the implementation
The implementation of this constraint is adapted from the algorithm given in [Frisch
et al. 2003]
and enforces generalized arcconsistency on the constraint Leximin in
O(n log(n)) (we choose
tha version of the algorithm that does not build the entire occurrence vectors, as the size of our
domains can be huge).
We made two versions of this constraint. The first one works on two vectors of variables, and the second
one works on one vector of variables and one vector of integers.
Download
Example
Here is a simple example using the Sorting Constraint (this example can be downloaded as a
Java file):
import choco.integer.IntDomainVar;
import choco.Problem;
public class LeximinExample {
public static void main (String[] args) {
Problem p = new Problem();
IntDomainVar[] u = p.makeEnumIntVarArray("u", 3, 2, 5);
IntDomainVar[] v = p.makeEnumIntVarArray("v", 3, 2, 4);
p.post(new LeximinConstraint(u, v));
p.post(p.allDifferent(v));
if(p.solve() == Boolean.TRUE) {
System.out.print("u = [ " + u[0].getVal() + " " + u[1].getVal() + " " + u[2].getVal() + " ]  ");
System.out.println("v = [ " + v[0].getVal() + " " + v[1].getVal() + " " + v[2].getVal() + " ]");
}
while(p.nextSolution() == Boolean.TRUE) {
System.out.print("u = [ " + u[0].getVal() + " " + u[1].getVal() + " " + u[2].getVal() + " ]  ");
System.out.println("v = [ " + v[0].getVal() + " " + v[1].getVal() + " " + v[2].getVal() + " ]");
}
}
}

The previous source code generates a problem with two vectors u and v of three variables, and the two
following global constraints: Leximin(u, v) and AllDifferent(u).
The only one admissible solutions are the following ones:
u = [ 2 2 2 ]  v = [ 2 3 4 ]
u = [ 2 2 3 ]  v = [ 2 3 4 ]
u = [ 2 2 4 ]  v = [ 2 3 4 ]
u = [ 2 2 5 ]  v = [ 2 3 4 ]
[...]
u = [ 3 2 3 ]  v = [ 4 3 2 ]
u = [ 3 3 2 ]  v = [ 4 3 2 ]
u = [ 4 2 2 ]  v = [ 4 3 2 ]
u = [ 5 2 2 ]  v = [ 4 3 2 ]
AtLeast constraint
Semantics
Let
x be a vector of
n variables,
y be a variable,
k ≥ n be
an integer, and
v be an instantiation. The constraint
AtLeast(x, y, k) holds on
the set of variables belonging to
x and on
y, and is satisfied by
v if and only if
at least
k variables among the
x_{i} are such that
v(x_{i} ) ≥ v(y).
The constraint
SemiAtLeast is the same, but where
y is a number instead of a variable.
Description of the implementation
Our implementation of this constraint is a bit similar to the implementation of the
Occurrence
constraint in the
Choco tutorial. It is
also based on a storing of the ordered vector of the upper bounds of
x. At the beginning,
and at each propagation step, a reordering of this vector is done, using respectively a quick sort
procedure at the beginning and an insertion sort procedure at each step. It leads to a
time complexity of
O(n^{2}), but it is much faster in average, since the vector
is almost sorted at each step (that is why we use an insertion sort procedure).
Two versions of the constraint are available, the second one being
Download