this repo has no description
dekker.one
1include "subgraph.mzn";
2
3function array[$$N,$$N] of var bool:
4 fzn_transitive_closure(array[int] of $$N: from, array[int] of $$N: to,
5 var $$N: r, array[$$N] of var bool: ns, array[int] of var bool: es) =
6 let {
7 array[index_set(ns)] of var 0..card(index_set(ns))-1: dist; /* distance from root */
8 array[index_set(ns)] of var index_set(ns): parent; /* parent */
9 } in
10 ns[r] /\ % the root must be chosen
11 dist[r] = 0 /\ % root is at distance 0
12 parent[r] = r /\ % root is its own parent
13 forall(n in index_set(ns)) % nonselected nodes have parent 0
14 (not ns[n] -> parent[n] = n) /\
15 forall(n in index_set(ns)) % nonselected nodes have distance 0
16 (not ns[n] -> dist[n] = 0) /\
17 forall(n in index_set(ns)) % each in node except root must have a parent
18 (ns[n] -> (n = r \/ parent[n] != n)) /\
19 forall(n in index_set(ns)) % each in node with a parent must be in and also its parent
20 (parent[n] != n -> (ns[n] /\ ns[parent[n]])) /\
21 forall(n in index_set(ns)) % each except with a parent is one more than its parent
22 (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
23 forall(n in index_set(ns)) % each node with a parent must have that edge in
24 (parent[n] != n -> exists(e in index_set(from) where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
25 subgraph(from,to,ns,es);