this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2% 'all_different' constrains an array of objects to be all different.
3%
4% Linear version: equality encoding; see e.g. [Refalo, CP 2000]
5%
6% For a given d in dom(x), at most one i with x_i = d can exist.
7%-----------------------------------------------------------------------------%
8
9include "domain_encodings.mzn";
10
11predicate fzn_all_different_int(array[int] of var int: x) =
12 if length(x)<=1 then true
13 else
14 let {
15 array[int,int] of var 0..1: x_eq_d = eq_encode(x)
16 } in (
17% my_trace(" all_different_int: x[" ++ show(index_set(x)) ++ "]\n") /\
18 forall(d in index_set_2of2(x_eq_d))( sum(i in index_set_1of2(x_eq_d))( x_eq_d[i,d] ) <= 1 )
19 )
20 endif;
21
22
23%-----------------------------------------------------------------------------%