this repo has no description
1include "alldifferent.mzn";
2
3/** @group globals
4 Constrains the elements of \a x to define a subcircuit where \a x[\p i] = \p j
5 means that \p j is the successor of \p i and \a x[\p i] = \p i means that \p i
6 is not in the circuit.
7*/
8%% Linear version
9predicate fzn_subcircuit(array[int] of var int: x) =
10 let { set of int: S = index_set(x),
11 int: l = min(S),
12 int: u = max(S),
13 int: n = card(S),
14 array[S] of var 1..n: order,
15 array[S] of var bool: ins = array1d(S,[ x[i] != i | i in S]),
16 var l..u+1: firstin = min([ u+1 + bool2int(ins[i])*(i-u-1) | i in S]), %% ...
17 var S: lastin,
18 var bool: empty = (firstin == u+1),
19 } in
20 alldifferent(x) /\
21 % NO alldifferent(order) /\
22
23 % If the subcircuit is empty then each node points at itself.
24 %
25 (empty <-> forall(i in S)(not ins[i])) /\
26
27 % If the subcircuit is non-empty then order numbers the subcircuit.
28 %
29 ((not empty) <->
30
31 %% Another way to express minimum.
32% forall(i in l..u+1)(
33% i==firstin <-> ins[i]
34% /\ forall(j in S where j<i)( not ins[j] )
35% ) /\
36
37 % The firstin node is numbered 1.
38 order[firstin] = 1 /\
39
40 % The lastin node is greater than firstin.
41 lastin > firstin /\
42
43 % The lastin node points at firstin.
44 x[lastin] = firstin /\
45
46 % And both are in
47 ins[lastin] /\ ins[firstin] /\
48
49 % The successor of each node except where it is firstin is
50 % numbered one more than the predecessor.
51% forall(i in S) (
52% (ins[i] /\ x[i] != firstin) -> order[x[i]] = order[i] + 1
53% ) /\
54 %%% MTZ model. Note that INTEGER order vars seem better!:
55 forall (i,j in S where i!=j) (
56 order[i] - order[j] + n*bool2int( x[i]==j /\ i!=lastin )
57 % + (n-2)*bool2int(x[j]==i) %% the Desrochers & Laporte '91 term
58 <= n-1 ) /\
59
60 % Each node that is not in is numbered after the lastin node.
61 forall(i in S) (
62 true
63% (not ins[i]) <-> (n == order[i])
64 )
65
66 );
67
68%-----------------------------------------------------------------------------%