# Better Together: Unifying Datalog and Equality Saturation

arXiv: https://arxiv.org/abs/2304.04332 · HTML: https://mlsanity.com/paper/2304.04332/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Apr 2023.

## Built on by (most cited first, 4 of 4)

- [e-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving](https://mlsanity.com/paper/2508.13020/) (2025)
- [SkyEgg: Heterogeneity-Aware Hardware Synthesis via Equality Saturation](https://mlsanity.com/paper/2511.15323/) (2025)
- [Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks](https://mlsanity.com/paper/2509.10694/) (2025)
- [Meganeura: Portable GPU Training and Inference through Vulkan and Metal](https://mlsanity.com/paper/2608.01563/) (2026)

## Abstract (arXiv)

We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, it supports term rewriting, efficient congruence closure, and extraction of optimized terms. We identify two recent applications--a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter--that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate egglog by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.