this repo has no description
dekker.one
1/* Linearized version
2 * Uses a predicate which constructs a subcircuit which always includes an extra dummy vertex
3 * Is worse than the just slightly adapted standard variant...
4*/
5include "alldifferent.mzn";
6
7/** @group globals
8 Constrains the elements of \a x to define a subcircuit where \a x[\p i] = \p j
9 means that \p j is the successor of \p i and \a x[\p i] = \p i means that \p i
10 is not in the circuit.
11*/
12%% Linear version
13predicate subcircuit(array[int] of var int: x) =
14 let { set of int: S = index_set(x),
15 int: l = min(S),
16 int: u = max(S),
17 int: n = card(S),
18 constraint forall(i in S)(x[i] in l..u),
19 array[l..u+1] of var l..u+1: xx,
20 constraint forall(i in S)(xx[i] in dom(x[i]) union {u+1}),
21 } in
22 alldifferent(x) /\
23 subcircuit_wDummy(xx) /\
24 forall( i in S, j in dom(x[i]) )( %% also when i==j?
25 eq_encode(x[i])[j] >= 2*eq_encode(xx[i])[j]
26 + eq_encode(xx[i])[u+1] + eq_encode(xx[u+1])[j] - 1 %% -1
27 /\
28 eq_encode(x[i])[j] >= eq_encode(xx[i])[j]
29 /\
30 eq_encode(x[i])[j] <= eq_encode(xx[i])[j] + eq_encode(xx[i])[u+1]
31 /\
32 eq_encode(x[i])[j] <= eq_encode(xx[i])[j] + eq_encode(xx[u+1])[j]
33 )
34 /\
35 forall( i in S )(
36 eq_encode(x[i])[i] == eq_encode(xx[i])[i]
37 )
38 ;
39
40%% Should include at least 2 nodes if >0?
41%% xx[n] is dummy
42predicate subcircuit_wDummy(array[int] of var int: x) =
43 let { set of int: S = index_set(x),
44 int: l = min(S),
45 int: u = max(S),
46 int: n = card(S),
47 set of int: S__ = S diff {u}, %% the real nodes
48 array[S__] of var 2..n: order,
49%% constraint order[n]==1, %% fix the dummy
50%% var bool: empty = (firstin == u+1), no, break 2-cycles with dummy
51 } in
52 alldifferent(x) /\
53 % NO alldifferent(order) /\
54
55 %%% MTZ model. Note that INTEGER order vars seem better!:
56 forall( i in S__, j in dom(x[i]) where i!=j /\ j!=u )(
57 order[i] - order[j] + (n-1)*eq_encode(x[i])[j]
58 % + (n-3)*bool2int(x[j]==i) %% the Desrochers & Laporte '91 term
59 % --- strangely enough it is much worse on vrp-s2-v2-c7_vrp-v2-c7_det_ADAPT_1_INVERSE.mzn!
60 <= n-2 ) /\
61
62 %% Break 2-cycles with dummy:
63 forall( i in S__ )(
64 eq_encode(x[i])[u] + eq_encode(x[u])[i] <= 1
65 /\
66 %% Ensure dummy is in:
67 if i in dom(x[i]) then
68 eq_encode(x[i])[i] >= eq_encode(x[u])[u]
69 else
70 true
71 endif
72 )
73 /\
74
75 % Symmetry? Each node that is not in is numbered after the lastin node.
76 forall(i in S) (
77 true
78% (not ins[i]) <-> (n == order[i])
79 )
80 ;
81
82predicate subcircuit_reif(array[int] of var int: x, var bool: b) =
83 abort("Reified subcircuit/1 is not supported.");
84
85%-----------------------------------------------------------------------------%
86%-----------------------------------------------------------------------------%