Information Technology Reference
In-Depth Information
Exercise 1.2
Show that in the backtracking algorithm there is a strategy for choosing
the next variable to be assigned so that on input a formula F in CNF with n variables
and at most k variables in each clause, the algorithm produces at most
2
k
n
/
k
(
−
1
)
recursive calls.
A proof of the unsatisfiability of a formula with the backtracking algorithm is
in fact a tree-like resolution refutation for the formula as can be seen in the next
well-known result:
Theorem 1.3
Let F be a nonsatisfiable formula in CNF and let r be the minimum
number of recursive calls made by the backtracking algorithm on input
(by
any ordering of the variables). Then there is a tree-like resolution refutation of F of
size at most r .
(
F
,
≤
)
Proof
The backtracking algorithm running on the input
defines a tree.
The nodes of the tree indicate what variable is being assigned. From an interior
node two edges come out, one for each of the two possible values (0 and 1) that the
variable can take. We can associate a resolution refutation with this tree. Every node
in the tree is reached from the root by a partial assignment and can be identified with
an initial clause falsified by this assignment in the following way: Every leaf in the
recursion tree is identified with a clause of
F
falsified by the assignment reaching the
leaf. Such a clause must exist because otherwise this particular assignment would
satisfy the formula. For an inner node corresponding to a variable
x
and whose chil-
dren are identified with clauses
K
i
and
K
j
, we associate a clause
K
. If both clauses
K
i
and
K
j
contain variable
x
, then in one of the clauses the variable is positive and in
the other clause it is negated. We define then the clause
K
as the resolvent of
K
i
and
K
j
. Otherwise we associate with the node the clause not containing variable
x
from
one of its children. One can see that in both cases
K
is falsified by the assignment
that goes from the root of the tree to the node. Moreover, every clause in the tree
is either the resolvent of its children or one of the clauses from the children. The
root in the recursion tree is associated to the empty clause
(
F
,
≤
)
since this is the only
clause falsified by the empty assignment. The tree with its associated clauses defines
a tree-resolution refutation for
F
with at most
r
clauses.
In this result, we have already used the natural complexitymeasure of
size
. The size
of a refutation is the number of clauses it contains. It is known that certain families of
propositional formulas need (general) resolution refutations with a number of clauses
that is exponential in the formula size [
Hak85
,
Urq87
,
CS88
,
BP96
].
Another natural complexity measure is the
space
. Intuitively, the resolution space
of a CNF formula is the minimal number of clauses that must be kept simultaneously
in order to refute a formula. The formal definition [
ET01
,
ABRW02
] is the following:
Definition 1.4
Let
k
, we say that an unsatisfiable CNF formula
F
has resolution
refutation bounded by space
k
if there is a series of CNF formulas
F
1
,...,
ↆ N
F
s
, such
that
F
1
∈
F
,
ↆ
F
s
,inany
F
i
there are at most
k
clauses, and for each
i
<
s
,
F
i
+
1
is obtained from
F
i
by:
