Information Technology Reference
In-Depth Information
Lemma 3.
v
C
is a minimal model of
ϕ
a
iff
C ∈
LSafe
(
ua
)
.
We can now explain how to compute all the minimal models of formula
ϕ
a
.
Let
ϕ
be a boolean formula over
V
.
First, we explain, knowing a model
v
of
ϕ
, how to compute a model
v
of
ϕ
such
that
v
<v
(if it exists). Consider the next formula
ϕ
:
(
(
ϕ
=
ϕ
∧
x∈V
0
¬
x
)
∧
x∈V
1
¬
x
)
where
V
0
(respectively
V
1
) is the set of all variables
x
V
such that
v
(
x
)=0
(resp.
v
(
x
)=1).If
ϕ
has a model
v
, it follows from the definition of
ϕ
that
v
is a model of
ϕ
such that
v
<v
.Otherwise,
v
is a minimal model of
ϕ
.So
from a model of
ϕ
we can compute a minimal model of
ϕ
by repeating the above
procedure.
Second, let us explain how to compute all the minimal models of
ϕ
. Suppose that
we already know some minimal model
v
of
ϕ
, and let
V
1
be the set of variables
x
∈
∈
V
such that
v
(
x
) = 1. Consider the formula
(
x
ϕ
=
ϕ
∧
V
1
¬
x
)
.
∈
Then a model
v
of
ϕ
, if it exists, is a model of
ϕ
such that neither
v
<v
(since
v
is minimal) nor
v<v
(by definition of
ϕ
). With the previous procedure,
we thus get a minimal model of
ϕ
that is distinct from
v
.Inthiswaywecan
compute all minimal models of
ϕ
.
5.4 Improved Algorithm and Data Structures
Let us come back to Algorithm 2 by indicating the underlying data structures
and the improvements resulting from the previous three sections.
As explained in Section 5.1, we restrict the computations to the set
H
of
minimal hedges. Notice that the algorithm that computes the set
{
rel
h
|
h
∈
H
}
can be easily adapted to compute the set of its
-minimal elements. In the main
loop of Algorithm 2, Steps 1 and 2 can be computed either with the new operator
≤
or with a SAT solver (see Sections 5.2 and 5.3 resp.).
Ecient data structures are used both for the relations associated to minimal
hedges and for the antichains
H
,
Safe
(
u
)
and
LSafe
(
u
)
.Arelation
rel
h
,
with
h
, is stored as an array of bit-vectors. In this way the composition is
computed eciently using bit-operations, as well as the number of elements of
the relation. A hash table is used to store each antichain, such that elements with
different weights are stored in different lists. In the case of
∈
H
H
, the weight is the
number of elements of
rel
h
∈
H
.Inthecaseof
Safe
(
u
)
(resp.
LSafe
(
u
)
),
the weight is the number of elements of
).
In this way, comparing a new element with the elements of the antichain is made
more ecient, by limiting the comparison with elements of the same weight.
C ∈
Safe
(
u
)
(resp.
C ∈
LSafe
(
u
)
