Incremental Equality Saturation
summary
Introduces an incremental egraph with per–e-class versions and a top-K analysis (K=2) so rewrites only target e-classes created by the current version and inner matches pick from the lowest-cost K enodes. Implementation reuses egg, uses a node-limit budget, and a local cost analysis; on 1,000 randomly generated algebraic terms (sizes 11/13) incremental ESAT becomes Pareto-optimal versus standard ESAT as budget grows, runs about 3x faster at 6,400 enodes but misses better results for 40/1,000 terms; requires a local cost function.
AI-written summary · about
chapters (11)
- 0:00Incremental equality saturation intro
- 1:03Batched saturation limits
- 2:50Core idea of incremental ES
- 4:16Example walkthrough
- 6:22Versions and e-matching
- 7:23Top K for runaway e-class
- 9:11Soundness and coverage of EKSAT
- 11:00Version policies for performance
- 13:06Performance results
- 14:54Limitations and future work
- 15:34Q&A
related talks
30megg: Fast and Extensible Equality Saturation
20mEquality Saturation and Joins
23mRewrite System Showdown: Stochastic Search vs. EqSat
21mImproving Equality Saturation for EDA via Semantic E-Graphs
23mVersioned E-Graphs
28mCERES: Making Equality Saturation Memory-Scalable
24mOptimism in Equality Saturation
25mDisequalities in E-Graphs: An Experiment
