Information Technology Reference
In-Depth Information
had been set by Prover because Delayer only sets 0's when a hole is not free or a
pigeon has already a hole. Therefore, Delayer scores at least
n
p 0
(
)
points for
this. Observe that since Delayer does not allow a pigeon to be in more than one hole,
the 0's set by Prover are different for every pigeon i . Summarizing, Delayer receives
either
2 log
points for each of the 2 variables x i , j i set to 1.
Let us now define the values for p 0 and p 1 . Intuitively Delayer has to score more
points when Prover sets a variable to 1 than we he sets it to 0 because the former
brings the game quicker to an unsatisfying assignment. We define:
p 1
n
p 0
log
(
)
or
2 log
(
)
2 log n
= e
=
log n
n
log n
n
log n
n
p 1
and p 0
=
=
1
n
The number of points scored for each of the 2 variables is then either
p 1
log
(
) =
n
p 0
(
With more complicated arguments the authors of the original paper [ BGL10 ]
provide a lower bound of
log n
)
or
2 log
(
) = (
log n
),
and the total number of points
(
n log n
)
.
n
n
2
PHP n )
. The best existing lower
bounds for the tree-like resolution size for PHP can be seen as consequences of this
result and Theorem 3.2:
Theorem 3.5 [ IM99 , D R0 1 ] Fo r m
2 log
(
+
1
)
for G
( ¬
>
n the size of a tree-like resolution refutation
is at least 2 2 log (
2 +
1
) .
PHP n
of
¬
9.4 Conclusions
We have shown in this tutorial that variations of a combinatorial game played on
formulas, characterize exactly the concepts of space and size in tree-like resolution.
It is interesting to observe that the outcome of these games depends only on the
structure of the input formulas. This means that the concepts of tree-like resolution
space and size are complexity measures intrinsic to the formulas and completely
independent of the notion of resolution. It is an important open question whether
such game characterizations also exist for the case of general resolution.
References
[ABRW02] M. Alekhnovich, E. Ben-Sasson, A.A. Razborov, A. Wigderson, Space complexity in
propositional calculus. SIAM J. Comput. 31 (4), 1184-1211 (2002)
[BP96]
P. Beame, T. Pitassi, Simplified and improved resolution lower bounds, in 37th Annual
IEEE Symposium on Foundations of Computer Science , pp. 274-282 (1996)
[BIW04]
E. Ben-Sasson, R. Impagliazzo, A. Wigderson, Near-optimal separation of tree-like
and general resolution. Combinatorica 24 (4), 585-603 (2004)
[BN08]
E. Ben-Sasson, J. Nordström, Short proofs may be spacious: an optimal separation of
space and length in resolution, in Proceedings of 49th FOCS Conference , pp. 709-718
(2008)
 
Search WWH ::




Custom Search