this repo has no description
dekker.one
1include "fzn_cost_mdd.mzn";
2include "fzn_cost_mdd_reif.mzn";
3
4/** @group globals.extensional
5 Requires that \a x defines a path in the cost MDD with total edge weight \a totalcost.
6
7 \a N is the number of nodes, the root node is node 1
8 \a level is the level of each node, the root is level 1, T is level \a length(x)+1
9 \a E is the number of edges
10 \a from is the leaving node (1..\a N)for each edge
11 \a label is the set of value of the x variable for each edge
12 \a cost is the cost for each edge
13 \a to is the entering node for each edge, where 0 = T node
14 \a totalcost is the total cost of the path defined by \a x
15
16*/
17predicate cost_mdd(array[int] of var int: x, % variables constrained by MDD
18 int: N, % number of nodes root is node 1
19 array[int] of int: level, % level of each node root is level 1, T is level length(x)+1
20 int: E, % number of edges
21 array[int] of int: from, % edge leaving node 1..N
22 array[int] of set of int: label, % values of variable on edge
23 array[int] of int: cost, % cost of using edge
24 array[int] of int: to, % edge entering node 0..N where 0 = T node
25 var int: totalcost % total cost of path
26 ) =
27 let { set of int: NODE = 1..N;
28 set of int: EDGE = 1..E;
29 int: L = length(x);
30 array[0..N] of int: levele = array1d(0..N,[L+1]++level);
31 } in
32 assert(index_set(level) = NODE,
33 "cost_mdd: level argument must be of length N = \(N)") /\
34 assert(level[1] = 1, "cost_mdd: level of root (1) must be 1") /\
35 forall(n in 2..N)(assert(level[n] != 1, "cost_mdd: level of non root node (\(n)) must not be 1")) /\
36 assert(index_set(from) = EDGE,
37 "cost_mdd: from argument must be of length E = \(E)") /\
38 assert(index_set(to) = EDGE,
39 "cost_mdd: to argument must be of length E = \(E)") /\
40 assert(index_set(label) = EDGE,
41 "cost_mdd: label argument must be of length E = \(E)") /\
42 assert(index_set(cost) = EDGE,
43 "cost_mdd: cost argument must be of length E = \(E)") /\
44 forall(e in EDGE)(assert(from[e] in NODE,
45 "cost_mdd: from[\(e)] must be in \(NODE)")) /\
46 forall(e in EDGE)(assert(to[e] in 0..N,
47 "cost_mdd: to[\(e)] must be in 0..\(N)")) /\
48 forall(e in EDGE)(assert(level[from[e]]+1 = levele[to[e]],
49 "cost_mdd: mdd level of from[\(e)] = \(level[from[e]])" ++
50 "must be 1 less than level of to[\(e)] = \(levele[to[e]])")) /\
51 forall(e1,e2 in EDGE where e1 < e2 /\ from[e1] = from[e2])
52 (assert(label[e1] intersect label[e2] = {},
53 "cost_mdd: Two edges \(e1) and \(e2) leaving node \(from[e1]) with overlapping labels")) /\
54 fzn_cost_mdd(x,N,level,E,from,label,cost,to,totalcost);
55
56predicate cost_mdd_reif(array[int] of var int: x, % variables constrained by MDD
57 int: N, % number of nodes root is node 1
58 array[int] of int: level, % level of each node root is level 1, T is level length(x)+1
59 int: E, % number of edges
60 array[int] of int: from, % edge leaving node 1..N
61 array[int] of set of int: label, % values of variable on edge
62 array[int] of int: cost, % cost of using edge
63 array[int] of int: to, % edge entering node 0..N where 0 = T node
64 var int: totalcost, % total cost of path
65 var bool: b % reification variable
66 ) =
67 fzn_cost_mdd_reif(x, N, level, E, from, label, cost, to, totalcost, b);
68
69% Example consider an MDD over 3 variables
70% 5 nodes and 8 edges
71% level 1 root = 1
72% level 2 2 3
73% level 3 4 5
74% level 4 T
75% with edges (from,label,cost,to) given by
76% (1,{1,3},3,2), (1,{2},1,3),
77% (2,{2},4,4), (2,{3},2,5),
78% (3,{3},3,4), (3,{2},5,5),
79% (4,{1,5},2,0),
80% (5,{2,4,6},4,0)
81% this is defined by the call
82% cost_mdd([x1,x2,x3],5,[1,2,2,3,3],8,[1,1,2,2,3,3,4,5],
83% [{1,3},{2},{2},{3},{3},{2},{1,5},{2,4,6}],[3,1,4,2,3,5,2,4],[2,3,4,5,4,5,0,0],tc)