Awesome E-Graphs

A curated list of resources related to e-graphs, equality saturation, and their applications. Contributions are welcome! Thanks to Yihong Zhang for the initial list.

Table of Contents

• Awesome E-Graphs
  • Table of Contents
  • Community
  • Implementations
  • General
  • Applications
    • Hardware
    • Program Synthesis
    • Program Optimization
    • Theorem Proving and Verification
    • Other
  • Extraction
  • Scheduling
  • EGRAPHS Workshop
    • EGRAPHS 2024
    • EGRAPHS 2023
    • EGRAPHS 2022
  • Blog Posts

Community

• egraphs.org
• zulip
• Community Meetings
• PLDI EGRAPHS Workshop

Implementations

• egg
• egglog
• egglog-python
• snake-egg
• Metatheory.jl Julia Library
• hegg Haskell library
• ego OCaml library
• quiche
• egraphs.cpp
• eqsat
• eggmt
• ekege
• Eqlog
• GATlab
• marktoberdorf-egglog
• egraph-sqlite
• egglog-speedrun

General

• Fast Decision Procedures Based on Congruence Closure
• Proof-Producing Congruence Closure
• Efficient E-matching for SMT Solvers
• The Chase Revisited
• egg Fast and Extensible Equality Saturation
• egglog Better Together: Unifying Datalog and Equality Saturation
• Small Proofs from Congruence Closure
• Colored E-Graphs arxiv
• Slotted E-Graphs
• E-Graphs, VSAs, and Tree Automata: a Rosetta Stone
• An Evaluation Algorithm for Datalog with Equality
• Algebraic Semantics of Datalog with Equality

Applications

A reverse search on the egg paper on Google Scholar is a good way to stay up to date

Hardware

• ROVER: Combining Power and Arithmetic Optimization via Datapath Rewriting. ARITH 2024.

• Infinity Stream: Portable and Programmer-Friendly In-/Near-Memory Fusion. ASPLOS 2023.

• Lakeroad FPGA Technology Mapping Using Sketch-Guided Program Synthesis repo

• Multiplier Optimization via E-Graph Rewriting

• SEER Super-Optimization Explorer for High-Level Synthesis using E-graph Rewriting

• ESFO Equality Saturation for FIRRTL Optimization

• There and Back Again A Netlist's Tale with Much Egraphin'

• E-Syn Eqsat framework for technology-aware logic synthesis

Program Synthesis

• Ruler: Rewrite Rule Inference Using Equality Saturation. OOPSLA 2021. Distinguished paper.

• CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. ICFP 2024.

• enumo: Equality Saturation Theory Exploration à la Carte. OOPSLA 2023.

• babble: Learning Better Abstractions with E-Graphs and Anti-unification. POPL 2023.

• MegaLibm: Implementation and Synthesis of Math Library Functions. POPL 2024. Distinguished paper.

• Isaria: Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. ASPLOS 2024. Best paper.

Program Optimization

• Herbie: Automatically Improving Accuracy for Floating Point Expressions.
  PLDI 2015. Distinguished paper.

• Felix: Optimizing Tensor Programs with Gradient Descent. ASPLOS 2024.

• aegraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler https://vimeo.com/843540328

• Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs

• peggy Equality Saturation: A New Approach to Optimization

• optir RVSDG optimizing intermediate representation

• eggcc

• Denali A practical algorithm for generating optimal code

• Glenside Pure Tensor Program Rewriting via Access Patterns

• Simplifying MBA Expression Using E-Graphs

• SPORES sum-product optimization via relational equality saturation for large scale linear algebra

• ∇SD: A Tensor Algebra Compiler for Sparse Differentiation. CGO 2024.

• TenSat: Equality Saturation for Tensor Graph Superoptimization. MLSys 2021.

• PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting. OOPSLA 2024.

• RisingLight: Write a SQL Optimizer using Egg. EGRAPHS 2023.

• Hydro: Optimizing Stateful Dataflow with Local Rewrites. EGRAPHS 2023.

• SpEQ: Translation of Sparse Codes using Equivalences

• ACC Saturator : Automatic Kernel Optimization for Directive-Based GPU Code

• High-performance symbolic-numerics via multiple dispatch

• Q-gym: An Equality Saturation Framework for DNN Inference Exploiting Weight Repetition

• Diospyros: Vectorization for Digital Signal Processors via Equality Saturation. ASPLOS 2021.

• Chassis : Target-Aware Implementation of Real Expressions

• Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search

• Latent Idiom Recognition for a Minimalist Functional Array Language Using Equality Saturation

Theorem Proving and Verification

• Most SMT solvers have an e-matching egraph implementation in them
• lean-egg: An Equality Saturation Tactic for Lean. Thesis 2023. (repo)
• KestRel: Relational Verification Using E-Graphs for Program Alignment. EGRAPHS 2023.
• cyclegg
• coq congruence
• Fast Approximations of Quantifier Elimination
• Congruence Closure in Intensional Type Theory
• Congruence Closure in Cubical Type Theory
• ZOMBIE: Programming up to Congruence
• GATlab: Modeling and Programming with Generalized Algebraic Theories
• Transforming Optimization Problems into Disciplined Convex Programming Form
• Coquetier a simplification tactic for our Coq toolbox

Other

• YOGO Semantic Code Search via Equational Reasoning

• VyZX: Formal Verification of a Graphical Quantum Language with automated structural rewrites.
  Thesis 2023.

• Szalinski: Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations.
  PLDI 2020.

• Maletskyi and Shymanskyi: Genome Compression Using Program Synthesis.
  IDDM 2023.

• Cornelius: Equivalent and redundant mutant detection with e-graphs!!!

• MetaEmu: An Architecture Agnostic Rehosting Framework for Automotive Firmware.
  CCS 2022.

• wasm-evasion: WebAssembly diversification for malware evasion.
  COSE 2023.

• Guided Equality Saturation: Improve performance/capabilities by using guides in a semi-automatic equality saturation process. POPL 2024.

• Novel Algorithms for Computing Correlation Functions of Nuclei

Extraction

• extraction-gym
• E-Graphs as Circuits, and Optimal Extraction via Treewidth
• Notes on the scheduling and extraction problems of EqSat
• Answer Set Programming for E-Graph DAG extraction
• Fast and Optimal Extraction for Sparse Equality Graphs

Scheduling

• Learned Graph Rewriting with Equality Saturation: A New Paradigm in Relational Query Rewrite and Beyond

Talks

• egg: Fast and Extensible Equality Saturation
• Better Together: Unifying Datalog and Equality Saturation (PLDI 2023)
• egglog Tutorial (EGRAPHS 2023) | Next Generation Egraphs
• egglog: E-Graphs in Python
• ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler
• E-Graphs and Automated Reasoning: Looking Back to Look Forward

EGRAPHS Workshop

EGRAPHS 2024

Accepted Papers

youtube

EGRAPHS 2023

Presentations

EGRAPHS 2022

Accepted papers

youtube

Blog Posts

• The e-graph data structure: A gradual introduction
• The Theoretical Aspect of Equality Saturation
• Acyclic Egraphs and Smart Constructors
• Gauss and Groebner Egraphs: Intrinsic Linear and Polynomial Equations
• What's in an e-graph?
• Improving MBA Deobfuscation using Equality Saturation
• Automating Transport with Univalent E-Graphs
• Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
• Binding in E-graphs