this repo has no description
at develop 2.2 kB view raw
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%-----------------------------------------------------------------------------%