Source-linked AI summary
Associativity and Commutativity in Equality Saturation
Tarik Rosin, Marcel Ullrich, Sebastian Hack
TL;DR
E-graphs can grow exponentially, with AC rules contributing to the blowup. The paper extends relational e-matching for AC operators using multiset storage and implicit subterms. It reports asymptotically lower memory in some cases, while noting theory-dependent savings and a worst case that remains exponential.
Problem
E-graphs can grow exponentially, even for small programs, and associativity and commutativity are known sources of combinatorial blowup.
Source: §1 · p. 1Method
The paper extends relational e-matching with indexed relations for AC operators, storing terms as multisets and managing subterms implicitly.
Source: §1 · p. 1, §2.2 · p. 3Results
The approach uses asymptotically less memory than traditional e-graphs, with savings that depend on the theory and a worst case that remains exponential.
Source: §4 · p. 6Takeaways & Limitations
The paper quantifies AC-related growth with O(2^n) bounds for both e-nodes and e-classes, while reporting reduced e-graph size in its evaluation.
Source: §3 · p. 4, §4 · p. 6The AC matching approach is incomplete: a pattern variable may not bind to a subset of e-class ids, and the significance of this loss remains for further research.
Source: §2.2 · p. 3
Abstract
from arXiv · showhide
Equality saturation is a promising technique for program optimization which sidesteps the phase ordering problem. However, current e-graph implementations grow exponentially large, even for simple examples. Many practical applications involve associative and commutative (AC) operators. We present an extension of relational e-matching that handles AC operators natively by storing terms as multisets. Preliminary results show that equality saturation modulo AC uses asymptotically less memory in certain cases.
1 Motivation
Equality saturation explores equivalent programs while retaining flexibility, but e-graphs can grow combinatorially, especially under associative and commutative rules. For a sum of n variables, the section bounds an AC-saturated graph’s e-classes and e-nodes explicitly.
1 Motivation
- E-graphs store explored programs compactly, permit bidirectional rewriting without non-productive cycles, and allow extraction of the best program found so far at any time.They avoid requiring a term ordering or another canonicalization strategy.Source: §1 · p. 1
- E-graphs can explode even for small programs and few rewrite rules, and associativity and commutativity are known sources of combinatorial blowup.AC rules are used in hardware synthesis, program optimization, and theorem proving.Source: §1 · p. 1
- With associativity and the rule x · 0 = 0, rewriting the initial term a · 0 can repeatedly produce larger terms such as (a · a) · 0.The process starts when the equality a · 0 = 0 permits backward substitution into the initial term.Source: §1 · p. 1
1.1 Bounds
- For a root sum of n variables, an AC-saturated e-graph has 2^n - 1 e-classes.Each class corresponds to a non-empty subset of variables, regardless of order or brackets.Source: §1.1 · p. 2
- An AC-saturated e-graph for a root sum of n variables has 3^n - 2^(n+1) + n + 1 e-nodes.The count adds possible distributions of variable sets across non-leaf nodes and the n leaf nodes.Source: §1.1 · p. 2
2 Approach
The approach extends relational e-matching with indexed multiset relations for AC operators, then uses modular AC congruence closure to rebuild the e-graph. The matching approach is incomplete when a pattern variable would need to bind to a subset of e-class ids.
2.1 Relational E-Matching
- Relational e-matching represents the e-graph as operator relations and rewrite patterns as conjunctive queries, using generic join to match them.The proposed novelty is a separate index structure for AC operators.Source: §2.1 · pp. 2–3
2.2 E-Graphs modulo AC
- AC operators are stored as variadic relations over multisets, so AC-equivalent terms share a multiset e-node instead of matching AC patterns as rewrites.Explicit and implicit representations allow the system to store only a fraction of the total e-nodes; trie indexing selects a multiset first with an auxiliary variable.Source: §2.2 · p. 3
- The matching approach is incomplete because pattern variables bind to e-class ids, not subsets of e-class ids.For example, it may fail to match a pattern on a flattened sum when a variable needs to bind to a+b; the significance of this loss requires further research.Source: §2.2 · p. 3
2.3 Rebuilding
- Rebuilding restores congruence closure by using modular AC congruence closure, which rebuilds each relation and propagates new equivalences through union-find.Kapur’s algorithm canonicalizes and simplifies dirty e-nodes, collects critical pairs, and produces a reduced convergent rewrite system containing only minimal e-nodes while retaining all represented terms.Source: §2.3 · pp. 3–4
3 Preliminary Results
The evaluation reports a significant e-graph size reduction for equality saturation modulo AC compared with standard equality saturation. It measures saturated graphs against egg and summarizes asymptotic scaling for selected terms.
3 Preliminary Results
- The evaluation inserts a term into an empty e-graph, saturates it, and measures the resulting size against egg.For equality saturation modulo AC, only explicitly represented e-nodes are counted because implicit e-nodes require no memory.Source: §3 · p. 4
- Table 1 summarizes asymptotic e-graph size scaling for selected terms.The supplied passages do not report the table’s individual bounds.Source: §3 · p. 4, Table 1 · p. 5
- The results demonstrate a significant reduction in e-graph size compared with standard equality saturation.Figure 1 compares egg and eqsat-mod-ac for selected terms.Source: §3 · p. 4, Figure 1 · p. 5
4 Conclusions
The paper proves exponential bounds for e-nodes and e-classes in classic equality saturation and extends relational e-matching to reduce memory for AC operators. The savings depend on the theory, and worst-case memory remains exponential.
4 Conclusions
- The analysis formally proves O(2n) bounds for both e-nodes and e-classes in classic equality saturation.These bounds quantify the effect of AC on equality saturation.Source: §4 · p. 6
- Extending relational e-matching lets the approach store terms as multisets and manage subterms implicitly, using asymptotically less memory than traditional e-graphs.Memory savings vary by theory.Source: §4 · p. 6
- The approach still requires exponential memory in the worst case, and further research is needed to understand where it breaks down and find remedies.Source: §4 · p. 6