Congruence closure

Congruence closure computes all equalities between terms that follow from a given set of equations, under the rules of equality and the congruence rule: if $s_1=t_1,\dots ,s_n=t_n$, then $f(s_1,\dots ,s_n)=f(t_1,\dots ,t_n)$ for every function symbol $f$^[1][2]. The function symbols are uninterpreted: nothing is known about them except that they are functions. Given ground equations and disequations, the algorithm partitions the subterms into equivalence classes, merging classes for each equation and then merging any applications whose argument classes coincide, until nothing changes; the input is satisfiable exactly when no disequation relates two terms of the same class. This decides the quantifier-free theory of equality with uninterpreted functions (EUF), one of the basic theories of SMT solvers, where congruence closure serves as the theory solver^[4]. Nelson and Oppen, and Downey, Sethi and Tarjan, published efficient algorithms in 1980^[1][2].

Equality with uninterpreted functions is axiomatized by reflexivity, symmetry, transitivity and congruence:

A conjunction of equations and disequations between ground terms is satisfiable if and only if no disequation $s\ne t$ has $s=t$ derivable from the equations by these rules. Ackermann showed in 1954 that the problem is decidable^[6], and Kozen that it is decidable in polynomial time^[5]. Uninterpreted functions are useful as abstractions: replacing an operation that is hard to reason about, such as multiplication or a hash function, by an uninterpreted symbol keeps only the fact that equal inputs give equal outputs, which is often all a proof needs.

Represent the subterms of the input as the nodes of a directed acyclic graph, sharing identical subterms. Keep the nodes in a union–find structure, and for each class the list of applications that use one of its members as an argument. To merge two classes, link their representatives and recompute the signature of each application that used the smaller class, the function symbol together with the representatives of its arguments. If another application already has the same signature, the two are congruent and are merged in turn^[2].

(* Congruence closure with use lists, in the style of Downey, Sethi and
   Tarjan. Terms are nodes of a DAG: constants, or a function symbol
   applied to argument nodes. *)
type node = { id : int; sym : string; args : int list }
 
type t = {
  nodes : node array;
  parent : int array;                    (* union–find *)
  uses : int list array;                 (* applications using a class as an argument *)
  sigs : (string * int list, int) Hashtbl.t;   (* signature -> a node with it *)
}
 
let trace = ref false
 
let rec find cc i = if cc.parent.(i) = i then i else (let r = find cc cc.parent.(i) in cc.parent.(i) <- r; r)
let signature cc n = (n.sym, List.map (find cc) n.args)
 
let make (nodes : node array) =
  let n = Array.length nodes in
  let cc = { nodes; parent = Array.init n Fun.id; uses = Array.make n [];
             sigs = Hashtbl.create 64 } in
  Array.iter (fun nd -> List.iter (fun a -> cc.uses.(a) <- nd.id :: cc.uses.(a)) nd.args) nodes;
  cc
 
let rec show cc i =
  let nd = cc.nodes.(i) in
  if nd.args = [] then nd.sym else nd.sym ^ "(" ^ String.concat "," (List.map (show cc) nd.args) ^ ")"
 
(* Merge the classes of a and b. The applications that used the smaller
   class get new signatures; any that now collide with another
   application are congruent, and are merged in turn. *)
let rec merge cc a b why =
  let ra = find cc a and rb = find cc b in
  if ra <> rb then begin
    if !trace then Printf.printf "  merge %s = %s   (%s)\n" (show cc a) (show cc b) why;
    let ra, rb = if List.length cc.uses.(ra) <= List.length cc.uses.(rb) then (ra, rb) else (rb, ra) in
    let moved = cc.uses.(ra) in
    cc.parent.(ra) <- rb;
    cc.uses.(rb) <- moved @ cc.uses.(rb);
    List.iter (fun u ->
        let s = signature cc cc.nodes.(u) in
        match Hashtbl.find_opt cc.sigs s with
        | Some v when find cc v <> find cc u -> merge cc u v "congruence"
        | Some _ -> ()
        | None -> Hashtbl.replace cc.sigs s u) moved
  end
 
