# Congruence Closure Algorithm and Correctness

## Congruences on all Ground Terms

Let be a set of ground equalities and disequalities representing the formula

Then the following are equivalent:

- is satisfiable
- there exists a congruence on ground terms in which is true
- is true in the least congruence containing

## Congruences on Ground Terms Occurring in the Formula

Instead of a congruence on the (typically infinite) set of all ground terms, we compute congruences on the set of the ground terms ocurring in .

Note that and that applying reflexivity, symmetry, transitivity keeps the relation in .

We need modify congruence condition to apply only to terms in , using the following congruence condition:

Algorith:

- start with
- apply the congruence rule above as well as reflexivity, symmetry and transitivity until the fixpoint
- denote result by .

**Theorem:** conjunction of formulas in is satisfiable iff for each we have .

**Proof:**

- for each pair we have that is a semantic consequence of
- we use to construct a structure in which holds
- take as domain the equivalence classes of ; let denote the equivalence class of
- define as if , and arbitrary otherwise

## Implementing Congruence Closure

Congruence is an equivalence relation, so the algorithm is a special case of union-find algorithms for finding partitions.

We represent expressions as directed acyclic graphs, which are syntax trees for expressions, with sharing. This data structure is called **E-graph**.

Within this structure we have union of inverted trees, representing union-find data structure.

Inverted tree representing equivalence classes.

**Example:** Let denote with -fold application of . Consider

Apply the congruence closure algorithm to check its satisfiability.