{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T18:10:43Z","timestamp":1778523043400,"version":"3.51.4"},"reference-count":15,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T00:00:00Z","timestamp":1778457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>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\u2013tiling 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\u00b7K\u00b7|P|\u00b7Cmax) 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\u00d7 higher weighted pattern coverage than standard extraction. Depth-2 tiling contributes 45\u201351% additional improvement, with overhead within 1.5\u00d7 of standard extraction.<\/jats:p>","DOI":"10.3390\/a19050377","type":"journal-article","created":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:17:42Z","timestamp":1778519862000},"page":"377","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exact Pattern-Aware Extraction for Equality Saturation via Bounded-Depth Tree Covering"],"prefix":"10.3390","volume":"19","author":[{"given":"Zi","family":"Cheng","sequence":"first","affiliation":[{"name":"School of Computer Science, Wuhan University, Wuhan 430072, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8758-8668","authenticated-orcid":false,"given":"Mengting","family":"Yuan","sequence":"additional","affiliation":[{"name":"School of Computer Science, Wuhan University, Wuhan 430072, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0542-2280","authenticated-orcid":false,"given":"Lefei","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computer Science, Wuhan University, Wuhan 430072, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2026,5,11]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast Decision Procedures Based on Congruence Closure","volume":"27","author":"Nelson","year":"1980","journal-title":"J. ACM"},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/3434304","article-title":"Egg: Fast and Extensible Equality Saturation","volume":"5","author":"Willsey","year":"2021","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., and Lerner, S. (2009). Equality Saturation: A New Approach to Optimization. Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201909), Savannah, GA, USA, 21\u201323 January 2009, ACM.","DOI":"10.1145\/1480881.1480915"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Coward, S., Constantinides, G.A., and Drane, T. (2023). Automating Constraint-Aware Datapath Optimization Using E-Graphs. Proceedings of the 60th ACM\/IEEE Design Automation Conference (DAC \u201923), San Francisco, CA, USA, 9\u201313 July 2023, IEEE.","DOI":"10.1109\/DAC56929.2023.10247797"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"VanHattum, A., Nigam, R., Lee, V.T., Bornholt, J., and Sampson, A. (2021). Vectorization for Digital Signal Processors via Equality Saturation. Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS \u201921), Lausanne, Switzerland, 19\u201323 April 2021, ACM.","DOI":"10.1145\/3445814.3446707"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Nandi, C., Willsey, M., Anderson, A., Wilcox, J.R., Darulova, E., Grossman, D., and Tatlock, Z. (2020). Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201920), London, UK, 15\u201320 June 2020, ACM.","DOI":"10.1145\/3385412.3386012"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"De Moura, L., and Bj\u00f8rner, N. (2008). Z3: An Efficient SMT Solver. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908), Budapest, Hungary, 29 March\u20136 April 2008, Springer.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref_8","unstructured":"Blindell, H. (2016). Instruction Selection, Springer International Publishing."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1145\/69558.75700","article-title":"Code Generation Using Tree Matching and Dynamic Programming","volume":"11","author":"Aho","year":"1989","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Pelegri-Llopart, E., and Graham, S.L. (1988). Optimal Code Generation for Expression Trees: An Application of BURS Theory. Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201988), San Diego, CA, USA, 10\u201313 January 1988, ACM.","DOI":"10.1145\/73560.73586"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1145\/543552.512566","article-title":"Denali: A Goal-Directed Superoptimizer","volume":"37","author":"Joshi","year":"2002","journal-title":"ACM SIGPLAN Not."},{"key":"ref_12","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., and Panchekha, P. (2022). Small Proofs from Congruence Closure. Proceedings of the 2022 Formal Methods in Computer-Aided Design (FMCAD \u201922), Trento, Italy, 17\u201321 October 2022, IEEE."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1145\/203095.203098","article-title":"BURS Automata Generation","volume":"17","author":"Proebsting","year":"1995","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Koes, D.R., and Goldstein, S.C. (2008). Near-Optimal Instruction Selection on DAGs. Proceedings of the 6th Annual IEEE\/ACM International Symposium on Code Generation and Optimization (CGO \u201908), Boston, MA, USA, 5\u20139 April 2008, ACM.","DOI":"10.1145\/1356058.1356065"},{"key":"ref_15","unstructured":"Barrett, C., Fontaine, P., and Tinelli, C. (2017). The SMT-LIB Standard: Version 2.6, Department of Computer Science, The University of Iowa. Available online: https:\/\/www.SMT-LIB.org."}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/19\/5\/377\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:31:29Z","timestamp":1778520689000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/19\/5\/377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,11]]},"references-count":15,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2026,5]]}},"alternative-id":["a19050377"],"URL":"https:\/\/doi.org\/10.3390\/a19050377","relation":{},"ISSN":["1999-4893"],"issn-type":[{"value":"1999-4893","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,5,11]]}}}