Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR10-045 | 21st April 2010 23:15

On the Relative Strength of Pebbling and Resolution

RSS-Feed




Revision #1
Authors: Jakob Nordström
Accepted on: 21st April 2010 23:15
Downloads: 2691
Keywords: 


Abstract:

The last decade has seen a revival of interest in pebble games in the
context of proof complexity. Pebbling has proven to be a useful tool
for studying resolution-based proof systems when comparing the
strength of different subsystems, showing bounds on proof space, and
establishing size-space trade-offs. The typical approach has been to
encode the pebble game played on a graph as a CNF formula and then
argue that proofs of this formula must inherit (various aspects of)
the pebbling properties of the underlying graph. Unfortunately, the
reductions used here are not tight. To simulate resolution proofs by
pebblings, the full strength of nondeterministic black-white pebbling
is needed, whereas resolution is only known to be able to simulate
deterministic black pebbling. To obtain strong results, one therefore
needs to find specific graph families which either have essentially
the same properties for black and black-white pebbling (not at all
true in general) or which admit simulations of black-white pebblings
in resolution.

This paper contributes to both these approaches. First, we design a
restricted form of black-white pebbling that can be simulated in
resolution and show that there are graph families for which such
restricted pebblings can be asymptotically better than black
pebblings. This proves that, perhaps somewhat unexpectedly,
resolution can strictly beat black-only pebbling, and in particular
that the space lower bounds on pebbling formulas in [Ben-Sasson and
Nordstrom 2008] are tight. Second, we present a versatile
parametrized graph family with essentially the same properties for
black and black-white pebbling, which gives sharp simultaneous
trade-offs for black and black-white pebbling for various parameter
settings. Both of our contributions have been instrumental in
obtaining the time-space trade-off results for resolution-based proof
systems in [Ben-Sasson and Nordstrom 2009].



Changes to previous version:

Fixed typos and made other minor revisions.


Paper:

TR10-045 | 15th March 2010 23:25

On the Relative Strength of Pebbling and Resolution





TR10-045
Authors: Jakob Nordström
Publication: 16th March 2010 08:28
Downloads: 3692
Keywords: 


Abstract:

The last decade has seen a revival of interest in pebble games in the
context of proof complexity. Pebbling has proven to be a useful tool
for studying resolution-based proof systems when comparing the
strength of different subsystems, showing bounds on proof space, and
establishing size-space trade-offs. The typical approach has been to
encode the pebble game played on a graph as a CNF formula and then
argue that proofs of this formula must inherit (various aspects of)
the pebbling properties of the underlying graph. Unfortunately, the
reductions used here are not tight. To simulate resolution proofs by
pebblings, the full strength of nondeterministic black-white pebbling
is needed, whereas resolution is only known to be able to simulate
deterministic black pebbling. To obtain strong results, one therefore
needs to find specific graph families which either have essentially
the same properties for black and black-white pebbling (not at all
true in general) or which admit simulations of black-white pebblings
in resolution.

This paper contributes to both these approaches. First, we design a
restricted form of black-white pebbling that can be simulated in
resolution and show that there are graph families for which such
restricted pebblings can be asymptotically better than black
pebblings. This proves that, perhaps somewhat unexpectedly,
resolution can strictly beat black-only pebbling, and in particular
that the space lower bounds on pebbling formulas in [Ben-Sasson and
Nordstrom 2008] are tight. Second, we present a versatile
parametrized graph family with essentially the same properties for
black and black-white pebbling, which gives sharp simultaneous
trade-offs for black and black-white pebbling for various parameter
settings. Both of our contributions have been instrumental in
obtaining the time-space trade-off results for resolution-based proof
systems in [Ben-Sasson and Nordstrom 2009].



ISSN 1433-8092 | Imprint