WiP: Labeled Union-Find for Constraint Factorization
summary
A new data structure called labeled union-find stores group-structured labels on union‑find edges and exposes find/union/get operations with path compression to recover relations between variables cheaply, representing only invertible pairwise relations like y = ax + b (a invertible modulo) or XOR/rotations as injective relations. The idea is constraint factorization*: group related variables to shrink other domains, doing fewer propagations. Early implementation integrates with a SEC-based nonrelational analysis, shows under ~10% overhead, and still needs a join algorithm for flow sensitivity.
AI-written summary · about
chapters (15)
- 0:00Labeled union-find intro
- 1:05Cheaper relational abstract domain
- 2:31Costly weakly relational domains
- 5:21Constraint elimination to reduce costs
- 7:56Group structure and label union-find
- 10:05Label union-find operations
- 12:54Group properties and injective functions
- 14:43Representable relations in domain
- 16:52Application in SEC-based domains
- 19:03Constraint factorization and grouping
- 20:46Summary of label union-find
- 22:14Future applications and challenges
- 23:00Q&A motivation/examples
- 25:05Q&A overhead/implementation
- 26:30Q&A vs egraphs
related talks
21mRelational Abstractions Based on Labeled Union-Find
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
21mMax-3-Lin over Non-Abelian Groups with Universal Factor Graphs
26mConstraining Complexity in the Generics Design
01h 02mTheory and Control
14mPredicate E-Graphs with Symbolic Conditional Rewriting
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...