Information Technology Reference
In-Depth Information
If
'
is satisable, then there exists an assignment (
x
1
;:::;x
n
)=(
z
1
;:::;z
n
)
R
:
satisfying
'
. It is sucient to take
x
1
7! fz
1
g;:::;x
n
7! fz
n
g
as the
R
:
singleton allocation. If
'
is unsatisable, it is sucient to take
x
1
;:::;x
n
7!
f
0
g
.
However, nding the singleton allocation
R
amounts to a head-on attack
on the primary NP-complete problem. Instead, we generalize the problem and
attempt to nd a small range allocation which is adequate for a
set
of formulas
'
'
which are \structurally similar" to the formula
, and includes
itself.
Consequently, we say that the range allocation
R
is
adequate
for the formula
set
if, for every equality formula in the set
' 2
,
'
is satisable i
'
is
satisable over
R
.
5.3
An Approach Based on the Set of Atomic Formulas
We assume that
has no constants or boolean variables, and is given in a positive
form, i.e. negations are only allowed within atomic formulas of the form
'
x
j
.
Any equality formula can be brought into such positive form, by expressing all
boolean operations such as
x
i
=
!
,
and the
if-then-else
construct in terms of the
basic boolean operations
:
,
_
,and
^
, and pushing all negations inside.
Let
At
(
'
) be the set of all atomic formulas of the form
x
i
=
x
j
or
x
i
=
x
j
appearing in
) be the family of all equality formulas which have
the same set of atomic formulas as
'
, and let
(
'
'
. Obviously
' 2
(
'
). Note that the family
dened by the atomic formula set
fx
1
=
x
2
;x
1
6
=
x
2
g
includes both the satisable
formula
x
1
=
x
2
_ x
1
6
=
x
2
and the unsatisable formula
x
1
=
x
2
^ x
1
6
=
x
2
.
For a set of atomic formulas
A
, we say that the subset
B
=
f
1
;:::;
k
gA
is
consistent
if the conjunction
1
^^
k
is satisable. Note that a set
B
is con-
sistent i it does not contain a chain of the form
x
1
=
x
2
;x
2
=
x
3
;:::;x
r−
1
=
x
r
together with the formula
x
r
.
Given a set of atomic formulas
x
1
=
A
, a range allocation
R
is dened to be
A
B A
R
satisfactory
for
if every consistent subset
is
-satisable.
R
x
1
;x
2
;x
3
7! f
For example, the range allocation
:
0
g
is satisfactory for the
fx
1
=
atomic formula set
x
2
;x
2
=
x
3
g
, while the allocation
R
:
x
1
7! f
1
g;x
2
7!
f
2
g;x
3
7! f
3
g
is satisfactory for the formula set
fx
1
=
x
2
;x
2
6
=
x
3
g
.Onthe
other hand, no singleton allocation is satisfactory for the set
fx
1
=
x
2
;x
1
6
=
x
2
g
.
A minimal satisfactory allocation for this set can be given by
R
:
x
1
7! f
1
g;x
2
7!
f
1
;
2
g
.
Claim.
The range allocation
R
is satisfactory for the atomic formula set
A
i
R
is adequate for
(
A
), the set of formulas
'
such that
At
(
'
)=
A
.
Thus, we concentrate our eorts on nding a small range allocation which is
satisfactory for
. In view of the claim,
we will continue to use the terms satisfactory and adequate synonymously.
We partition the set
A
=
At
(
'
) for a given equality formula
'
A
into the two sets
A
=
A
=
[ A
6
=
,where
A
=
contains
all the equality formulas in
A
, while
A
6
=
contains the inequalities.
can be computed
without actually carrying out the transformation to positive form. All that is
Note that the sets
A
=
(
'
)and
A
6
=
(
'
) for a given formula
'
Search WWH ::
Custom Search