Please consider providing Graph Reachability Matrix predicate

[LebedevRI]

It would have been rather useful to me when i was trying to write a model,
and i couldn't quite come up with anything good on a spot,
and thus after much pain ended up with:
https://github.com/LebedevRI/minizinc-graph-reachability-matrix-predicate.mzn

Unfortunately it ends up having O(n^3) complexity, as benchmark notes,
but that is only because connected() is itself O(n^2).
There may perhaps be a better formulation for all that,
but i'm not seeing it currently.
The results are already much better than i had hoped.

(There may be a standard set of inefficiencies in minizinc itself,
not sure how much i want to look into that given how it's developed and tested...)

[LebedevRI]

FYI i'm looking at a non-cubic implementation, hang on.

[LebedevRI]

@cyderize @guidotack Ok! I think i got what i was looking for.

Essentially, this ended up consisting of two parts:

1. reachable_multiroot() - a seemingly rather boringly straight-forward generalization of the reachable(),
   which, instead of enforcing that the subgraph is reachable from the root node (given by index, non-optional),
   and thus forcing there to be a single joint subgraph, instead takes (zero or more) roots as a mask.
   The rest of the logic is generalized accordingly.

include "subgraph.mzn";

predicate fzn_dreachable(array[int] of $$N: from, array[int] of $$N: to,
                        var $$N: r, array[$$N] of var bool: ns, array[int] 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
        ns[r] /\ % the root must be chosen
        dist[r] = 0 /\ % root is at distance 0
        parent[r] = r /\ % root is its own parent
        forall(n in index_set(ns)) % nonselected nodes have parent 0
              (not ns[n] -> parent[n] = n) /\
        forall(n in index_set(ns)) % nonselected nodes have distance 0
              (not ns[n] -> dist[n] = 0) /\
        forall(n in index_set(ns)) % each in node except root must have a parent
              (ns[n] -> (n = r \/ parent[n] != n)) /\
        forall(n in index_set(ns)) % each in node with a parent must be in and also its parent
              (parent[n] != n -> (ns[n] /\ ns[parent[n]])) /\
        forall(n in index_set(ns)) % each except with a parent is one more than its parent
              (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
        forall(n in index_set(ns)) % each node with a parent must have that edge in
              (parent[n] != n -> exists(e in index_set(from) where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
        subgraph(from,to,ns,es);
   
%-----------------------------------------------------------------------------%

vs

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 zero distance from root
              ((parent[n] = n) == (dist[n] = 0)) /\
        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);

%-----------------------------------------------------------------------------%

2. cluster() predicate.
   This one took quite a bit of rewrites to fully distill it to it's purest+simplest+fastest form. :)
   The (final) basic idea is to, basically, give each node a unique "color",
   and then set the nodes, linked together by selected edges, to the same color,
   thus ensuring that the nodes, that are not in any way connected, don't have the same "color",
   and vice versa.

   Implementation-wise, instead of color, for each node, we track the index of the disjoint subgraph
   to which this node belongs, and it turned out that tracking that by tracking the root node
   of each subgraph is the best approach (referred to as root). So there's 3 parts:

   1. Splitting disjoint subgraphs: we then defer to reachable_multiroot() to enfore
      that each disjoint subgraph actually has a root node,
      thus different disjoint subgraphs have different roots.
   2. Coalescing same-color subgraphs: nodes, that are linked together by selected edge, have the same root.
   3. And then we actually compute reachability matrix based on whether or not
      two nodes have same root (belong to the same disjoint subgraph)

   Now, this is controversial. I've decided to return the reachability matrix,
   NOT the subgraph index. While sparse data structure seems better,
   it immediately requires symmetry breaking constraint, which is tricky (i have written it.),
   and --all-solutions actually ends up being MUCH slower (O^3?)
   than just returning reachability matrix... The directed version would need to
   return the matrix, so this is also future-proofing for consistency sake

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
        ) /\
        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])
        );

%-----------------------------------------------------------------------------%

I have an exhaustive test harness for the cluster() (but not the rest),
it would not have been possible to refine the predicate so much otherwise,
please see https://github.com/LebedevRI/minizinc-graph-reachability-matrix-predicate.mzn
minizinc-graph-reachability-matrix-predicate.zip

Knowing that this repo is just a mirror, and PR would not be merged anyways,
what else would you want to see before this can be merged?
Please do ensure that the commit does end up being committed with --author="Roman Lebedev <[email protected]>" to ensure proper attribution.