一句话：首次形式化直接支持不等式的 e-graph，证明其比等式嵌入编码更高效，并在 egg 中实现验证。
E-graph 是紧凑表示程序空间并推理项相等性的数据结构，已用于程序优化与自动定理证明。但许多应用还需推理不等式，虽可编码实现，直接支持却能提升性能并简化元理论。本文提出与具体实现无关的形式化框架，首次证明 e-graph 等价于其所编码等价关系的自反、对称、传递与同余闭包。基于此，作者首次形式化直接支持不等式的 e-graph 扩展，并从解析上证明其效率优于 SMT 求解器与自动验证器常用的嵌入技术。他们通过剖析发现 SMT 求解器处理不等式耗时可观，并在 Rust 的 egg 库中实现该扩展，于 SMT 求解器与自动定理证明器上用标准基准评估，结果证实直接支持不等式优于等式嵌入编码。
E-graphs are a data structure to compactly represent a program space and reason about equality of program terms. E-graphs have been successfully applied to a number of domains, including program optimization and automated theorem proving. In many applications, however, it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory. In this paper, we develop a framework independent of a specific implementation to formally reason about e-graphs. For the first time, we prove the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of the equivalence relation they are expected to encode. We use these results to present the first formalization of an extension of e-graphs that directly supports disequalities and prove an analytical result about their superior efficiency compared to embedding techniques that are commonly used in SMT solvers and automated verifiers. We further profile an SMT solver and find that it spends a measurable amount of time handling disequalities. We implement our approach in an extension to egg, a popular e-graph Rust library. We evaluate our solution in an SMT solver and an automated theorem prover using standard benchmarks. The results indicate that direct support for disequalities outperforms other encodings based on equality embedding, confirming the results obtained analytically.
@article{paperbot3226,
title = {Dis/Equality Graphs},
author = {George Zakhour and Pascal Weisenburger and Jahrim Gabriele Cesario and Guido Salvaneschi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704913}
}