Information Technology Reference
In-Depth Information
(
)
x
i
,
1
≥
x
i
,
2
≥···≥
ↆ[
]
1
x
i
,
n
for
i
m
, and
(
)
x
i
,
k
≥
,
ↆ[
]
,
ↆ[
]
,
<
.
2
x
j
,
k
for
i
j
m
k
n
i
j
Clauses of type (1) express the fact that every pigeon is mapped to some hole, while
the clauses of type (2) indicate that at most one pigeon can be mapped to any hole.
The number of clauses in
+
2
n
PHP
n
m
2
n
.
¬
<
is
m
PHP
n
)
Lemma 2.2
g
(
¬
n
Proof
We give a strategy for Delayer scoring at least
n
points. When asked for the
value of a variable
x
i
,
j
Delayer answers 0 if for some
i
∧
∩=
i
,
x
i
∧
,
j
has been assigned
value 1, otherwise she assigns value
to
x
i
,
j
. With this strategy the game can only
end when a clause of Type 1 has been falsified. Observe that since Delayer does not
assign any 1's, for every 0 she assigns to a variable
x
i
,
j
, she must have assigned
before a
to another variable
x
i
∧
,
j
that is set to 1 by Prover. When a clause
j
=
1
x
i
,
j
is falsified because all its variables have value 0, Delayer has assigned a
to at least
one variable
x
i
∧
,
j
corresponding to position
j
for each position, and therefore she has
scored at least
n
points.
Exercise 2.3
Show by designing a suitable strategy for Prover that it also holds
PHP
n
)
(
¬
g
n.
We show now that for an unsatisfiable CNF formula
F
, the space needed in a
tree-like resolution refutation of
F
is exactly
g
(
F
)
+
1. In our example this implies
PHP
n
that the tree-like resolution space for
¬
is exactly
n
+
1 independently of
m
.
We show first that
g
(
F
)
+
1 is an upper bound for the tree-like resolution space.
Theorem 2.4
[
ET03
]
If a CNF formula F requires tree-like resolution space s, then
Delayer has a strategy in which at least s
−
1
points can be scored.
Proof
Let
s
be the minimum space needed in any tree-like resolution refutation of
F
.
We give a strategy for Delayer for playing the combinatorial game on
F
that scores
at least
s
1 points with any strategy of Prover. We prove the result by induction on
n
, the number of variables in
F
.
For the base case
n
−
=
1,
F
contains just one variable and therefore
s
2. Delayer
just needs to answer
to the only variable asked by Prover.
For
n
>
1, let
x
be the first variable asked by Prover and let
F
{
x
=
1
}
and
{
=
}
the
CNF
formulas obtained after given value 1 and 0 respectively to
variable
x
in
F
. Any tree-like refutation of
F
requires
s
pebbles and therefore either
F
x
0
(i) the tree-like space for refuting each of
F
{
x
=
1
}
and
F
{
x
=
0
}
is at least
s
−
1or
(ii) for one of the formulas (say
F
{
x
=
1
}
) the tree-like resolution space is at least
s
.
Any other possibility would imply that
F
could be refuted in space less than
s
.
In the first case, Delayer can answer
and she scores one point. By induction hypothe-
sis Delayer can score
s
−
2more points playing the game in any of the formulas
F
{
x
=
1
. In the second case, Delayer answers the value leading to the formula
that requires tree-like resolution space
s
(
x
}
or
F
{
x
=
0
}
=
1 in this case) and the game is played on
{
=
}
F
x
1
in the next round.
