Information Technology Reference
In-Depth Information
(
)
is also a lower bound for the tree-like resolution space.
Theorem 2.5
[
ET03
]
The tree-like space needed for refuting a CNF F is at least
g
On the other hand
g
F
1
.
Proof
Let
s
be the minimum space needed in a tree-like refutation of
F
. We describe
a Strategy for Prover in which the number
p
of points scored by Delayer is at most
s
(
F
)
+
s
. Prover
chooses the variables in the order induced by the refutation in the following way:
He starts at the empty clause in
R
and in general at the end of a round moves to
a clause
C
that is falsified by the partial assignment constructed so far. In the next
round, Prover chooses the resolved variable
x
from the two parent clauses of
C
.Let
ˇ
i
be the partial assignment constructed after
i
rounds of the game and
R
−
1. Let
R
be a tree-like resolution refutation for
F
with Peb
(
R
)
=
ˇ
i
be the
subtree of the refutation that has its root at the node reached from the root of
R
by the path specified by
ˇ
i
and let
p
i
be the number of points scored by Delayer
after round
i
. If Delayer assigns to
x
a value 0 or 1 (by setting the weights in the
way indicated above) then Prover moves to the parent clause that is falsified by
the constructed partial assignment and the new round starts. When Delayer assigns
value
to a variable
x
at step
i
then Prover gives
x
value 0 if Peb
(
R
ˇ
i
−
1
{
x
=
0
}
)
Peb
and assigns
x
value 1 otherwise. We show by induction on the
number
i
of rounds that with this strategy
(
R
ˇ
i
−
1
{
x
=
1
}
)
p
i
s
−
Peb
(
R
ˇ
i
).
The result follows from this fact because when the game has reached a contradiction
of an initial clause after constructing an assignment
ˇ
, then Peb
(
R
ˇ)
=
1 and the
inequality shows
p
1.
In the beginning of the game
R
s
−
ˇ
0
is the whole tree and Delayer has scored 0
points.
For the inductive step, if at round
i
1 Prover chooses variable
x
and Delayer
assigns values 0 or 1 to it then she does not score any points, and we get
+
p
i
+
1
=
p
i
s
−
Peb
(
R
ˇ
i
)
s
−
Peb
(
R
ˇ
i
+
1
)
since
R
ˇ
i
+
1
is a subtree of
R
ˇ
i
.
If Delayer assigns
to
x
, since Prover select the value corresponding to the
subtree from
R
ˇ
i
with the smallest pebbling number and min
{
Peb
(
R
ˇ
i
{
x
=
0
}
),
Peb
(
R
ˇ
i
{
x
=
1
}
)
}
<
Peb
(
R
ˇ
i
)
we get
p
i
+
1
=
p
i
+
1
s
−
Peb
(
R
ˇ
i
)
−
1
s
−
Peb
(
R
ˇ
i
+
1
)
and the result follows.
As mentioned before, the combinatorial game was defined in [
PI00
]asatool
for proving lower bound for the size of tree-like resolution refutation. This applica-
tion can be seen considering the relationship between tree-like space and size from
Theorem 1.8:
