Equality saturation allows to optimize programs by growing an e-graph using rewrite rules, efficiently exploring many equivalent programs. Unfortunately, some optimizations remain out of reach: the e-graph grows too big as they require long rewrite sequences and explosive combinations of rewrite rules (e.g. associativity and commutativity).

In this talk, we propose sketch-guided equality saturation to factor unfeasible equality saturations into a sequence of simpler, feasible equality saturations. The programmer guides rewriting by providing a sequence of sketches, describing how the program should evolve during optimization.

Sketch-guided equality saturation is evaluated by performing seven realistic optimizations of matrix multiplication expressed in a functional array language called Rise. Unguided equality saturation cannot discover the five most complex optimizations, even with an hour of compilation time and 60GB of RAM. By specifying three or fewer sketch guides, all seven optimizations are found in seconds of compilation time, using under 1GB of RAM, and generating high performance code.