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:
The great Global Constraint Catalog entry alldifferent_except_0) explains this constraint as:
- 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
- Nonogram (Comet): nonogram.co. (A faster model using the regular constraint, nonogram_regular.co, is described here and here).
- I wrote about
- 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
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
When modeling the constraint in Gecode/R, I experimented with different approaches. The reification variant
Note that here
This is exactly the same approach as the Choco version.
The Gecode version is very succint since it use overloaded boolean operators. Very nice.
Here are the previous entries:
- Learning constraint programming (languages) - part I
- Learning constraint programming - part II: Modeling with the Element constraint
Introduction
The global constraintalldifferent_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 ofalldifferent_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(Solverm, 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.javaThis 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.cppThe 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());