Exploring Exponentially Many Programs at Once with E-Graphs

Adam Chlipala

Nov 10, 2026

6

3

Share

The last sequence of articles has been making the case for automated programming via gradually deriving implementations from specifications, in a way that enforces correctness by construction thanks to formal verification. I have given examples with tensor algebra in software, digital hardware, and low-level cryptographic software.

The last example was presented as applying a limited version of a classic technique from automated theorem proving. This article presents more of that technique, setting up for the next post, on a new application in a challenging domain (compiler correctness).

One of the most important kinds of automated theorem prover today is satisfiability-modulo-theories (SMT) solvers, which underlie a variety of program-verification tools. A core data structure in their implementations is e-graphs, which were developed for this purpose in the late 1970s by Nelson and Oppen.

E-graphs were originally used to answer a very fundamental kind of query for theorem proving: given a set of logical facts that we know, does another fact follow as a consequence? Specifically, we are concerned with equalities between algebraic terms. This usage mode in a reduced version of e-graphs was central to our earlier example of program equivalence checking in CryptOpt.

However, a more recent usage of e-graphs is for automatic optimization of programs, dubbed equality saturation. Namely, one uses an e-graph to derive many alternative programs that are provably equal to the original. Then the most efficient alternative is returned to the programmer. It was not obvious up front (before this work or its predecessor by a few years Denali) that the same technology could be used in automated theorem proving and program optimization, but the connection has turned out to be a robust one. It’s even very natural for program optimization to create subproblems that involve straight-up automated theorem proving, say to prove side conditions of rewrite rules.

That outline is easier said than done! In general, there could be many different alternative programs, and every program could be quite large, so we should worry about running out of memory to store them all, let alone efficiently computing the full set of alternatives. Let’s consider other approaches to the same problem.

We can just ask an AI agent to mirror a programmer’s thought process, exploring different program variants and benchmarking them to help zero in on the fastest one. Since deep learning is fundamentally slow (high-latency), we will need to have subagents exploring many variants at once, if we hope for a quick overall answer. We also have no rigorous rhyme or reason behind the generation of different variants. Even if we rely on formal verification to validate variants, it is still hard to be systematic about generating variants and representing giant spaces of variants efficiently.

Alternatively, we can adopt a naive version of correct-by-construction derivation, the subject of this sequence of articles. We can loop repeatedly using a heuristic to select a proved rewrite rule and where to apply it within the current program. The trouble is that most sets of rewrite rules are not confluent, a technical term meaning that all orders of rewrites can get us to the same final results. Instead, early heuristic choices can trap us in local optima.

A classic solution to such a problem is backtracking search: sometimes we give up on a particular sequence of rewrites, rewinding our search to a state before some of the rewrites, so we can try different choices. In theory, this approach could enumerate all rewrite sequences up to some length bound, keeping the one with the best outcome, though the number of possible sequences grows so quickly with sequence length that this method is impractical in practice. Instead, we need some kind of search heuristic, which could pay off in limited circumstances.

However, what if instead we used data structures and algorithms from the 1970s to compute the set of reachable program variants quickly and represent that set compactly, with lots of sharing, still with strong mathematical guarantees about correctness of all variants?

Naturally, we’ll now survey how choice #4 works, using e-graphs. The key benefit we will see is avoiding premature commitment to optimization choices. That is, conventional methods will usually decide at some point in search whether a given optimization is worth applying. E-graphs instead note the possibility of the optimization and allow continued exploration to consider both variants of the program. These choices stack on top of each other, so that search can consider exponentially many variants, without the running time or memory usage we would expect in interpreting that characterization naively. This style of search can still quickly exhaust resource limits, but often a lot more can be accomplished within a given budget of time or memory.

I’m going to keep it to a basic algebra example in this article, and we’ll turn to a larger-scale domain of examples next time. Imagine that we want to find an efficient way to compute the value of (a + b)c + (b + a)d, where these variable values are not known until runtime. We will throw this expression into an e-graph and let it find the lowest-cost variant.

The problem starts out represented with syntax trees where the semantic equality between a + b and b + a is not clear.

We internalize the syntax tree of our starting expression into an e-graph, a graph in the computer-science sense of “a diagram of nodes and edges.” Each node is labeled with either a variable name (each variable gets a unique node) or an operator plus child pointers (edges) to operands.

For the moment, assume some unspecified procedure realizes a + b = b + a and asks to merge the nodes for these two expressions (E4 and E5). Both operations are retained inside the combined node, which now represents a nondegenerate e-class: a set of equivalent ways (called “e-nodes”) to express the same semantic value, stored with carefully preserved sharing, so the e-graphs don’t grow too large.

