From 819cfc45c0acfba13485dc9a42e586328827c153 Mon Sep 17 00:00:00 2001 From: Roman Lebedev Date: Sat, 3 May 2025 04:14:20 +0300 Subject: [PATCH] `cluster` predicate - unidirectional graph reachability matrix Questions/notes: 1. Is there an autoformatter? 2. I'm not sure about the `multiroot` suffix, should it be `anyroot`? 3. Also, is `cluster` the best name? Is `constellations`/`sccs` better? I needed this some time back, and having this would have saved me quite some time. 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. 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** 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/tree/proof-of-concept/unidirectional --- share/minizinc/std/cluster.mzn | 56 + share/minizinc/std/fzn_cluster_enum.mzn | 31 + share/minizinc/std/fzn_cluster_enum_reif.mzn | 6 + share/minizinc/std/fzn_cluster_int.mzn | 30 + share/minizinc/std/fzn_cluster_int_reif.mzn | 6 + .../std/fzn_dreachable_multiroot_enum.mzn | 20 + .../fzn_dreachable_multiroot_enum_reif.mzn | 6 + .../std/fzn_dreachable_multiroot_int.mzn | 20 + .../std/fzn_dreachable_multiroot_int_reif.mzn | 6 + .../std/fzn_reachable_multiroot_enum.mzn | 15 + .../std/fzn_reachable_multiroot_enum_reif.mzn | 6 + .../std/fzn_reachable_multiroot_int.mzn | 13 + .../std/fzn_reachable_multiroot_int_reif.mzn | 6 + share/minizinc/std/globals.mzn | 2 + share/minizinc/std/reachable_multiroot.mzn | 100 + .../cluster/cluster-exhaustive-sat.enum.mzn | 388 ++ .../cluster/cluster-exhaustive-sat.int.mzn | 388 ++ .../cluster/cluster-exhaustive-unsat.enum.mzn | 51 + .../cluster/cluster-exhaustive-unsat.int.mzn | 51 + .../globals/cluster/cluster.naive.mzn.model | 32 + .../cluster/cluster_naive-exhaustive-sat.mzn | 388 ++ ...eachable_multiroot-exhaustive-sat.enum.mzn | 5358 +++++++++++++++++ ...reachable_multiroot-exhaustive-sat.int.mzn | 5358 +++++++++++++++++ ...eachable_multiroot-exhaustive-sat.enum.mzn | 748 +++ ...reachable_multiroot-exhaustive-sat.int.mzn | 748 +++ 25 files changed, 13833 insertions(+) create mode 100644 share/minizinc/std/cluster.mzn create mode 100644 share/minizinc/std/fzn_cluster_enum.mzn create mode 100644 share/minizinc/std/fzn_cluster_enum_reif.mzn create mode 100644 share/minizinc/std/fzn_cluster_int.mzn create mode 100644 share/minizinc/std/fzn_cluster_int_reif.mzn create mode 100644 share/minizinc/std/fzn_dreachable_multiroot_enum.mzn create mode 100644 share/minizinc/std/fzn_dreachable_multiroot_enum_reif.mzn create mode 100644 share/minizinc/std/fzn_dreachable_multiroot_int.mzn create mode 100644 share/minizinc/std/fzn_dreachable_multiroot_int_reif.mzn create mode 100644 share/minizinc/std/fzn_reachable_multiroot_enum.mzn create mode 100644 share/minizinc/std/fzn_reachable_multiroot_enum_reif.mzn create mode 100644 share/minizinc/std/fzn_reachable_multiroot_int.mzn create mode 100644 share/minizinc/std/fzn_reachable_multiroot_int_reif.mzn create mode 100644 share/minizinc/std/reachable_multiroot.mzn create mode 100644 tests/spec/unit/globals/cluster/cluster-exhaustive-sat.enum.mzn create mode 100644 tests/spec/unit/globals/cluster/cluster-exhaustive-sat.int.mzn create mode 100644 tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.enum.mzn create mode 100644 tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.int.mzn create mode 100644 tests/spec/unit/globals/cluster/cluster.naive.mzn.model create mode 100644 tests/spec/unit/globals/cluster/cluster_naive-exhaustive-sat.mzn create mode 100644 tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.enum.mzn create mode 100644 tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.int.mzn create mode 100644 tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.enum.mzn create mode 100644 tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.int.mzn diff --git a/share/minizinc/std/cluster.mzn b/share/minizinc/std/cluster.mzn new file mode 100644 index 000000000..4c4c03f08 --- /dev/null +++ b/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) + ); diff --git a/share/minizinc/std/fzn_cluster_enum.mzn b/share/minizinc/std/fzn_cluster_enum.mzn new file mode 100644 index 000000000..6e0a02879 --- /dev/null +++ b/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]) + ); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_cluster_enum_reif.mzn b/share/minizinc/std/fzn_cluster_enum_reif.mzn new file mode 100644 index 000000000..a524041cd --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_cluster_int.mzn b/share/minizinc/std/fzn_cluster_int.mzn new file mode 100644 index 000000000..3d3c56186 --- /dev/null +++ b/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]) + ); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_cluster_int_reif.mzn b/share/minizinc/std/fzn_cluster_int_reif.mzn new file mode 100644 index 000000000..e9fa69cbb --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_dreachable_multiroot_enum.mzn b/share/minizinc/std/fzn_dreachable_multiroot_enum.mzn new file mode 100644 index 000000000..4ed392a3b --- /dev/null +++ b/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); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_dreachable_multiroot_enum_reif.mzn b/share/minizinc/std/fzn_dreachable_multiroot_enum_reif.mzn new file mode 100644 index 000000000..1aec8808c --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_dreachable_multiroot_int.mzn b/share/minizinc/std/fzn_dreachable_multiroot_int.mzn new file mode 100644 index 000000000..ea17c3e37 --- /dev/null +++ b/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); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_dreachable_multiroot_int_reif.mzn b/share/minizinc/std/fzn_dreachable_multiroot_int_reif.mzn new file mode 100644 index 000000000..af657b8ab --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_reachable_multiroot_enum.mzn b/share/minizinc/std/fzn_reachable_multiroot_enum.mzn new file mode 100644 index 000000000..278091b76 --- /dev/null +++ b/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); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_reachable_multiroot_enum_reif.mzn b/share/minizinc/std/fzn_reachable_multiroot_enum_reif.mzn new file mode 100644 index 000000000..27fa9d57f --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_reachable_multiroot_int.mzn b/share/minizinc/std/fzn_reachable_multiroot_int.mzn new file mode 100644 index 000000000..437fbe8f7 --- /dev/null +++ b/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); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_reachable_multiroot_int_reif.mzn b/share/minizinc/std/fzn_reachable_multiroot_int_reif.mzn new file mode 100644 index 000000000..cff0c5848 --- /dev/null +++ b/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"); + +%-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/globals.mzn b/share/minizinc/std/globals.mzn index 80cc77c85..c8d3028f5 100644 --- a/share/minizinc/std/globals.mzn +++ b/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"; diff --git a/share/minizinc/std/reachable_multiroot.mzn b/share/minizinc/std/reachable_multiroot.mzn new file mode 100644 index 000000000..54aecdffe --- /dev/null +++ b/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) + ); diff --git a/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.enum.mzn b/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.enum.mzn new file mode 100644 index 000000000..1be21aa08 --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.enum.mzn @@ -0,0 +1,388 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true +***/ + +include "cluster.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrix; + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES); +enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES); + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint cluster(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrix, GraphNodes, GraphEdges); + +% List all computed matrices. diff --git a/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.int.mzn b/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.int.mzn new file mode 100644 index 000000000..bacf8e3bb --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster-exhaustive-sat.int.mzn @@ -0,0 +1,388 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true +***/ + +include "cluster.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrix; + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +set of int: GRAPH_NODES = 1..NUM_GRAPH_NODES; +set of int: GRAPH_EDGES = 1..NUM_GRAPH_EDGES; + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint cluster(NUM_GRAPH_NODES, NUM_GRAPH_EDGES, GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrix, GraphNodes, GraphEdges); + +% List all computed matrices. diff --git a/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.enum.mzn b/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.enum.mzn new file mode 100644 index 000000000..28c520c89 --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.enum.mzn @@ -0,0 +1,51 @@ +/*** +--- !Test +expected: !Result + status: UNSATISFIABLE +***/ + +include "cluster.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +include "cluster.naive.mzn.model"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrixNaive; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrix; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 5; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES); +enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES); + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint cluster_naive(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrixNaive, GraphNodes, GraphEdges); +constraint cluster (GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrix, GraphNodes, GraphEdges); + +% Look for solutions where matrices *DO NOT* match. +% There should *NOT* be any such solutions. +constraint not(forall (j,i in GRAPH_NODES)( + ReachabilityMatrix[j,i] == ReachabilityMatrixNaive[j,i] +)); diff --git a/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.int.mzn b/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.int.mzn new file mode 100644 index 000000000..0bdc13fd5 --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster-exhaustive-unsat.int.mzn @@ -0,0 +1,51 @@ +/*** +--- !Test +expected: !Result + status: UNSATISFIABLE +***/ + +include "cluster.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +include "cluster.naive.mzn.model"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrixNaive; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrix; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 5; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +set of int: GRAPH_NODES = 1..NUM_GRAPH_NODES; +set of int: GRAPH_EDGES = 1..NUM_GRAPH_EDGES; + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint cluster_naive(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrixNaive, GraphNodes, GraphEdges); +constraint cluster (NUM_GRAPH_NODES, NUM_GRAPH_EDGES, GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrix, GraphNodes, GraphEdges); + +% Look for solutions where matrices *DO NOT* match. +% There should *NOT* be any such solutions. +constraint not(forall (j,i in GRAPH_NODES)( + ReachabilityMatrix[j,i] == ReachabilityMatrixNaive[j,i] +)); diff --git a/tests/spec/unit/globals/cluster/cluster.naive.mzn.model b/tests/spec/unit/globals/cluster/cluster.naive.mzn.model new file mode 100644 index 000000000..aaf5a057d --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster.naive.mzn.model @@ -0,0 +1,32 @@ +include "reachable.mzn"; +include "subgraph.mzn"; + +predicate cluster_naive(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),index_set(es)] of var bool: des, + } 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]) + ) /\ + forall (e in index_set(es))( + es[e] -> r[from[e],to[e]] + ) /\ + forall (j,i,k in index_set(ns) where i > j /\ k != j /\ k != i)( + (r[j,k] /\ r[k,i]) -> r[j,i] + ) /\ + forall (j in index_set(ns), i in index_set(es))( + des[j,i] -> es[i] + ) /\ + forall (j in index_set(ns))( + reachable(from, to, j, r[j,..], array1d(index_set(es),des[j,..])) + ) /\ + % nodes connected by chosen edges must be chosen + subgraph(from,to,ns,es); diff --git a/tests/spec/unit/globals/cluster/cluster_naive-exhaustive-sat.mzn b/tests/spec/unit/globals/cluster/cluster_naive-exhaustive-sat.mzn new file mode 100644 index 000000000..93746d278 --- /dev/null +++ b/tests/spec/unit/globals/cluster/cluster_naive-exhaustive-sat.mzn @@ -0,0 +1,388 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - true + - - true + - true + - true + - - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - true + - - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - false + - - false + - true + - false + - - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - false + - true + - - false + - true + - false + - - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + ReachabilityMatrix: + - - true + - true + - false + - - true + - true + - false + - - false + - false + - true +***/ + +include "reachable.mzn"; +include "subgraph.mzn"; + +include "cluster.naive.mzn.model"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES,GRAPH_NODES] of var bool: ReachabilityMatrix; + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES); +enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES); + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint cluster_naive(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, ReachabilityMatrix, GraphNodes, GraphEdges); + +% List all computed matrices. diff --git a/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.enum.mzn b/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.enum.mzn new file mode 100644 index 000000000..d6bf0575b --- /dev/null +++ b/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.enum.mzn @@ -0,0 +1,5358 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - false + - false + Roots: + - false + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - false + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true +***/ + +include "reachable_multiroot.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES] of var bool: Roots; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i != j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i != j ]; + +%------------------------------------------------------------------------------- + +enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES); +enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES); + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint dreachable_multiroot(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, Roots, GraphNodes, GraphEdges) + +% List all roots. diff --git a/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.int.mzn b/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.int.mzn new file mode 100644 index 000000000..4b9a6b9f1 --- /dev/null +++ b/tests/spec/unit/globals/reachable_multiroot/dreachable_multiroot-exhaustive-sat.int.mzn @@ -0,0 +1,5358 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - false + - false + Roots: + - false + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - false + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true +***/ + +include "reachable_multiroot.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES] of var bool: Roots; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i != j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i != j ]; + +%------------------------------------------------------------------------------- + +set of int: GRAPH_NODES = 1..NUM_GRAPH_NODES; +set of int: GRAPH_EDGES = 1..NUM_GRAPH_EDGES; + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint dreachable_multiroot(NUM_GRAPH_NODES, NUM_GRAPH_EDGES, GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, Roots, GraphNodes, GraphEdges) + +% List all roots. diff --git a/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.enum.mzn b/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.enum.mzn new file mode 100644 index 000000000..ccf7c2200 --- /dev/null +++ b/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.enum.mzn @@ -0,0 +1,748 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - false + Roots: + - false + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false +***/ + +include "reachable_multiroot.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES] of var bool: Roots; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES); +enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES); + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint reachable_multiroot(GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, Roots, GraphNodes, GraphEdges) + +% List all roots. diff --git a/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.int.mzn b/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.int.mzn new file mode 100644 index 000000000..a69ee8ade --- /dev/null +++ b/tests/spec/unit/globals/reachable_multiroot/reachable_multiroot-exhaustive-sat.int.mzn @@ -0,0 +1,748 @@ +/*** +--- !Test +options: + all_solutions: true +expected: !Result + status: ALL_SOLUTIONS + solution: !SolutionSet + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - false + Roots: + - false + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - false + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - false + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - false + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - false + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - false + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - true + - !Solution + GraphEdges: + - false + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - false + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false + - !Solution + GraphEdges: + - true + - true + - false + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - false + - true + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - false + - false + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - false + - true + - false + - !Solution + GraphEdges: + - true + - true + - true + GraphNodes: + - true + - true + - true + Roots: + - true + - true + - false +***/ + +include "reachable_multiroot.mzn"; + +include "reachable.mzn"; +include "subgraph.mzn"; + +%------------------------------------------------------------------------------- + +array[GRAPH_NODES] of var bool: GraphNodes; % free variable +array[GRAPH_EDGES] of var bool: GraphEdges; % free variable +array[GRAPH_NODES] of var bool: Roots; % free variable + +%=============================================================================== + +int: NUM_GRAPH_NODES = 3; % par +int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); +array[GRAPH_EDGES] of tuple(GRAPH_NODES,GRAPH_NODES): GRAPH_NODE_PAIRS = [ (j,i) | j,i in GRAPH_NODES where i > j ]; + +%------------------------------------------------------------------------------- + +set of int: GRAPH_NODES = 1..NUM_GRAPH_NODES; +set of int: GRAPH_EDGES = 1..NUM_GRAPH_EDGES; + +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ p.1 | p in GRAPH_NODE_PAIRS ]; +array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ p.2 | p in GRAPH_NODE_PAIRS ]; + +constraint subgraph( + GRAPH_LEAVING_NODE, + GRAPH_ENTERING_NODE, + GraphNodes, + GraphEdges +); + +%------------------------------------------------------------------------------- + +constraint reachable_multiroot(NUM_GRAPH_NODES, NUM_GRAPH_EDGES, GRAPH_LEAVING_NODE, GRAPH_ENTERING_NODE, Roots, GraphNodes, GraphEdges) + +% List all roots.