PLDI 2026 (series) / EGRAPHS 2026 (series) / EGRAPHS /
Augmenting Rewrite Rule Sets via Knuth-Bendix Completion
Mon 15 Jun 2026 11:30 - 11:55 at Meadows CD - Session 2
Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem.
However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations.
In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.
Mon 15 JunDisplayed time zone: Mountain Time (US & Canada) change
Mon 15 Jun
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:20 | |||
10:40 25mTalk | A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching. EGRAPHS Remi Delmas Amazon Web Services Pre-print | ||
11:05 25mTalk | Associativity and Commutativity in Equality Saturation EGRAPHS Tarik Rosin Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:30 25mTalk | Augmenting Rewrite Rule Sets via Knuth-Bendix Completion EGRAPHS Michael Schifferer Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus Pre-print | ||
11:55 25mTalk | E-graphs modulo theoriesRemote EGRAPHS Sofia Brookie Chalmers University of Technology | ||