cluster predicate - unidirectional graph reachability matrix

share/minizinc/std/cluster.mzn

@@ -0,0 +1,56 @@
+include "fzn_cluster_int.mzn";
+include "fzn_cluster_int_reif.mzn";
+include "fzn_cluster_enum.mzn";
+include "fzn_cluster_enum_reif.mzn";
+
+/** @group globals.graph
+    Clusterize the subgraph \a ns and \a es of a given undirected graph into disjoint subgraphs,
+    and produce a \a r node reachability matrix.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param r: node reachability matrix
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate cluster(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                  array[int,int] of var bool: r,
+                  array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"cluster: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"cluster: index set of to must be 1..\(E)") /\
+    assert(index_set(ns) = 1..N,"cluster: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"cluster: index set of es must be 1..\(E)") /\
+    fzn_cluster(N,E,from,to,r,ns,es);
+
+/** @group globals.graph
+    Clusterize the subgraph \a ns and \a es of a given undirected graph into disjoint subgraphs,
+    and produce a \a r node reachability matrix.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param r: node reachability matrix
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate cluster(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                  array[$$N,$$N] of var bool: r,
+                  array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        int: NUM_NODES = card(index_set(ns));
+    } in
+    assert(index_set(from) = index_set(to),"cluster: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"cluster: index set of from and es must be identical") /\
+    assert(index_set_1of2(r) = index_set_2of2(r),"cluster: nodes in from must be in index set of r") /\
+    assert(dom_array(from) subset index_set_1of2(r),"cluster: nodes in from must be in index set of r") /\
+    assert(dom_array(to) subset index_set_1of2(r),"cluster: nodes in to must be in index set of r") /\
+    assert(dom_array(from) subset index_set(ns),"cluster: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"cluster: nodes in to must be in index set of ns") /\
+    fzn_cluster(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(r),
+        index2int(ns),
+        index2int(es)
+    );

share/minizinc/std/fzn_cluster_enum.mzn

@@ -0,0 +1,31 @@
+include "reachable_multiroot.mzn";
+
+predicate fzn_cluster(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                      array[$$N,$$N] of var bool: r,
+                      array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        array[index_set(ns)] of var index_set(ns): NodeRoot;
+        array[index_set(ns)] of var bool: NodeRootnessMask;
+        array[index_set(ns)] of bool: ALL_GRAPH_NODES = [ true | n in index_set(ns) ];
+    } in
+        symmetry_breaking_constraint(forall (j,i in index_set(ns) where i > j)(
+            r[i,j] == r[j,i]
+        )) /\
+        forall (c in index_set(ns))(
+            r[c,c] == true
+        ) /\
+        forall (j,i in index_set(ns) where i > j)(
+            r[j,i] -> (ns[j] /\ ns[i])
+        ) /\
+        reachable_multiroot(from,to,NodeRootnessMask,ALL_GRAPH_NODES,es) /\
+        forall (n in index_set(ns))(
+            NodeRootnessMask[n] == (NodeRoot[n] == n)
+        ) /\
+        forall (e in index_set(es))(
+            es[e] -> (NodeRoot[from[e]] == NodeRoot[to[e]])
+        ) /\
+        forall (j,i in index_set(ns) where i > j)(
+            r[j,i] == (NodeRoot[i] == NodeRoot[j])
+        );
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_cluster_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                           array[$$N,$$N] of var bool: r, array[$$N] of var bool: ns,
+                           array[$$E] of var bool: es, var bool: b) =
+  abort("Reified cluster constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_int.mzn

@@ -0,0 +1,30 @@
+include "reachable_multiroot.mzn";
+
+predicate fzn_cluster(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                      array[int,int] of var bool: r, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..N] of var 1..N: NodeRoot;
+        array[1..N] of var bool: NodeRootnessMask;
+        array[1..N] of bool: ALL_GRAPH_NODES = [ true | n in 1..N ];
+    } in
+        symmetry_breaking_constraint(forall (j,i in 1..N where i > j)(
+            r[i,j] == r[j,i]
+        )) /\
+        forall (c in 1..N)(
+            r[c,c] == true
+        ) /\
+        forall (j,i in 1..N where i > j)(
+            r[j,i] -> (ns[j] /\ ns[i])
+        ) /\
+        reachable_multiroot(N,E,from,to,NodeRootnessMask,ALL_GRAPH_NODES,es) /\
+        forall (n in 1..N)(
+            NodeRootnessMask[n] == (NodeRoot[n] == n)
+        ) /\
+        forall (e in 1..E)(
+            es[e] -> (NodeRoot[from[e]] == NodeRoot[to[e]])
+        ) /\
+        forall (j,i in 1..N where i > j)(
+            r[j,i] == (NodeRoot[i] == NodeRoot[j])
+        );
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_cluster_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                           array[int,int] of var bool: r, array[int] of var bool: ns,
+                           array[int] of var bool: es, var bool: b) =
+  abort("Reified cluster constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_enum.mzn

@@ -0,0 +1,20 @@
+include "subgraph.mzn";
+
+predicate fzn_dreachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                   array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        array[index_set(ns)] of var 0..card(index_set(ns))-1: dist; /* distance from root */
+        array[index_set(ns)] of var index_set(ns): parent; /* parent */
+    } in
+        forall(n in index_set(ns)) % root nodes must be chosen
+              (rs[n] -> ns[n]) /\
+        forall(n in index_set(ns)) % self-parent is the same as either non-chosen node or root node
+              ((parent[n] = n) == ((not ns[n]) \/ rs[n])) /\
+        forall(n in index_set(ns)) % each non-self-parent node is one more step removed from a root than its parent node
+              (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
+        forall(n in index_set(ns)) % each non-self-parent node must have a chosen edge from its parent
+              (parent[n] != n -> exists(e in index_set(from) where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
+        % nodes connected by chosen edges must be chosen
+        subgraph(from,to,ns,es);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_dreachable_multiroot_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                        array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es,
+                                        var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_int.mzn

@@ -0,0 +1,20 @@
+include "subgraph.mzn";
+
+predicate fzn_dreachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                   array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..N] of var 0..N-1: dist; /* distance from root */
+        array[1..N] of var 1..N: parent; /* parent */
+    } in
+        forall(n in 1..N) % root nodes must be chosen
+              (rs[n] -> ns[n]) /\
+        forall(n in 1..N) % self-parent is the same as either non-chosen node or root node
+              ((parent[n] = n) == ((not ns[n]) \/ rs[n])) /\
+        forall(n in 1..N) % each non-self-parent node is one more step removed from a root than its parent node
+              (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
+        forall(n in 1..N) % each non-self-parent node must have a chosen edge from its parent
+              (parent[n] != n -> exists(e in 1..E where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
+        % nodes connected by chosen edges must be chosen
+        subgraph(N,E,from,to,ns,es);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_dreachable_multiroot_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                        array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es,
+                                        var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_enum.mzn

@@ -0,0 +1,15 @@
+include "subgraph.mzn";
+
+predicate fzn_reachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                  array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        int: E = length(es);
+        set of int: NODE = index_set(ns);
+        array[1..2*E] of NODE: dfrom   = from ++ to;
+        array[1..2*E] of NODE: dto     = to ++ from;
+        array[1..2*E] of var bool: des = es ++ es;
+    } in
+        /* duplicate the edges so that we can use directed graph reachability */
+        fzn_dreachable_multiroot(dfrom,dto,rs,ns,des);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_reachable_multiroot_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                       array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es,
+                                       var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_int.mzn

@@ -0,0 +1,13 @@
+include "subgraph.mzn";
+
+predicate fzn_reachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                  array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..2*E] of 1..N: dfrom   = from ++ to;
+        array[1..2*E] of 1..N: dto     = to ++ from;
+        array[1..2*E] of var bool: des = es ++ es;
+    } in
+        /* duplicate the edges so that we can use directed graph reachability */
+        fzn_dreachable_multiroot(N,2*E,dfrom,dto,rs,ns,des);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_reachable_multiroot_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                       array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es,
+                                       var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/globals.mzn

@@ -64,6 +64,7 @@ include "bin_packing_load_fn.mzn";
 include "bounded_path.mzn";
 include "circuit.mzn";
 include "circuit_opt.mzn";
+include "cluster.mzn";
 include "connected.mzn";
 include "cost_mdd.mzn";
 include "cost_regular.mzn";
@@ -129,6 +130,7 @@ include "piecewise_linear_non_continuous.mzn";
 include "range.mzn";
 include "range_fn.mzn";
 include "reachable.mzn";
+include "reachable_multiroot.mzn";
 include "regular.mzn";
 include "regular_nfa.mzn";
 include "regular_regexp.mzn";

share/minizinc/std/reachable_multiroot.mzn

@@ -0,0 +1,100 @@
+include "fzn_reachable_multiroot_int.mzn";
+include "fzn_reachable_multiroot_int_reif.mzn";
+include "fzn_reachable_multiroot_enum.mzn";
+include "fzn_reachable_multiroot_enum_reif.mzn";
+include "fzn_dreachable_multiroot_int.mzn";
+include "fzn_dreachable_multiroot_int_reif.mzn";
+include "fzn_dreachable_multiroot_enum.mzn";
+include "fzn_dreachable_multiroot_enum_reif.mzn";
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given directed graph to be reachable from roots \a rs.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate dreachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                               array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"dreachable_multiroot: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"dreachable_multiroot: index set of to must be 1..\(E)") /\
+    assert(index_set(rs) = 1..N,"dreachable_multiroot: index set of rs must be 1..\(N)") /\
+    assert(index_set(ns) = 1..N,"dreachable_multiroot: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"dreachable_multiroot: index set of es must be 1..\(E)") /\
+    fzn_dreachable_multiroot(N,E,from,to,rs,ns,es);
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given directed graph to be reachable from roots \a rs.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate dreachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                               array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    assert(index_set(from) = index_set(to),"dreachable_multiroot: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"dreachable_multiroot: index set of from and es must be identical") /\
+    assert(dom_array(from) subset index_set(rs),"dreachable_multiroot: nodes in from must be in index set of rs") /\
+    assert(dom_array(to) subset index_set(rs),"dreachable_multiroot: nodes in to must be in index set of rs") /\
+    assert(dom_array(from) subset index_set(ns),"dreachable_multiroot: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"dreachable_multiroot: nodes in to must be in index set of ns") /\
+    fzn_dreachable_multiroot(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(rs),
+        index2int(ns),
+        index2int(es)
+    );
+
+%-----------------------------------------------------------------------------%
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given undirected graph to be reachable from roots \a rs.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate reachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                              array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"reachable_multiroot: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"reachable_multiroot: index set of to must be 1..\(E)") /\
+    assert(index_set(rs) = 1..N,"reachable_multiroot: index set of rs must be 1..\(N)") /\
+    assert(index_set(ns) = 1..N,"reachable_multiroot: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"reachable_multiroot: index set of es must be 1..\(E)") /\
+    fzn_reachable_multiroot(N,E,from,to,rs,ns,es);
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given undirected graph to be reachable from roots \a rs.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate reachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                              array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    assert(index_set(from) = index_set(to),"reachable_multiroot: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"reachable_multiroot: index set of from and es must be identical") /\
+    assert(dom_array(from) subset index_set(rs),"reachable_multiroot: nodes in from must be in index set of rs") /\
+    assert(dom_array(to) subset index_set(rs),"reachable_multiroot: nodes in to must be in index set of rs") /\
+    assert(dom_array(from) subset index_set(ns),"reachable_multiroot: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"reachable_multiroot: nodes in to must be in index set of ns") /\
+    fzn_reachable_multiroot(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(rs),
+        index2int(ns),
+        index2int(es)
+    );