Disequalities in E-Graphs: An Experiment
summary
Implements disequalities inside egg as a lightweight extension called dis that adds a forbid field to e-classes and a disunion operation to record class-level disequality edges; compares that to embedding disequalities as equalities. On synthetic tests (15k equalities, 30k pairs) embedding finds contradictions faster but causes exponential saturation during construction; on SMT‑EUF benchmarks (1,600 solved files) embedding yields 66% more nodes and is 10× slower to decide consistency, though SAT-solving time is not measured.
AI-written summary · about
chapters (17)
- 0:00Disequalities in e-graphs
- 0:23Propel experiment context
- 1:27Propel algebra and types
- 3:37Propel case analysis
- 6:01Disequalities in proofs
- 9:12Storing equalities
- 10:16E-graph limitations
- 12:00Equality as uninterpreted function
- 13:46Disequalities in SMT solvers
- 14:52Disequalities between e-classes
- 15:35Disequality edges in e-graphs
- 16:19Implementing disequality edges
- 18:07Embedding vs disequality edges
- 19:12Performance with S-expressions
- 20:37EUF benchmark testing
- 22:01Conclusion and future work
- 22:53Q&A
related talks
30megg: Fast and Extensible Equality Saturation
20mEquality Saturation and Joins
19mDestructive E-Graph Rewrites
24mIncremental Equality Saturation
17mBetter Together: Unifying Datalog and Equality Saturation
21mImproving Equality Saturation for EDA via Semantic E-Graphs
23mVersioned E-Graphs
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching