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

The left tree describes the search process of old SEM, while the right one de-
scribes the effect of congruence closure computation on the search process. We
see that some branches of the search tree can be eliminated if we combine con-
gruence closure computation with existing reasoning methods of SEM.

4 The Extended Search Algorithm

The model generation process can be described by the recursive procedure in
Fig. 1, which searches for every possible model. It can be easily modified to
search for only one model. The procedure uses the following parameters:

- : assignments (cells and their assigned

values), where Dom ( ce ) is the domain of values for ce ;
- D

Pmod = { ( ce, e ) | e ∈ Dom ( ce ) }

= { ( ce, D ) | D ⊂ Dom ( ce ) } : unassigned cells and their possible values;

- Ψ : constraints (i.e. the clauses).

Initially Pmod is empty, and D contains ( ce, Dom ( ce )) for every cell ce .

proc search( Pmod,D,Ψ )
{

if D = ∅ then /* a model is found */
{ print( Pmod ); return; }
choose and delete ( ce i ,D i ) from D ;
if D i = then return; /* no model */

for e ∈ D i do
{

∅

( Pmod , D ,Ψ ) := propa ( Pmod∪{ ( ce i ,e ) }, D,Ψ ) ;
if Ψ is not FALSE /* no contradiction found */
then search ( Pmod , D ,Ψ ) ;

}

}

Fig. 1. The abstract search procedure

The procedure propa ( Pmod,D,Ψ ) propagates assignment Pmod in Ψ :it
simplifies Ψ and may force some variables in to be assigned. The procedure

propa ( Pmod,D,Ψ ) is essentially a closure operation (with respect to a set of
sound inference rules). It repeatedly modifies Pmod,D

D

,and Ψ until no further
changes can be made. When it exits, it returns the modified triple ( Pmod,D,Ψ ).
The basic steps of this procedure can be described as follows.

(1) For each new assignment ( ce, e )in Pmod , replace the occurrence of ce in Ψ
by e .
(2) If there exists an empty clause in Ψ (i.e., each of its literals becomes FALSE
during the propagation), replace Ψ by FALSE , and exit from the procedure.
Otherwise, for every unit clause in Ψ (i.e. all but one of its literals become
FALSE ), examine the remaining literal l .