Information Technology Reference
In-Depth Information
Lemma 9.
(termination) Let
φ ∈
Cnf
. Then the set of reduction rules of the
UIF-DPLL
calculus is terminating.
Proof.
Let we have a CNF
φ
and let after applying an arbitrary reduction rule
of the
UIF-DPLL
calculus we obtained a CNF
ψ
. One can check that either
NPCls
(
ψ
)
≺
2
are well-founded
orders on CNFs. We obtain that the set of reduction rules of the
UIF-DPLL
calculus is terminating.
<
NPCls
(
φ
)or
k
(
ψ
)
<k
(
φ
). Trivially,
≺
1
and
5The
UIF-DPLL
Procedure
In this section we introduce the
UIF-DPLL
procedure and prove its soundness
and completeness.
The algorithm is implemented by the function
UIF-DPLL
() in Figure 2.
The
UIF-DPLL
procedure takes in input a EUF formula in conjunctive normal
form and returns either “satisfiable” or “unsatisfiable”. It invokes the function
REDUCE
.
REDUCE
takes in input a CNF
φ
, applies the reduction rules of
UIF-DPLL
calculus till none of the rules is applicable, and returns a reduced CNF.
The function
REDUCE
(
φ
) is not uniquely defined as we will show with an
example.
Example 10.
Let us consider the formula
φ
=
{{a ≈ f
(
b
)
}, {a ≈ g
(
c
)
}, {f
(
b
)
≈ h
(
a, c
)
}}
.
We will apply unit propagation II rule on
a ≈ f
(
b
). We can replace
a
with
f
(
b
).
In this case we obtain
φ
=
{{a ≈ f
(
b
)
}, {f
(
b
)
≈ g
(
c
)
}, {f
(
b
)
≈ h
(
f
(
b
)
,c
)
}}
.
The formula
φ
is reduced.
We can also replace
f
(
b
)with
a
. The result is the reduced formula
φ
=
{{a ≈ f
(
b
)
}, {a ≈ g
(
c
)
}, {a ≈ h
(
a, c
)
}}
.
The
UIF-DPLL
procedure is done recursively, according the following steps.
• φ
is replaced by a CNF
REDUCE
(
φ
) such that
φ
is satisfiable iff
REDUCE
(
φ
)
is satisfiable.
•
If
⊥∈φ
,
UIF-DPLL
(
φ
) returns “unsatisfiable”.
•
If
Core
(
φ
)=
∅
,where
φ
is reduced, then
UIF-DPLL
(
φ
) returns “satisfiable”.
•
If none of the above situations occurs, then
ChooseLiteral
(
Core
(
φ
)) returns a
literal which occurs in
Core
(
φ
) according some heuristic criterion.
Search WWH ::
Custom Search