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

Equality saturation explores equivalent program expressions via e-graphs, and its extraction step selects one representative per equivalence class to form an output tree. Standard extraction minimizes a decomposable per-node cost function that cannot capture multi-node structural patterns arising in SMT preprocessing and compiler instruction selection. We formalize pattern-aware extraction as a weighted pattern cover problem on AND-OR DAGs and establish its correspondence to tree covering in instruction selection. Three challenges arise when migrating tree covering to e-graphs: 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, generalizing BURS tree covering from fixed trees to AND-OR DAGs. A bottom-up pass computes optimal DP values, and 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·K·|P|·Cmax) time. The evaluation targets extraction-level coverage, since end-to-end performance additionally depends on rewrite-rule design and saturation completeness. On SMT-COMP benchmarks, the algorithm achieves up to 31× higher weighted pattern coverage than standard extraction. Depth-2 tiling contributes 45–51% additional improvement, with overhead within 1.5× of standard extraction.