Information Technology Reference
In-Depth Information
Proof.
See [11].
Theorem 17.
(Satisfiability criterion) Let
φ ∈
Cnf
such that
-
φ
is reduced,
-
⊥ ∈ φ
,
-
Core
(
φ
)=
∅
.
Then
φ
is satisfiable.
Proof.
By the theorem assumption
Core
(
φ
)=
. Then every clause of length
more than one contains at least one negative literal. Let
ψ ∈
Cnf
is obtained
from
φ
by removing from all clauses of length more than one all literals except
one negative literal. Obtained
∅
ψ
is reduced by construction. Since
ψ ∈
UCnf
and
ψ
is reduced then by Lemma 15 and Theorem 16,
ψ
is satisfiable. If
ψ
is
satisfiable then
I
|
=
ψ
for some E-interpretation
I
. One can easily see, that
I
|
=
φ
,
i.e.
φ
is satisfiable.
Soundness and Completeness of the
UIF-DPLL
Procedure
5.2
In this section we will prove that the
UIF-DPLL
procedure is sound and com-
plete. One can see that both rules for unit propagation and the tautology atoms
removing preserve (un)satisfiability of a formula.
Lemma 18.
Let
φ ∈
Cnf
.Then
φ
is satisfiable if and only if
REDUCE
(
φ
)
is
satisfiable.
Proof.
One can easily check that the rules of the
UIF-DPLL
calculus preserve
(un)satisfiability.
Theorem 19.
(
Soundness and Completeness
)
ACNF
φ
is unsatisfiable if and
only if the
UIF-DPLL
(
φ
)
returns “unsatisfiable”.
Proof.
(
⇒
)Let
φ
be unsatisfiable CNF.
Let
⊥∈φ
. Then by definition of the function
REDUCE
(),
⊥∈
REDUCE
(
φ
),
and the procedure returns “unsatisfiable”.
Let
⊥ ∈ φ
. We will give a proof by induction on
|
MLit
(
Core
(
φ
))
|
.
Base case
.
|
MLit
(
Core
(
φ
))
|
= 0. Then one of the following holds.
-
⊥∈
REDUCE
(
φ
). Then the procedure returns “unsatisfiable”.
-
⊥ ∈
REDUCE
(
φ
). Since
.
By Theorem 17, we obtain that
REDUCE
(
φ
) is satisfiable. By Lemma 18,
φ
is also satisfiable. We obtain a contradiction with the assumption that
φ
is
unsatisfiable. Then
|
MLit
(
Core
(
φ
))
|
=0then
Core
(
REDUCE
(
φ
)) =
∅
⊥∈
REDUCE
(
φ
) and the procedure returns “unsatisfi-
able”.
Inductive step
.Letforevery
ψ ∈
Cnf
the procedure returns “unsatisfiable” if
|
MLit
(
Core
(
ψ
))
| <n
.
Assume that
=
n
.Wedenote
REDUCE
(
φ
)by
ψ
.Onecan
easily check that by definition of
UIF-DPLL
,foreach
l ∈
Core
(
ψ
)
|
MLit
(
Core
(
φ
))
|
Search WWH ::
Custom Search