Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
summary
JijModeling separates symbolic formula from input data and uses e-graphs to detect structured constraints like SOS1 so solvers can use dedicated APIs; benchmarks on a two‑plant placement family show solve time grows exponentially without detection but stays near linear/constant with detection for n up to ~60, yielding dramatic speedups. Detection overhead runs about 1 second, saturation benefits from bidirectional and reductive rules (one case drops from ~5s to <1s), and a Rust utility egg_recursive eases writing recursive egg terms.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:44Motivation and constraints
- 5:39Symbolic egraphs in JJ
- 7:26SOS constraints impact
- 11:00Case study: egraph detection
- 16:50Lessons from egg development
- 19:03Future work and conclusion
- 21:13Q&A on egraph extraction
related talks
13mProgram Analysis via Efficient Symbolic Abstraction
15mInter-theory Dependency Analysis for SMT String Solvers
19mAn Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu...
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
24mOptimism in Equality Saturation
15mFormulog: Datalog for SMT-Based Static Analysis
33mSolving constraints during type inference
17mBetter Together: Unifying Datalog and Equality Saturation