Home

Union-Find

Interactive lab — UF solver with path compression & union by rank

QF_UF · Flat Cube
Flat Cube Input
⚠ Formula is not flat — UF requires a flat cube
Union-Find requires all literals to be in flat form (all function arguments must be variables).
You can auto-flatten here, or open the Flatten Lab to do it step by step.
Input a flat cube: equalities =, disequalities !=. All arguments must be variables. Literals separated by ,.
Examples:
UF Actions
Auto-Solve
Applies all Union steps, then checks all disequalities with Find.
What can I do?
Load a flat cube to begin.
Flat Cube
Load a formula to see literals here.
Union-Find Forest
✓ SATISFIABLE
No rules apply and no disequality is contradicted — the cube is SAT.
✗ UNSATISFIABLE
A disequality is contradicted.
Initialize to see the forest.
Step History
No steps yet.
Union
Choose an equality from the cube to union the two sides. Uses union by rank; find() with path compression is applied automatically.
Find — Check Disequality
Choose a disequality x≠y. find(x) and find(y) are called (compressing paths). If they return the same root → UNSAT; otherwise → no conflict.