this repo has no description
dekker.one
1include "alldifferent.mzn";
2
3predicate fzn_subcircuit(array[int] of var int: x) =
4 let {
5 set of int: S = index_set(x),
6 int: l = min(S),
7 int: u = max(S),
8 int: n = card(S),
9 array[S] of var 1..n: order,
10 array[S] of var bool: ins = array1d(S,[ x[i] != i | i in S]),
11 var l..u+1: firstin = min([ u+1 + bool2int(ins[i])*(i-u-1) | i in S]),
12 var S: lastin,
13 var bool: empty = (firstin > u),
14 } in
15 alldifferent(x) /\
16 alldifferent(order) /\
17
18 % If the subcircuit is empty then each node points at itself.
19 %
20 (empty -> forall(i in S)(not ins[i])) /\
21
22 % If the subcircuit is non-empty then order numbers the subcircuit.
23 %
24 ((not empty) ->
25
26 % The firstin node is numbered 1.
27 order[firstin] = 1 /\
28
29 % The lastin node is greater than firstin.
30 lastin > firstin /\
31
32 % The lastin node points at firstin.
33 x[lastin] = firstin /\
34
35 % And both are in
36 ins[lastin] /\ ins[firstin] /\
37
38 % The successor of each node except where it is firstin is
39 % numbered one more than the predecessor.
40 forall(i in S) (
41 (ins[i] /\ x[i] != firstin) -> order[x[i]] = order[i] + 1
42 ) /\
43
44 % Each node that is not in is numbered after the lastin node.
45 forall(i in S) (
46 ins[i] \/ order[lastin] < order[i]
47 )
48 );
49
50%-----------------------------------------------------------------------------%