Information Technology Reference
In-Depth Information
UIF-DPLL
(
φ
):
begin
φ
:=
REDUCE
(
φ
);
if (
)
return “unsatisfiable”;
if (
Core
(
φ
)=
∅
)
return “satisfiable”;
l
:=
ChooseLiteral
(
Core
(
φ
));
if (
UIF-DPLL
(
φ ∪{{l}}
) is “satisfiable”)
return “satisfiable”;
⊥∈φ
else
return
UIF-DPLL
(
φ ∪ {{¬l}}
);
end
Fig. 2.
The
UIF-DPLL
procedure
Example 11.
As am example we consider the formula raised during translation
validation [9], where concrete functions replaced by uninterpreted function sym-
bols.
φ
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 unit propagation II rule, we obtain
φ
1
=
{{u
1
≈ f
(
x
1
,y
1
)
}, {u
2
≈ f
(
x
2
,y
2
)
}, {z ≈ g
(
u
1
,u
2
)
},
{z ≈ g
(
u
1
,f
(
x
2
,y
2
))
}},
φ
2
=
{{u
1
≈ f
(
x
1
,y
1
)
}, {u
2
≈ f
(
x
2
,y
2
)
}, {z ≈ g
(
u
1
,u
2
)
}, {z ≈ g
(
u
1
,u
2
)
}},
φ
3
=
{{u
1
≈ f
(
x
1
,y
1
)
}, {u
2
≈ f
(
x
2
,y
2
)
}, {z ≈ g
(
u
1
,u
2
)
}, {z ≈ z}}.
After applying tautology atom removing rule, we obtain
φ
4
=
{{u
1
≈ f
(
x
1
,y
1
)
}, {u
2
≈ f
(
x
2
,y
2
)
}, {z ≈ g
(
u
1
,u
2
)
}, ⊥}.
Since
⊥∈φ
4
then
φ
4
is unsatisfiable and therefore
φ
0
is unsatisfiable.
5.1
Satisfiability Criterion
Let
φ
be a reduced CNF not containing the empty clause;
Core
(
φ
)=
∅
. We will
give a proof that such CNF
φ
is satisfiable.
Let
φ
be a reduced CNF and
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. Then, trivially, if
I
∅
.Since
Core
(
φ
)=
∅
|
=
ψ
for some E-interpretation
I
then
I
=
φ
, i.e.
φ
is satisfiable if
ψ
is satisfiable. It means that w.l.o.g. we can
restrict ourself to the case when
φ
contains only unit clauses.
|
Search WWH ::
Custom Search