this repo has no description
dekker.one
1predicate fzn_cost_mdd(array[int] of var int: x, % variables constrained by MDD
2 int: N, % number of nodes root is node 1
3 array[int] of int: level, % level of each node root is level 1, T is level length(x)+1
4 int: E, % number of edges
5 array[int] of int: from, % edge leaving node 1..N
6 array[int] of set of int: label, % values of variable on edge
7 array[int] of int: cost, % cost of using edge
8 array[int] of int: to, % edge entering node 0..N where 0 = T node
9 var int: totalcost % total cost of path
10 ) =
11 let { set of int: NODE = 1..N;
12 set of int: EDGE = 1..E;
13 int: L = length(x);
14 array[1..L] of int: maxlevelcost =
15 [ max(e in EDGE where level[from[e]] = l)(cost[e]) | l in 1..L];
16 array[1..L] of int: minlevelcost =
17 [ min([0] ++ [ cost[e] | e in EDGE where level[from[e]] = l /\ cost[e] < 0])| l in 1..L] ;
18 int: maxcost = sum(maxlevelcost);
19 set of int: COST = sum(minlevelcost)..L*(maxcost+1);
20 array[0..N] of var bool: bn;
21 array[EDGE] of var bool: be;
22 array[0..N] of var COST: ln; % distance from T
23 array[0..N] of var COST: un; % distance from root
24 } in
25 bn[0] /\ % true node is true
26 bn[1] /\ % root must hold
27 % T1 each node except the root enforces an outgoing edge
28 forall(n in NODE)(bn[n] -> exists(e in EDGE where from[e] = n)(be[e])) /\
29 % T23 each edge enforces its endpoints
30 forall(e in EDGE)((be[e] -> bn[to[e]]) /\ (be[e] -> bn[to[e]])) /\
31 % T4 each edge enforces its label
32 forall(e in EDGE)(be[e] -> x[level[from[e]]] in label[e]) /\
33 % P1 each node enforces its outgoing edges
34 forall(e in EDGE)(bn[from[e]] /\ x[level[from[e]]] in label[e] -> be[e]) /\
35 % P2 each node except the root enforces an incoming edge
36 exists(e in EDGE where to[e] = 0)(be[e]) /\
37 forall(n in 2..N)(bn[n] -> exists(e in EDGE where to[e] = n)(be[e])) /\
38 % P3 each label has a support
39 forall(i in 1..L, d in dom(x[i]))
40 (x[i] = d -> exists(e in EDGE where level[from[e]] = i /\ d in label[e])(be[e])) /\
41 ln[0] = 0 /\ un[1] = 0 /\
42 forall(n in NODE)
43 (ln[n] = min(e in EDGE where from[e] = n)(ln[to[e]] + cost[e] + (not be[e])*(maxcost+1 - cost[e]))) /\
44 forall(n in 2..N)
45 (un[n] = min(e in EDGE where to[e] = n)(un[from[e]] + cost[e] + (not be[e])*(maxcost+1 - cost[e]))) /\
46 forall(e in EDGE)(be[e] -> un[from[e]] + cost[e] + ln[to[e]] <= maxcost) /\
47 totalcost = ln[1];