Information Technology Reference
In-Depth Information
Example 23.
We consider the formula from Example 11.
φ
0
:
u
1
≈ f
(
x
1
,y
1
)
∧ u
2
≈ f
(
x
2
,y
2
)
∧ z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
f
(
x
1
,y
1
)
,f
(
x
2
,y
2
))
.
After applying the term reduction rule, we obtain
φ
1
:
u
1
≈ v
1
∧ u
2
≈ v
2
∧ z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
v
1
,v
2
)
,
where a term
f
(
x
1
,y
1
) is replaced by a fresh variable
v
1
and a term
f
(
x
2
,y
2
)is
replaced by a fresh variable
v
2
.
The Optimized
UIF-DPLL
Procedure
6.2
The optimized
UIF-DPLL
procedure invokes the function
REDUCE
() which takes
as an input a CNF
φ
and returns a reduced CNF which is obtained by applying
the unit propagation I rule, the unit propagation II rule, the tautology atom
removing rule and the term reduction rule.
Example 24.
We consider the formula from Example 11.
φ
0
:
u
1
≈ f
(
x
1
,y
1
)
∧ u
2
≈ f
(
x
2
,y
2
)
∧ z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
f
(
x
1
,y
1
)
,f
(
x
2
,y
2
))
.
After applying the term reduction rule, we obtain
φ
1
:
u
1
≈ v
1
∧ u
2
≈ v
2
∧ z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
v
1
,v
2
)
,
where a term
f
(
x
1
,y
1
) is replaced by a fresh variable
v
1
and a term
f
(
x
2
,y
2
)is
replaced by a fresh variable
v
2
.
After applying the unit propagation I rule, we obtain
φ
2
:
u
2
≈ v
2
∧ z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
u
1
,v
2
)
,
φ
3
:
z ≈ g
(
u
1
,u
2
)
∧ z ≈ g
(
u
1
,u
2
)
,
φ
4
:
z ≈ g
(
u
1
,u
2
)
∧ z ≈ z.
After applying tautology atoms removing rule, we obtain
φ
5
:
z ≈ g
(
u
1
,u
2
)
∧⊥.
6.3
Soundness and Completeness of the Optimized Procedure
In this section we will prove the soundness and completeness of the optimized
procedure. An only difference the optimized
UIF-DPLL
comparing to the basic
UIF-DPLL
that it replaces all reducible terms by fresh variables.
Theorem 25.
Let
t
be reducible in
φ
;
x
be a fresh variable in
φ
.Then
φ
is
satisfiable iff
φ
[
t
:=
x
]
is satisfiable.
Search WWH ::
Custom Search