Parallelizing Congruence Closure

Abstract

Given a set of ground equalities over terms with uninterpreted function symbols, congruence closure computes the smallest equivalence relation containing these equalities that respects functional congruence. While congruence closure is a performance-critical component of SAT solvers, satisfiability modulo theories (SMT) solvers, and equality saturation engines, all existing implementations are sequential. In this work, we provide the first parallel algorithms for congruence closure. We build on two ideas from the parallel algorithms literature: a union-find data structure that supports concurrent union operations and a semisort (group-by) algorithm that allows us to discover new congruences in parallel. We present two algorithms that replace the classic sequential worklist with a bulk-synchronous closure loop: each round processes all pending unions in parallel, detects new congruences, and repeats until a fixpoint. The two algorithms differ in how they identify which terms to re-examine in each round. We evaluate both these algorithms against a sequential baseline on a number of benchmarks and show near-linear speedup on up to 32 cores.