Extending Finite Model Searching with Congruence Closure Computation - Artificial Intelligence and Symbolic Computation - page 96

In this paper, we will solve the finite model generation problem using back-
track search. The basic idea of such a search procedure is roughly like the fol-
lowing: repeatedly extend a partial model (denoted by Pmod ) until it becomes
a complete model (in which every cell gets a value). Initially Pmod is empty.
Pmod is extended by selecting an unassigned cell and trying to find a value for
it (from its domain). When no value is appropriate for the cell, backtracking is
needed and Pmod becomes smaller.
The execution of the search procedure can be represented as a search tree.
Each node of the tree corresponds to a partial model, and each edge corresponds
to assigning a value to some cell by the heuristic. We define the level of a node
as usual, i.e., the level of the root is 0 and the level of the children of a level n
node is n +1.

3 Congruence Closure for Constraint Propagation

The eciency of the search procedure depends on many factors. One factor
is how we can perform reasoning to obtain useful information when a certain
number of cells are assigned values. That is, we have to address the following
issue: how can we implement constraint propagation and consistency checking
eciently?
This issue may be trivial for some constraint satisfaction algorithms because
the constraints they accept are often assumed to be unary or binary. It is true
that n -ary constraints can be converted into an equivalent set of binary con-
straints; but this conversion usually entails the introduction of new variables
and constraints, and hence an increase in problem size. This issue is particu-
larly important to model generation because in this case, the constraints are
represented by complicated formulas. Experience tells us that a careful imple-
mentation can improve the performance of a program significantly.
In [15], a number of inference rules are described in detail. They are quite
effective on many problems. In this paper, we discuss another inference rule,
namely congruence closure , which can be quite useful for equational problems.

3.1 Congruence Closure

An equivalence relation is a reflexive, symmetric and transitive binary relation.
Arelation ∼ on the terms is monotonic if f ( s 1 ,...,s n ) ∼ f ( t 1 ,...,t n ) whenever

f ≤ i ≤ n ), s i ∼ t i .A congruence

relation is a monotonic equivalence relation. A set of ground equations, E , defines
a relation among the ground terms. The congruence generated by E , denoted by
E ∗ , is the smallest congruence relation containing E .
There are several algorithms for computing the congruence generated by a
set of ground equations, called congruence closure algorithms, e.g., [1, 8]. The
Nelson-Oppen algorithm [8] represents terms by vertices in a directed graph. It
uses UNION and FIND to operate on the partition of the vertices, to obtain the
congruence relation.

is an n -ary function symbol and for every i (1