一句话：提出带标签并查集，并基于它构造可高效表示关系约束的抽象域，用于程序分析与 SMT 求解。
经典并查集只能高效表示等价关系，难以直接刻画更一般的关系约束。本文提出带标签并查集：在并查集边上附加满足群公理的标签与复合运算，使其可高效计算关系的传递闭包，并能表示等价类之间的单射变换，包括 y=a×+b 形式的双变量每等式（TVPE）约束。作者在抽象解释框架下研究以抽象关系为标签时导出的性质，以及它与其他约束表示的组合，从而提升精度并简化已有约束。该抽象效率较高，在基于抽象解释的程序分析和 SMT 约束求解两个用例中取得初步积极结果。
We introduce a new family of abstractions based on a data structure that we call labeled union-find , an extension of the classic efficient union-find data structure where edges carry labels. These labels have a composition operation that obey the group axioms. Like union-find, the labeled version can efficiently compute the transitive closure of a relation, but it is not limited to equivalence relations; it can represent any injective transformation between equivalence classes, which includes two-variables per equality (TVPE) constraints of the form y = a × + b . Using abstract interpretation theory, we study the properties deriving from the use of abstract relations as labels, and the combination of labeled union-find with other representations of constraints, allowing both improvements in precision and simplification of existing constraints. Due to its efficiency, the labeled union-find abstractions could find many uses; we use it in two use cases, program analysis based on abstract interpretation and constraint solving for SMT, with encouraging preliminary results.
@article{paperbot3068,
title = {Relational Abstractions Based on Labeled Union-Find},
author = {Dorian Lesbre and Matthieu Lemerre and Hichem Rami Ait-El-Hara and François Bobot},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729298}
}