Interesting applications of union-find

I've been trying to find interesting applications of union-find that are lesser known. Here are some popular algorithms based on union-find that I know:

• Kruskal's algorithm for MST

• Tarjan's off-line lowerst common ancestors (LCA) algorithm 1

• Solving range minimum queries using union-find by reduction to LCA (with $O(m+n)$ bound given by [Tarjan & Gabow '83, see 1]

• Finding connected components

• Various textbook examples

Question: What are some interesting use-cases of union-find inside a larger, more complicated algorithm that are lesser-known?

Here are two additional interesting uses of union find in formal methods and programming languages, that are perhaps lesser-known at an undergraduate level.

• Decision procedure for the quantifier free fragment of theory of equality for uninterpreted functions in Satisfiability Modulo Theory (SMT) solving (https://www.cs.utexas.edu/~isil/cs389L/lecture11-6up.pdf). In this particular case, we are given (quantifier-free) logical formulas that range over constant symbols, (possibly uninterpreted) function symbols, and equality. We are asked to decide whether such a formula is satisfiable.

• Tarjan's algorithm for dominator tree construction and path expression computation over a directed graph (https://dl.acm.org/doi/pdf/10.1145/322261.322273) all use ideas or variants of the union-find data structure.

The bottom line is, in each case above we seek to partition some particular set of elements into equivalence classes. Union-find is very effective in keeping track of the equivalence class each object belongs to and updating such information.

StackExchange Computer Science Q#108659, answer score: 2