Information Technology Reference
In-Depth Information
Corollary 2.6
For any unsatisfiable CNF formula F , if Delayer has a strategy on
F which scores r points then any tree-like resolution refutation of F has size at least
2
r
+
1
−
1
.
PHP
n
needs tree-like
resolution refutation of size at least 2
n
. The given estimation for the points obtained
by Delayer on the formula
Buss and Pitassi [
BP97
] showed that for for any
m
>
n
,
¬
PHP
n
with the space characterization and the above
corollary provide an alternative proof for this result. The bound has been improved
to 2
(
n
log
n
)
in [
IM99
,
DR01
].
Computing the number of points that can be scored by Delayer on a formula is
in general not an easy task. Hertel and Urquhart [
HU07
] have shown that in fact this
problem is PSPACE complete. We finish this section with some exercises to compute
the points scored on certain formulas related to pebbling.
¬
Exercise 2.7
Consider the following pebbling formulas defined by Ben-Sasson and
Wigderson in
[
BW01
]
. They express the principle that in a directed acyclic graph,
pebbling the source nodes and following the rule that if all the predecessors of a
node
v
contain a pebble then
v
also gets one, implies that a pebble will be placed on
the sink.
Let G
be a directed acyclic graph in which every vertex has fan-in 2
or 0 with a unique sink s. We call a graph with these properties a circuit graph. We
associate
2
distinct Boolean variables
=
(
V
,
E
)
v
1
,v
2
with every vertex
v
ↆ
V. Peb
G
,the
pebbling contradiction of G, is the conjunction of:
1
2
for each source
•
v
≥
v
v
Source axioms:
.
Pebbling axioms:
u
i
j
1
2
for u and
•
≥
v
≥
w
≥
w
v
the two predecessors of
w
and
i
,
j
ↆ{
1
,
2
}
.
Sink axioms:
s
i
•
for the sink s and i
ↆ{
1
,
2
}
.
Show that for a constant c, if G is a tree then g
(
Peb
G
)
=
Peb
(
G
)
+
c
Exercise 2.8
[
Nor12
]
Consider now a variation of the pebbling formulas, defined
by Ben-Sasson and Nordström in
[
BN08
]
expressing the same principle but using the
parity function instead of disjunction. For simplicity we just define these formulas
for line graphs G
=
(
V
,
E
)
with n vertices
v
1
...v
n
with unique source
v
1
, unique
sink
v
n
and with a directed edge
(v
1
,v
i
+
1
)
for
1
i
n
−
1
. We associate
2
distinct
V. Peb
G
is the conjunction of (the
clauses expressing in conjunctive normal form the formulas):
1
2
i
Boolean variables
v
i
,v
with every vertex
v
i
ↆ
1
2
•
Source axioms:
v
1
∅
v
1
.
1
i
2
i
1
i
2
i
•
Pebbling axioms:
v
∅
v
⃐
v
1
∅
v
1
for
1
i
n
−
1
.
+
+
n
∅
v
n
)
•
Sink axioms:
¬
(v
.
Peb
G
)
=
(
Show that for a line graph G with n vertices, g
(
log
n
).
