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