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

Table 1. Performance comparison

Problem Size Satisfiable SEM SEMc

Round Time Round Time

BN1 4 No 888 0.00 502 0.22

BN1 5 Yes 34 0.00 26 0.02

g1x 4 Yes 11803 0.05 675 0.11

BOO033-1 5 Yes 29 0.00 27 0.05

LCL137-1 6 Yes 609 0.01 569 0.03

LCL137-1 8 Yes 5662 0.09 5466 0.15

ROB012-1 3 No 983694 2.55 982652 2.69

ROB015-1 3 No 1004638 2.25 1001420 2.35

f(z,f(g(f(y,z)),f(g(f(y,g(f(y,x)))),y))) = x
f(0,g(0)) != f(1,g(1))

The existence of a model implies that the first equation is not a single axiom for
group theory. The other problems are from TPTP [12].
For some problems, there are non-unit clauses as well as negated equations.
Thus the use of congruence computation does not make much difference. For
problems like g1x where complex equations dominate in the input, the new
version of SEM can reduce the number of branches greatly (by 17 times).
In the above experiments, Lvl is set to 10 (an arbitrary value). Without the
restriction, the overhead of computing congruence closure might be significant.

6 Concluding Remarks

Many factors can affect the eciency of a backtrack procedure. In the context of
finite model searching, these include the heuristics for choosing the next cell and
the inference rules for deducing new information from existing assignments. In
this paper, we have demonstrated that adding congruence computation as a new
inference rule can reduce the number of branches of the search tree, especially
when most clauses are complex equations.
The current implementation is not so ecient because we have implemented
only the original Nelson-Oppen algorithm [8] for computing congruences. With
more ecient data structures and algorithms (e.g. [9]), we expect that the run-
ning time of SEMc can be reduced. Another way of improvement is that the
congruence should be computed incrementally. In the current version of SEMc,
each time the congruence is computed, the algorithm starts from all ground in-
stances of the input equations. However, during the search, many of them can
be neglected (when both the left-hand side and the right-hand side are reduced
to the same value).

Acknowledgements

We are grateful to the anonymous reviewers for their detailed comments and
suggestions.