Fast Decision Procedures Based on Congruence Closure

TLDR

The paper defines the congruence closure of a relation on a graph and surveys algorithms for computing it. The authors present a decision procedure for the quantifier‑free theory of LISP list structure that builds on the congruence closure algorithm. The congruence closure algorithm yields a decision procedure for the quantifier‑free theory of equality, and the LISP list theory procedure solves satisfiability in average O(n log n) time, but a slight change to the list axioms makes the problem NP‑complete, and both procedures are implemented in the Stanford Pascal Verifier.

Abstract

The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length n in average time O ( n log n ) using the fastest known congruence closure algorithm. It is also shown that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier.