int: NUM_GRAPH_NODES = 7; % par
int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); % par
enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES);
enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES);
enum DISJOINT_SUBGRAPH_INDICES = DG(1..NUM_GRAPH_NODES);
enum DISJOINT_SUBGRAPH_NODES = DGn(GRAPH_NODES);
enum DISJOINT_SUBGRAPH_EDGE_INDICES = DGe(DISJOINT_SUBGRAPH_INDICES);
array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE = [ j | j,i in GRAPH_NODES where i > j ];
array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ i | j,i in GRAPH_NODES where i > j ];
array[GRAPH_NODES] of var bool: GraphNodes; % par
array[GRAPH_EDGES] of var bool: GraphEdges; % par
array[GRAPH_EDGES] of DISJOINT_SUBGRAPH_NODES: DISJOINT_SUBGRAPH_LEAVING_NODE = [DGn(GRAPH_LEAVING_NODE[e]) | e in GRAPH_EDGES];
array[GRAPH_EDGES] of DISJOINT_SUBGRAPH_NODES: DISJOINT_SUBGRAPH_ENTERING_NODE = [DGn(GRAPH_ENTERING_NODE[e]) | e in GRAPH_EDGES];
array[GRAPH_NODES] of var DISJOINT_SUBGRAPH_INDICES: NodeDisjointSubgraphIndex;
array[DISJOINT_SUBGRAPH_NODES] of var bool: NodeRootnessMask;
array[GRAPH_NODES] of var GRAPH_NODES: parent;
array[GRAPH_NODES,GRAPH_NODES] of var bool: HardWires;
constraint forall (j,i in GRAPH_NODES)(
let {
GRAPH_NODES: m = min(i,j);
GRAPH_NODES: M = max(i,j);
} in
HardWires[m,M] == ((m,M) == (1,2) \/ (m,M) == (2,3) \/ (m,M) == (2,7) \/ (m,M) == (4,5))
);
constraint forall (n in GRAPH_NODES)(
GraphNodes[n] == exists(HardWires[n,..])
);
constraint forall (e in GRAPH_EDGES)(
GraphEdges[e] == HardWires[GRAPH_LEAVING_NODE[e],GRAPH_ENTERING_NODE[e]]
);
constraint forall(n in GRAPH_NODES)(
parent[n] != n -> exists(e in index_set(GRAPH_LEAVING_NODE) where GRAPH_ENTERING_NODE[e] = n)(GraphEdges[e] /\ GRAPH_LEAVING_NODE[e] = parent[n])
);
$ minizinc --version
MiniZinc to FlatZinc converter, version 2.8.5
Probably not fully reduced: