Information Technology Reference
In-Depth Information
p
i
be the number of points scored by Delayer after round
i
. When Delayer assigns
values
p
0
p
1
(
,
)
(
ˇ
i
−
1
{
=
to a variable
x
at step
i
then Prover gives
x
value 0 if
L
R
x
p
0
L
0
and assigns
x
value 1 otherwise. By the property of the weights
p
0
and
p
1
and by the fact that
L
}
)
(
R
ˇ
i
−
1
)
(
R
ˇ
i
−
1
)
=
L
(
R
ˇ
i
−
1
{
x
=
0
}
)
+
L
(
R
ˇ
i
−
1
{
x
=
1
}
)
p
1
L
it follows that in this last case
L
ˇ
i
−
1
).
We show by induction on the number
i
of rounds that with this strategy
(
R
ˇ
i
−
1
{
x
=
1
}
)
(
R
L
(
R
)
2
p
i
ˇ
i
)
.
L
(
R
Again the result follows from this because when the game has reached a contradiction
of an initial clause after constructing an assignment
ˇ
(
ˇ)
=
then
L
R
1 and the
inequality shows 2
p
(
)
.
In the beginning of the game
R
L
R
ˇ
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 weights
p
0
p
1
,
to it, and Prover selects value
b
ↆ{
0
,
1
}
for the variable,
we get
2
p
i
p
b
L
(
R
)
L
(
R
)
2
p
i
−
log
p
b
2
p
i
+
1
=
=
ˇ
i
)
p
b
L
(
R
L
(
R
ˇ
i
+
1
)
and the result follows.
The extended game completely characterizes the size of a tree-like resolution
proof. This is a consequence of Theorem 3.2 and the converse result:
Theorem 3.3
[
BGL13
]
Let F be an unsatisfiable formula in CNF. If the smallest
tree-like refutation for F has size S then G
S
(
F
)
log
∃
2
.
Proof
Let
L
be the number of leaves in the shortest tree-like refutation of
F
.
When a new variable
x
is selected by Prover and
(
F
)
is the partial assignment computed
so far, Delayer assigns weights according to the following rules: for
b
ˇ
ↆ{
0
,
1
}
,
L
(
F
ˇ
{
x
=
b
}
)
p
b
=
}
)
.
L
(
F
ˇ
{
x
=
0
}
)
+
L
(
F
ˇ
{
x
=
1
We show by induction on
n
, the number of variables in
F
, that Delayer scores at
least log
L
(
F
)
points. This implies the result, since a tree-like refutation of size
S
has exactly
2
.
leaves. The base case is trivial; if there is only one variable, the
resolution tree has two leaves, and Delayer can always score 1 point. For
n
>
1, let
x
be the first variable chosen by Prover and let
b
ↆ{
0
,
1
}
be the value assigned by
log
p
b
him to it. The score of the game is
X
where
X
is the score achieved in the
subsequent steps. By induction hypothesis we have
X
−
+
log
L
(
F
{
x
=
b
}
)
. The total
score is then at least
