Information Technology Reference

In-Depth Information

(3) Choose the cell
a(0,1)
and assign the value 1 to it. After the first two choices,

SEM deduces that
a(0,1)
cannot be
0
.Otherwise,suppose
a(0,1) = 0
.Let

x=1
and
y=z=0
in the formula (BN1-1), we have
a(a(a(0,1),0),0)

= a(1,a(0,0))
, which is simplified to
0 = a(1,0)
.Thenlet
y=0
in the

formula (BN1-3), we shall have
0

=
0
.

(4) Choose the cell
a(1,1)
and assign the value 2 to it.

After the first three steps, SEM will also deduce that
a(1,1)

=
1
.

The Effect of Congruence Closure Computation.
If we apply the con-

gruence closure algorithm to the ground instances of the formulas (BN1-1) and

(BN1-2) and the first three assignments

a(0,0) = 0; f(0) = 1; a(0,1) = 1; (P1)

we shall get the conclusion
a(1,1) = 1
. This contradicts with the inequality

a(1,1)

=
1
which is deduced by SEM. Thus if we extend SEM's reasoning

mechanism with the congruence closure algorithm, we know that, at step 3,

assigning the value 1 to the cell
a(0,1)
will lead to a dead end.

Now suppose we try
a(0,1) = 2
next. For this new branch, we add the

following three equations to
Ψ
:

a(0,0) = 0; f(0) = 1; a(0,1) = 2. (P2)

After computing the congruence closure, we can get these equations:

a(0,0) = a(1,0) = a(2,0) = 0;

f(0) = 1;

a(0,1) = a(0,2) = a(1,2) = a(2,2) = 2.

However, with the old version of SEM, after the three assignments (P2), we

only deduce
a(0,2) = 2
as a new cell assignment. In other words, the partial

model consists of these four assignments:

a(0,0) = 0; f(0) = 1; a(0,1) = 2; a(0,2) = 2.

SEM can also deduce some negative assignments, e.g.,
a(1,2)

=
2
.Thiscon-

tradicts with what we get from the closure computation algorithm. Thus, we

have come to a dead end again. We don't need to go further and expand the

search tree (as the old version of SEM does). The difference is illustrated by the

following two search trees:

a(0,0) =

0

a(0,0) =

0

f(0) =

1

f(0) =

1

a(0,1) =

1

2

a(0,1) =

1

2

⊗

⊗

a(1,1) = 2

Search WWH ::

Custom Search