138 Graph Theory — Union Find
138.1 Overview
This module establishes the correctness of the union–find data structure used by Kruskal’s algorithm: the relation \(\mathtt{SamePartition}\) is an equivalence, merging along a list of edges is invariant under permutation of that list, and two vertices end up in the same component after merging all edges exactly when they are connected by a path in the corresponding edge set.
138.2 Declarations
Every union–find state \(\mathit{uf} : \mathtt{UF}\, n\) induces the same partition as itself: \(\mathtt{SamePartition}\, \mathit{uf}\, \mathit{uf}\).
If \(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_2\) then \(\mathtt{SamePartition}\, \mathit{uf}_2\, \mathit{uf}_1\).
If \(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_2\) and \(\mathtt{SamePartition}\, \mathit{uf}_2\, \mathit{uf}_3\), then \(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_3\). Together with reflexivity and symmetry, \(\mathtt{SamePartition}\) is an equivalence relation on union–find states.
If two vertices \(i, j\) already carry the same representative, \(\mathit{uf}\, i = \mathit{uf}\, j\), then merging them leaves the state unchanged: \(\mathit{uf}.\mathtt{merge}\, i\, j = \mathit{uf}\).
If \(\mathit{uf}\, a = \mathit{uf}\, b\), then for any list of weighted edges \(\mathit{edges}\) we still have \((\mathit{uf}.\mathtt{mergeAll}\, \mathit{edges})\, a = (\mathit{uf}.\mathtt{mergeAll}\, \mathit{edges})\, b\); that is, merging never splits vertices that are already in the same component.
Suppose the union–find state \(\mathit{uf}\) represents reachability in a base edge list, i.e. \(\mathit{uf}\, a = \mathit{uf}\, b \leftrightarrow \mathtt{Reach}\, \mathit{base}\, a\, b\) for all \(a, b\). Then after merging along \(\mathit{edges}\),
Starting from the initial union–find state \(\mathtt{UF.init}\, n\), in which every vertex is its own component, two vertices \(a, b\) end up with the same representative after merging along \(\mathit{edges}\) if and only if \(\mathtt{Reach}\, \mathit{edges}\, a\, b\).
If \(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_2\), then merging both states along the same edge list preserves this: \(\mathtt{SamePartition}\, (\mathit{uf}_1.\mathtt{mergeAll}\, \mathit{edges})\, (\mathit{uf}_2.\mathtt{mergeAll}\, \mathit{edges})\).
For any state \(\mathit{uf}\) and edges \(a, b\), merging the endpoints of \(a\) and then those of \(b\) yields the same partition as merging them in the opposite order: \(\mathtt{SamePartition}\, ((\mathit{uf}.\mathtt{merge}\, a.u\, a.v).\mathtt{merge}\, b.u\, b.v)\, ((\mathit{uf}.\mathtt{merge}\, b.u\, b.v).\mathtt{merge}\, a.u\, a.v)\).
If the edge lists \(l_1\) and \(l_2\) are permutations of each other, then merging along them gives the same partition: \(\mathtt{SamePartition}\, (\mathit{uf}.\mathtt{mergeAll}\, l_1)\, (\mathit{uf}.\mathtt{mergeAll}\, l_2)\).
Merging along \(l \mathbin {+\! \! +} [e]\) equals first merging along \(l\) and then merging the endpoints of \(e\): \(\mathit{uf}.\mathtt{mergeAll}\, (l \mathbin {+\! \! +} [e]) = (\mathit{uf}.\mathtt{mergeAll}\, l).\mathtt{merge}\, e.u\, e.v\).
Merging along \(e :: S\) gives the same partition as first merging the endpoints of \(e\) and then merging along \(S\): \(\mathtt{SamePartition}\, (\mathit{uf}.\mathtt{mergeAll}\, (e :: S))\, ((\mathit{uf}.\mathtt{merge}\, e.u\, e.v).\mathtt{mergeAll}\, S)\).
If \(e \in l\) for an edge list \(l\), then \(l\) is a permutation of \(l.\mathtt{erase}\, e \mathbin {+\! \! +} [e]\).