Exact Pattern-Aware Extraction for Equality Saturation via Bounded-Depth Tree Covering

Equality saturation explores equivalent program expressions via e-graphs, and its final step—extraction—selects one representative per equivalence class to form an output tree. Standard extraction minimizes a decomposable, single-node cost function that cannot capture multi-node structural patterns exploited by downstream systems such as SMT preprocessors and compiler backends. We formalize pattern-aware extraction as a weighted pattern cover problem on AND-OR directed acyclic graphs and establish its correspondence to tree covering in compiler instruction selection. Three challenges arise: annotation ambiguity from multiple candidates per class, context-dependent selection from depth-2 templates, and DAG sharing conflict. We show that the coupled selection-tiling problem reduces to a tree DP with three mutually exclusive tile-role states—independent, tile-root, and tile-leaf—generalizing BURS tree covering from fixed trees to AND-OR DAGs. A bottom-up pass computes optimal DP values; a top-down pass traces back decisions to produce the output tree. For template depth at most two, the algorithm computes an exact optimum in ( O(N cdot K cdot |mathcal{P}| cdot C_{max}) ) time. Experiments on SMT-COMP hardware verification benchmarks show up 31× higher weighted pattern coverage than standard extraction, with depth-2 tiling contributing 45–51% additional improvement and overhead remaining within 2–3×, demonstrating exact, context-sensitive extraction at practical cost.