E-graphs modulo theories
summary
Develops E-graphs modulo theories to avoid the exponential (≈2^n) blow-up that AC causes, connects AC closure to the word problem and Buchberger‑style completion, and implements a prototype that compares AC completion vs plain AC saturation by measuring final e‑graph size. Results show AC completion produces much smaller graphs (green points below the diagonal), savings grow with input size, but the underlying problem is space‑complete. Also sketches terminating AC matching via oriented rewrite rules; implementation is functional but not performance‑tuned.
AI-written summary · about
chapters (10)
- 0:00E-graphs modulo theories intro
- 1:06AC causes e-graph explosion
- 3:09Motivation for theory solvers
- 6:57AC closure in e-graphs
- 11:12Side table vs integrated AC closure
- 13:37AC closure and word problem
- 15:44AC closure fundamental step
- 17:08AC matching challenges
- 19:12Summary and future work
- 19:34Q&A
related talks
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
38mE-graphs and Automated Reasoning: Looking back to look forward
23mVersioned E-Graphs
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
37mEquivalence Hypergraphs: E-Graphs for Monoidal Theories
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
25mEGSTRA: E-Graph-Based Strategy for Test Suite Reduction and Abstraction