Information Technology Reference
In-Depth Information
and
x
1
. Resolving them we obtain
. For the induction step, by giving variable
x
n
the values 0 and 1 we obtain two new sets of clauses
F
{
=
}
{
=
}
x
n
0
and
F
x
n
1
containing at most
n
1 variables. Since
F
is unsatisfiable, so are the new sets
of clauses and applying the induction hypothesis we know that there exist tree-like
resolution refutations
R
0
and
R
1
for
F
−
{
x
n
=
0
}
and
F
{
x
n
=
1
}
. The clauses of
F
{
x
n
=
0
}
are either clauses of
F
(not containing variable
x
n
) or are clauses
C
for
which
C
x
n
is in
F
. By adding
x
n
to the initial clauses of this type in
R
0
we either
get a tree-like derivation of
x
n
from clauses in
F
(variable
x
n
is never resolved) or a
derivation of
≥
(in case none of the clauses in
R
0
contain variable
x
n
). In the later
case we are done, oth
erw
ise we can do the same process on
R
1
obtaining either a
tree-like derivation of
x
n
from
F
or a refutation of
F
. Again, in the second case
we
are done, otherwise we put together the tree-like resolution derivations of
x
n
and
x
n
and the resolvent of this two clauses to obtain a tree-like refutation of
F
.
From the proof of the above Theorem it follows that the number of clauses needed
in a tree-like refutation of a formula
F
is at most exponential in the number of its
variables.
It is known that for certain formulas general resolution can produce shorter refuta-
tions than tree-like resolution [
BEGJ02
,
BIW04
]. The reason for this is that, contrary
to general resolution, in tree-like resolution if a clause is needed more than once it
must be re-derived from the initial clauses each time. Even if tree-like refutations can
be larger than in general resolution, the study of this proof system is well motivated
bymanymethods used in practice for testing satisfiability (SAT solvers). These meth-
ods are in fact concrete implementations of tree-like resolution. Most SAT solvers
are based on the basic backtracking algorithm:
proc
Backtracking
(
F
:
set of clauses
,ˇ
:
assignment
)
:
bool
//
outputs 1, if F
ˇ
is satisfiable and 0 otherwise
if
ↆ
F
ˇ
then return
0
if
F
then return
1
else
(choose a variable
x
ˇ
=≤
ↆ
Va r
(
F
ˇ))
if
Backtracking
(
F
,ˇ
{
x
=
0
}
)
then return
1
else return
Backtracking
(
F
,ˇ
{
x
=
1
}
)
In order to test if a formula is satisfiable, the algorithms starts with the empty
assignment. This backtracking algorithm is in principle more efficient than a straight-
forward test of all possible total assignments for the variables because when for a
partial assignment
ˇ
, the algorithms obtains
ↆ
F
ˇ
, then it follows
F
ʲ
=
0 for all
extensions
. The Algorithm does not need to explore the sub-tree with the
possible extensions from
ʲ
from
ˇ
and this decreases the search space.
In the algorithm we have not specified the way to choose the next variable to be
considered. There are many ways to do this. Modern SAT solvers use refinedmethods
for choosing the next variable to be assigned as well as many other techniques for
efficiently pruning the search tree (see e.g., [
ST13
]).
ˇ
