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