Information Technology Reference
In-Depth Information
-
If
l
is a Boolean cell term
ce
,and(
ce, D
)
D
and add (
ce,
TRUE
)to
Pmod
; similarly, if
l
is the negation of a Boolean
cell term in
∈D
, then delete (
ce, D
)from
D
, i.e.
¬ce
, delete (
ce, D
)from
D
and add (
ce,
FALSE
)to
Pmod
.
-
If
l
is of the form
EQ
(
ce, e
)(or
EQ
(
e, ce
)), and (
ce, D
)
∈D
, delete (
ce, D
)
from
D
and add (
ce, e
)to
Pmod
; similarly, if
l
is of the form
¬
EQ
(
ce, e
)
(or
¬
EQ
(
e, ce
)), and (
ce, D
)
∈D
, then delete
e
from
D
.
(3) For each pair (
ce, D
)
∈D
,if
D
=
∅
, then replace
Ψ
by
FALSE
,andexitfrom
the procedure; if
D
=
{e}
(i.e.
|D|
= 1), then delete the pair (
ce, D
)from
, and add the assignment (
ce, e
)to
Pmod
.
(4) Let
E
∗
=
groundCC
(
Pmod∪E
(
Ψ
)), where
E
(
X
)isthesetofallequationsin
X
and
groundCC
(
Q
) returns the consequences of the congruence closure of
ground equations
Q
.If
E
∗
and
Pmod
are inconsistent, replace
Ψ
by
FALSE
and exit from the procedure; otherwise extend
Pmod
with all cell assign-
ments in
E
∗
.
D
The last item in the above list is an addition to the original constraint propaga-
tion procedure implemented in SEM. Basically, the extended search algorithm
tries to deduce useful information using congruence closure computation, from
all the equations in
Ψ
and all the cell assignments in
Pmod
.
When will
E
∗
and
Pmod
be inconsistent? Firstly, if
E
∗
puts two domain
elements in the same equivalence class (e.g.,
1=2
,orTRUE=FALSE),weget
an inconsistency. Secondly, if
E
∗
contains
ce
=
v
but
v
is not in
Dom
(
ce
), then it
is also inconsistent. When consistent, we extend the current partial assignment
Pmod
with all cell assignments in
E
∗
, i.e. equations like
a(0,1) = 2
.
5
Implementation and Experiments
We have extended SEM [16] with the Nelson-Oppen algorithm [8] for computing
congruences. We call the new version SEMc.
The implementation of the congruence closure algorithm is straightforward.
No advanced data structures are used. As a result, the eciency is not so good.
But this still allows us to experiment with the new search procedure.
Since congruence computation may not offer new information at all nodes of
the search tree, we add a control parameter (denoted by
Lvl
)toSEMc.Itmeans
that congruence is only computed at nodes whose levels are less than
Lvl
.
We have experimented with SEMc on some model generation problems. Ta-
ble 1 compares the performances of SEMc with that of SEM. The results were
obtained on a Dell Optiplex GX270 (Pentium 4, 2.8 GHz, 2G memory), running
RedHat Linux. In the table, the running times are given in seconds. A “round”
refers to the number of times when we try to find an appropriate value for a
selected cell. This can be done either when extending a partial solution (i.e.,
trying to assign a value for a new cell) or during backtracking (i.e., trying to
assign a new value to a cell which already has a value).
Here
BN1
refers to the combinatorial logic problem described in Section 3.
The problem
g1x
has the following two clauses:
Search WWH ::
Custom Search