Information Technology Reference
In-Depth Information
We experimentally observed that a good strategy to evaluate an expression
A
1
...
A
n
is to process sets
A
i
with increasing cardinality.
Equation (11) can now be rewritten in a simpler way as follows.
Safe
(
ua
)
=
⎣
h
⎦
(14)
C
∈
{C
h
| C
h
is a minimal
h
-predecessor of
LSafe
(
ua
)
}
∈
H
We can go further by reconsidering the notions of minimal
a
-and
h
-prede-
cessor with the new operator
. From the definition of minimal predecessor,
C
iff
we immediately get that
C
is a minimal
a
-predecessor of
C
belongs to
the set
(
q
,σ
)
∈C
→
(
q
,σ
)
, and similarly for
h
-minimal
predecessors. A similar improvement can be provided for
Safe
(
a
)
.
{
(
q,σ
)
}|
(
q,σ
)
a
5.3 Using a SAT Solver to Find Minimal Predecessors
The operator
allows to compute Step 1 and Step 2. Equation (13) accelerates
these computations. In this section, we propose a method to compute Step 1
based on a SAT solver (a similar approach also works for Step 2).
A SAT solver is an algorithm used to eciently test the satisfiability of a
boolean formula
ϕ
, that is, to check whether there exists a valuation
v
of the
boolean variables of
ϕ
that makes
ϕ
true. In this case we say that
v
is a
model
of
ϕ
, denoted by
v
=
ϕ
.
In Step 1, the computation of set
|
LSafe
(
ua
)
Safe
(
u
)
from
is given in (7):
C
∈
LSafe
(
ua
)
=
{C | C
is an
a
-predecessor of
Safe
(
u
)
}
.
C
if for all (
q
,σ
)
∈ C
,thereexists
We recall that
C
is an
a
-predecessor of
a
→
(
q
,σ
). We also recall that
(
q,σ
)
∈ C
such that (
q,σ
)
C ∈
LSafe
(
ua
)
is
C ⊆
Q
×
Γ
k
for some
k
. Let us associate a boolean
a finite object such that
variable
x
c
to each configuration
c
Γ
k
.
We consider the following boolean formula
ϕ
a
:
∈
Q
×
ϕ
a
=
x
c
,
C
∈Safe
(
u
)
c
∈C
c
a
→
c
Let
v
C
be the valuation such that
v
C
(
x
c
)=1iff
c
∈ C
. We immediately obtain
that:
Γ
k
.
We define an ordering over valuations as follows, in a way to have a notion of
minimal models equivalent to
v
C
|
=
ϕ
a
iff
C ∈
LSafe
(
ua
)
∩
Q
×
-minimal elements of
LSafe
(
ua
).
Let
V
be a set of boolean variables, let
v
and
v
be two valuations over
V
.
We define
v
≤
⊆
V
,
v
(
x
)=1 =
v
iff for all variables
x
∈
⇒
v
(
x
) = 1. We denote
v
<v
if
v
≤
v
and
v
=
v
.Given
ϕ
a boolean formula over
V
,wesaythata
model
v
of
ϕ
is
minimal
if for all model
v
of
ϕ
,wehave
v
≤
v
=
v
.We
v
=
⇒
get the next characterization.