(* Build the structure; applications that have equal signatures from
   the start are congruent and are merged at once. *)
let create nodes =
  let cc = make nodes in
  Array.iter (fun nd ->
      if nd.args <> [] then
        match Hashtbl.find_opt cc.sigs (signature cc nd) with
        | Some v when find cc v <> find cc nd.id -> merge cc v nd.id "congruence"
        | Some _ -> ()
        | None -> Hashtbl.replace cc.sigs (signature cc nd) nd.id) nodes;
  cc

Merging the smaller use list into the larger means that each application is re-signed $O(\log n)$ times, so the whole closure takes $O(n\log n)$ time with a hash table for signatures, for a graph with $n$ edges^[2].

From $f^3(a)=a$ and $f^5(a)=a$ it follows that $f(a)=a$. By congruence, $f^3(a)=a$ gives $f^4(a)=f(a)$ and $f^5(a)=f^2(a)$; with $f^5(a)=a$ this makes $f^2(a)=a$, and then $f^3(a)=f(a)$, so $f(a)=f^3(a)=a$.

open Cc
 
(* a, f(a), f(f(a)), ..., f^5(a) as nodes 0 .. 5 *)
let chain = Array.init 6 (fun i -> if i = 0 then { id = 0; sym = "a"; args = [] }
                            else { id = i; sym = "f"; args = [ i - 1 ] })

assert f(f(f(a))) = a
  merge f(f(f(a))) = a   (given)
  merge f(f(f(f(a)))) = f(a)   (congruence)
  merge f(f(f(f(f(a))))) = f(f(a))   (congruence)
assert f(f(f(f(f(a))))) = a
  merge f(f(f(f(f(a))))) = a   (given)
  merge f(f(f(a))) = f(a)   (congruence)
f(a) = a? true
classes: 1

(* Random term DAGs over a, b, f and g, and random equations: does the
   use-list algorithm agree with naive repeated closure? *)
let rec to_term (nodes : Cc.node array) i =
  let n = nodes.(i) in
  if n.args = [] then Euf.Const n.sym else Euf.App (n.sym, List.map (to_term nodes) n.args)

500 random problems, 500 agree on all 72000 pairs of terms

As a theory solver, congruence closure must be incremental, adding equations one at a time as the SAT solver asserts them; backtrackable, undoing merges when the SAT solver backtracks; and able to explain its conclusions. When a disequation $s\ne t$ is contradicted, the solver must name a small set of input equations from which $s=t$ follows, which becomes the learned clause. Nieuwenhuis and Oliveras showed how to record, for each merge, the equation or congruence that caused it, and to extract explanations in time proportional to their size^[4]. The Simplify prover, the basis of many program verifiers, was built around an e-graph of this kind^[11].

An alternative is to remove the functions altogether. Ackermann's reduction replaces each application by a fresh variable and adds, for each pair of applications of the same function, the constraint that equal arguments imply equal results. The result is a formula in the theory of equality alone, at the cost of a quadratic number of constraints^[6][10].

The congruence-closure data structure, a set of term nodes grouped into classes and kept closed under congruence, is called an e-graph. Compilers use it for global value numbering, to find expressions that are guaranteed to compute the same value^[7]. Equality saturation applies rewrite rules to an e-graph without discarding the original terms, so that all equivalent forms of a program are represented at once, and then extracts the best one^[8]. The egg library made the technique practical for program optimizers and synthesis tools^[9].

Ackermann decided the ground case of equality with functions in 1954^[6], and Kozen gave a polynomial algorithm in 1977^[5]. Shostak described an equality procedure for program verification in 1978^[3]. In 1980 Nelson and Oppen presented congruence closure as the decision procedure for EUF, as part of their method for combining decision procedures^[1], and Downey, Sethi and Tarjan gave the $O(n\log n)$ algorithm in the context of common subexpressions^[2]. Proof-producing congruence closure for SMT followed in 2007^[4], and the e-graph returned to compilers with equality saturation in 2009^[8][9].

