一句话：针对 e-graph 提取的 NP 难与不可近似性，提出稀疏低树宽 e-graph 的最优提取参数化算法及 Rust 实现。
等式饱和（equality saturation）依赖从 e-graph 中提取最优项，但该提取问题一般 NP 难，现有工具或使用缓慢的 ILP 最优算法，或使用可能远离最优的启发式。作者进一步证明 e-graph 提取在任意常数因子内不可近似，说明最坏情况下启发式会严重次优。为此，论文利用实际 e-graph 常具有稀疏性，提出一种面向低树宽 e-graph 的参数化最优提取算法，并证明其正确性。作者用 Rust 实现该算法，并在 Cranelift 基准上与 ILP 比较。实验表明，对树宽最高为 10 的 e-graph，该算法能在远少于 ILP 的时间内完成最优提取，为需要从稀疏 e-graph 提取最优项的用户提供了实用工具。
Equality graphs (e-graphs) are used to compactly represent equivalence classes of terms in symbolic reasoning systems. Beyond their original roots in automated theorem proving, e-graphs have been used in a variety of applications. They have become particularly important as the key ingredient in the popular technique of equality saturation , which has notable applications in compiler optimization, program synthesis, program verification, and symbolic execution, among others. In a typical equality saturation workflow, an e-graph is used to store a large number of equalities that are generated by local rewrites during a saturation phase, after which an optimal term is extracted from the e-graph as the output of the technique. However, despite its crucial role in equality saturation, e-graph extraction has received relatively little attention in the literature, which we seek to start addressing in this paper. Extraction is a challenging problem and is notably known to be NP-hard in general, so current equality saturation tools rely either on slow optimal extraction algorithms based on integer linear programming (ILP) or on heuristics that may not always produce the optimal result. In fact, in this paper, we show that e-graph extraction is hard to approximate within any constant ratio. Thus, any such heuristic will produce wildly suboptimal results in the worst case. Fortunately, we show that the problem becomes tractable when the e-graph is sparse, which is the case in many practical applications. We present a novel parameterized algorithm for extracting optimal terms from e-graphs with low treewidth, a measure of how “tree-like” a graph is, and prove its correctness. We also present an efficient Rust implementation of our algorithm and evaluate it against ILP on a number of benchmarks extracted from the Cranelift benchmark suite, a real-world compiler optimization library based on equality saturation. Our algorithm optimally extracts e-graphs with treewidths of up to 10 in a fraction of the time taken by ILP. These results suggest that our algorithm can be a valuable tool for equality saturation users who need to extract optimal terms from sparse e-graphs.
@article{GoharshadyLP24,
title = {Fast and Optimal Extraction for Sparse Equality Graphs},
author = {Amir Kafshdar Goharshady and Chun Kit Lam and Lionel Parreaux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689801}
}