Taming Equality Saturation by Synthesizing Reusable Strategies

Equality Saturation (EqSat) compactly represents equivalent program variants in an e-graph and explores them through rewrite rules, exposing optimization opportunities overlooked by heuristic pass pipelines in conventional compilers. However, retaining these alternatives can cause exponential e-graph growth, incurring prohibitive runtime and memory overhead. Consequently, practical EqSat requires carefully engineered search control to orchestrate rewrite applications and constrain e-graph growth, which demands extensive manual effort. Large Language Models (LLMs) offer a promising way to automate this process, yet existing formulations typically optimize EqSat control separately for each input, causing domain-level optimization insights to be repeatedly rediscovered. Moreover, LLM-based EqSat search remains difficult because of the low-level controls, risky candidate evaluation, and weak refinement feedback exposed by existing systems. We present EGGMIND, a framework that addresses these issues by reformulating EqSat optimization as offline synthesis of reusable strategies followed by online reuse. EGGMIND introduces EqSatL, an executable structured representation of saturation strategies that exposes high-level decisions over rewrite interactions and simplification. Its synthesis process combines proof-derived structural feedback with tractability guidance to efficiently refine candidate strategies across representative program instances. The resulting strategies can be reused for unseen related programs without LLM calls. Evaluations show that EGGMIND consistently improves both solution quality and resource efficiency. Compared with unguided EqSat, it reduces expression cost by 54.6%, while achieving a $69.5\times$ runtime speedup and a 91.8% reduction in peak memory. It also achieves an $8.7\times$ speedup over an expert-designed strategy while matching or improving its solution quality.