• Theory solverIn an SMT solver, a theory solver decides whether a conjunction of literals of one theory, such as linear arithmetic or equality with uninterpreted functions, is consistent. The SAT search asserts literals to it incrementally and asks it to check them; on inconsistency it returns an explanation, a small subset of the asserted literals that is already inconsistent, which the SAT search learns as a clause. A theory solver must also undo assertions when the search backtracks, and it may propagate literals that the asserted ones imply. The quality of explanations and propagation largely determines the solver's performance.
• SMTSatisfiability modulo theories (SMT) is the problem of deciding whether a first-order formula is satisfiable when some of its symbols are interpreted by background theories, such as integer or real arithmetic, bit-vectors, arrays and uninterpreted functions. SMT solvers such as Z3 and cvc5 combine a SAT solver, which handles the Boolean structure, with specialized decision procedures for the theories, usually in the DPLL(T) architecture. They read the standard SMT-LIB language and are the reasoning engines of program verifiers, symbolic execution tools, test generators and many other analysis tools.
• Nelson–Oppen combinationThe Nelson–Oppen method decides satisfiability of quantifier-free formulas that mix several theories with disjoint signatures, such as linear arithmetic and uninterpreted functions, using only a decision procedure for each theory. The formula is first purified, by naming mixed subterms with fresh variables, so that every literal belongs to one theory; the theory solvers then agree on which of their shared variables are equal, either by propagating the equalities each entails (enough for convex theories) or by searching over all arrangements of the shared variables. It is complete for theories that are stably infinite, and it is how SMT solvers combine their theory solvers.
• DPLL(T)DPLL(T) is the architecture of lazy SMT solvers: a CDCL SAT solver searches over the Boolean structure of a formula, treating each theory atom as a propositional variable, and a theory solver for T checks the consistency of the atoms it assigns. When the theory solver finds the assigned literals inconsistent, it returns an explanation, whose negation the SAT solver learns as a clause before backjumping; it may also propagate literals the assignment implies. The approach separates a generic engine from pluggable theory solvers and is used by nearly all SMT solvers, including Z3, cvc5 and Yices.
• Union–findUnion–find, or a disjoint-set forest, maintains a partition of a set into disjoint classes under two operations: union merges two classes, and find returns a representative of an element's class. Each class is a tree of parent pointers whose root is the representative. With union by rank and path compression, any sequence of m operations on n elements takes O(m α(n)) time, where α is the inverse Ackermann function, which is at most 4 for any practical n.

• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.

1. [1]G. Nelson, D. C. Oppen, “Fast decision procedures based on congruence closure”, Journal of the ACM 27 (1980).
2. [2]P. J. Downey, R. Sethi, R. E. Tarjan, “Variations on the common subexpression problem”, Journal of the ACM 27 (1980).
3. [3]R. E. Shostak, “An algorithm for reasoning about equality”, Communications of the ACM 21 (1978).
4. [4]R. Nieuwenhuis, A. Oliveras, “Fast congruence closure and extensions”, Information and Computation 205 (2007).
5. [5]D. Kozen, “Complexity of finitely presented algebras”, STOC (1977).
6. [6]W. Ackermann, Solvable Cases of the Decision Problem, North-Holland (1954).
7. [7]B. Alpern, M. N. Wegman, F. K. Zadeck, “Detecting equality of variables in programs”, POPL (1988).
8. [8]R. Tate, M. Stepp, Z. Tatlock, S. Lerner, “Equality saturation: a new approach to optimization”, POPL (2009).
9. [9]M. Willsey, C. Nandi, Y. R. Wang, O. Flatt, Z. Tatlock, P. Panchekha, “egg: fast and extensible equality saturation”, POPL (2021).
10. [10]D. Kroening, O. Strichman, Decision Procedures: An Algorithmic Point of View, ch. 4, Springer (2nd ed., 2016).
11. [11]D. Detlefs, G. Nelson, J. B. Saxe, “Simplify: a theorem prover for program checking”, Journal of the ACM 52 (2005).

last updated 28 September 2026