We don’t just stop with merging these two nodes. A follow-up phase is congruence closure, where we merge additional nodes whose equalities are now implied by what we learned. Specifically, if we know x = y, then we also know f(x) = f(y) for any function f. This congruence rule holds more generally for functions of multiple arguments.

Here is a diagram of how congruence closure proceeds for a slight variant of our running example. To make things more interesting, imagine the original problem had used c where d appeared. In the following diagram, dashed edges represent parent edges that are present in the actual data structure, so that, when a node is implicated in a new equality, we can instantly find all larger expressions that mention that node and consider which now have new implied equalities. Here, after E4 and E5 merge, we can follow their parent edges to find E6 and E9, which we then confirm also deserve to merge.

Note that E6 contains a single multiplication operation, while E4 contains two additions. The reason is that there is now a single way to express E6 as a multiplication of other nodes, while there are two genuinely different ways to express E4 as an addition of other nodes. These alternatives embody my promise above that e-graphs help us avoid premature commitment to optimizations, since we store away two alternative ways to express the same value, and later we can choose the right one that enables some other optimization. Now let us return to the original running example.

Let’s now demystify how we can identify opportunities like a + b = b + a. Clearly a rewrite rule for commutativity of addition covers this case, but how do we efficiently find all the opportunities to apply a rewrite rule within an e-graph? Here we reveal yet another part of the data structure: an operator index that maps each available operator to all nodes that mention that operator, to characterize alternative ways to compute those nodes’ values.

Now say we want to find all opportunities to use the commutativity rewrite rule. We use the operator index for “+” to identify all additions, and we find all that don’t already have their swapped-order variants equated with the originals. We add the swapped versions that are missing into the e-classes of the originals, and, in cases where both orders already appeared in the e-graph, we merge their nodes. Here is an illustration using a distributivity rule, which is the other rewrite needed to optimize our running example to minimize operator count.

The general pattern is that auxiliary index structures within the e-graph support zeroing in quickly on places where a rewrite rule might match. Such a search can be much faster than walking the whole e-graph to find matches, though in general, more optimizations than I cover here are called for. Each time we apply rewrites to merge nodes, we trigger fix-up passes that use congruence closure to propagate consequences to merge more nodes. Then we can do more rounds of searching for applicable rewrites, in a virtuous cycle.

An important final stage is extracting the most desirable variant of our initial program. E-graphs support efficient extraction of this kind, using a variant of dynamic programming. Assume we have some simple cost function over expression trees; for this example, we’ll just use number of operators in a tree. For a graph with straightforward tree structure, we traverse it from leaves to the root, computing for each node its optimal cost, along with some expression that realizes that cost. On visiting each node, we look through the different expressions labeled on it, each an operator plus pointers to operands, and consider the optimal-cost extractions of each pair of operands, plus the cost of the associated operator. We simply pick the alternative that gives the lowest cost, using the extracted versions of the child operands to build the extracted version of the parent. (This whole process is importantly more complicated in graphs with cycles, which can arise given algebraic rules like x + 0 = x, implying e + 0 + 0 + 0 + … = e, represented finitely in an e-graph using a cycle.)

Here we found a program variant that uses three arithmetic operations instead of five.

What’s important to keep in mind about this process is that it is associated with very strong correctness guarantees. If all rewrite rules are proved correct, then all equalities learned through execution are guaranteed to hold, and thus extraction is guaranteed to produce a program variant that equals the original. The e-graph data structure can also represent gigantic sets of alternative programs very efficiently. It is not hard to see that an e-graph with n nodes can easily represent two-to-the-n alternatives for the original program, if each node is associated with two alternative expressions. The kinds of coding-agent searches for good code that are popular today can’t scale nearly that well to considering many alternatives – and they certainly don’t provide mathematical guarantees of code correctness. I should acknowledge a tradeoff, though, of coding agents effectively using more expensive but also more accurate cost models to evaluate program-variant performance, on many fewer variants considered.

The bottom line is that e-graphs pay off in making it possible to explore a space of program variants without precommitting to sequences of optimization choices, instead representing many of them compactly.

Coming Up

There remain puzzles around the fine points of data structures and algorithms here, with a popular line of implementation work being on the egg and egglog tools. I’ll have a bit to say about that implementation strategy in my next article, but it will focus more on an application of these ideas. Compilers, which translate between programming languages, are