this repo has no description
dekker.one
1predicate fzn_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, % value of variable
7 array[int] of int: to % edge entering node 0..N where 0 = T node
8 ) =
9 let { set of int: NODE = 1..N;
10 set of int: EDGE = 1..E;
11 int: L = length(x);
12 array[0..N] of var bool: bn;
13 array[EDGE] of var bool: be;
14 set of int: D = dom_array(x); } in
15 bn[0] /\ % true node is true
16 bn[1] /\ % root must hold
17 % T1 each node except the root enforces an outgoing edge
18 forall(n in NODE)(bn[n] -> exists(e in EDGE where from[e] = n)(be[e])) /\
19 % T23 each edge enforces its endpoints
20 forall(e in EDGE)((be[e] -> bn[from[e]]) /\ (be[e] -> bn[to[e]])) /\
21 % T4 each edge enforces its label
22 forall(e in EDGE)(be[e] -> x[level[from[e]]] in label[e]) /\
23 % P1 each node enforces its outgoing edges
24 forall(e in EDGE)(bn[from[e]] /\ x[level[from[e]]] in label[e] -> be[e]) /\
25 % P2 each node except the root enforces an incoming edge
26 exists(e in EDGE where to[e] = 0)(be[e]) /\
27 forall(n in 2..N)(bn[n] -> exists(e in EDGE where to[e] = n)(be[e])) /\
28 % P3 each label has a support
29 forall(i in 1..L, d in D)
30 (x[i] = d -> exists(e in EDGE where level[from[e]] = i /\ d in label[e])(be[e]));