Information Technology Reference
In-Depth Information
Theorem 1.8
Let F be an unsatisfiable CNF formula with a tree-like refutation of
size s, then F has a tree-like resolution refutation of space
∃
+
log
s
1
.
Proof
As mentioned in Exercise 1.6, the resolution tree in the refutation of
F
can
be pebbled with
d
1 pebbles, where
d
is the depth of the biggest complete binary
tree embedded in the refutation tree. As the biggest possible complete binary tree
embedded in a tree of size
s
has depth
+
∃
log
s
, the result follows.
Exercise 1.9
Show that if in an unsatisfiable formula F all its clauses have at most
2 literals, then there is a tree-like resolution refutation for F with constant space and
polynomial size.
9.2 A Combinatorial Game for Proving Lower Bounds
in Tree-Like Resolution
Impagliazzo and Pudlák introduced in [
PI00
] a combinatorial game for proving lower
bounds on the size of tree-like refutations. This game was also used in [
BIW04
]. We
will show that this game exactly characterizes tree-like resolution space.
The Prover-Delayer game:
The game is played in rounds on an unsatisfiable set of clauses
F
by two players:
Prover and Delayer.
2
Prover wants to falsify some initial clause and Delayer tries to
retard this as much as possible. In each round Prover chooses a variable in
F
and asks
Delayer for a value for this variable. Delayer can answer either 0,1 or
. In this last
case Prover can choose the truth value (0 or 1) for the variable and Delayer scores
one point. The variable is set to the selected value and the next round begins. The
game ends when a clause in
F
is falsified (all its literals are set to 0) by the partial
assignment constructed in this way. The goal of Delayer is to score as many points
as possible and Prover tries to prevent this. The outcome of the game is the number
of points scored by Delayer.
(
)
Definition 2.1
Let
F
be an unsatisfiable formula in CNF. We denote by
g
the
maximum number of points that Delayer can score while playing the game on
F
with an optimal strategy of Prover.
F
As an example we show how this game applies to the family of formulas for
the general Pigeonhole Principle PHP
n
. These formulas express the fact that it is
not possible to fit
m
pigeons in
n
pigeonholes (for
m
>
n
). For the case
m
=
PHP
n
was the first example of a family of formulas with an exponential
resolution size lower bound [
Hak85
]. The contradiction
n
+
1,
¬
PHP
n
can be written as
a CNF formula in the following way: The variables of the formula are
x
i
,
j
,
¬
i
ↆ
[
.
x
i
,
j
has the intuitive meaning that pigeon
i
is mapped to hole
j
. There
are
mn
variables. The clauses of the formula are:
m
]
,
j
ↆ[
n
]
2
For clarity in the exposition Delayer is a female player.
