this repo has no description
dekker.one
1include "subgraph.mzn";
2
3predicate fzn_dtree(int: N, int: E, array[int] of int: from, array[int] of int: to,
4 var int: r, array[int] of var bool: ns, array[int] of var bool: es) =
5 let {
6 set of int: NODE = 1..N;
7 set of int: EDGE = 1..E;
8 array[NODE] of var 0..N-1: dist; /* distance from root */
9 array[NODE] of var 0..N: parent; /* parent */
10 } in
11 ns[r] /\ % the root must be chosen
12 dist[r] = 0 /\ % root is at distance 0
13 forall(n in NODE) % nonselected nodes have parent 0
14 (not ns[n] -> parent[n] <= 0) /\
15 forall(n in NODE) % nonselected nodes have distance 0
16 (not ns[n] -> dist[n] = 0) /\
17 forall(n in NODE) % each in node except root must have a parent
18 (ns[n] -> (n = r \/ parent[n] > 0)) /\
19 forall(n in NODE) % each node with a parent then parent is in
20 (parent[n] > 0 -> (ns[n] /\ ns[parent[n]])) /\
21 forall(n in NODE) % each node with a parent is one more than its parent
22 (parent[n] > 0 -> dist[n] = dist[parent[n]] + 1) /\
23 forall(n in NODE) % each node with a parent must have that edge in
24 (parent[n] > 0 -> exists(e in EDGE)(es[e] /\ from[e] = parent[n] /\ to[e] = n)) /\
25 forall(e in EDGE) % each edge must be part of the parent relation
26 (es[e] -> parent[to[e]] = from[e]) /\
27 sum(e in EDGE)(es[e]) = sum(n in NODE)(ns[n]) - 1 /\ % redundant relationship of trees
28 subgraph(N,E,from,to,ns,es);
29
30%-----------------------------------------------------------------------------%