Rewrite System Showdown: Stochastic Search vs. EqSat
summary
Compares stochastic search (128-thread implementation) to equality saturation (egg/egglog style) across five benchmarks: matrix-chain (optimal known; stochastic stays near-optimal past ~300 matrices while e-graphs collapse), trig identities (23/35 both solved; split failures), indefinite integrals (similar split), Zelinski decompilation (2,000 cases: ~600 ties, ~800 e-graph wins, ~730 stochastic wins), and Halide inequalities (large set unsolved). Implements a stochastic engine matching egg’s interface and shows neither method dominates; hybrid pulsing improves e-graphs.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:01Equality saturation limits
- 3:51Stochastic search alternative
- 6:21Matrix chain multiplication
- 8:48Trigonometric simplification
- 10:14Indefinite integration
- 12:23Zelenski decompilation
- 15:52Halide inequality proofs
- 16:54Key takeaways
- 17:57Equational program optimization
- 19:01Future directions
- 19:43Q&A
related talks
30megg: Fast and Extensible Equality Saturation
24mIncremental Equality Saturation
20mEquality Saturation and Joins
17mBetter Together: Unifying Datalog and Equality Saturation
24mOptimism in Equality Saturation
19mEquality Saturation for Quantum Circuit Optimization
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
22mUsing Equality Saturation and Stochastic Mutations for Molecular Dynamics Code(…)