On the relative strength of pebbling and resolution
(2010) 25th Annual IEEE Conference on Computational Complexity, CCC 2010 In Proceedings of the Annual IEEE Conference on Computational Complexity p.151-162- 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... (More)
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 Nordström 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 Nordström 2009].
(Less)
- author
- Nordström, Jakob LU
- publishing date
- 2010
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Pebble games, Pebbling formula, Proof complexity, Resolution, Space, Trade-off
- host publication
- Proceedings - 25th Annual IEEE Conference on Computational Complexity, CCC 2010
- series title
- Proceedings of the Annual IEEE Conference on Computational Complexity
- article number
- 5497889
- pages
- 12 pages
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- 25th Annual IEEE Conference on Computational Complexity, CCC 2010
- conference location
- Cambridge, MA, United States
- conference dates
- 2010-06-09 - 2010-06-11
- external identifiers
-
- scopus:77955251566
- ISSN
- 1093-0159
- ISBN
- 9780769540603
- DOI
- 10.1109/CCC.2010.22
- language
- English
- LU publication?
- no
- id
- d14c03c1-3a40-45ec-9de5-adfac3fc2071
- date added to LUP
- 2020-12-18 22:28:16
- date last changed
- 2022-02-01 18:41:09
@inproceedings{d14c03c1-3a40-45ec-9de5-adfac3fc2071,
abstract = {{<p>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 Nordström 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 Nordström 2009].</p>}},
author = {{Nordström, Jakob}},
booktitle = {{Proceedings - 25th Annual IEEE Conference on Computational Complexity, CCC 2010}},
isbn = {{9780769540603}},
issn = {{1093-0159}},
keywords = {{Pebble games; Pebbling formula; Proof complexity; Resolution; Space; Trade-off}},
language = {{eng}},
pages = {{151--162}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
series = {{Proceedings of the Annual IEEE Conference on Computational Complexity}},
title = {{On the relative strength of pebbling and resolution}},
url = {{http://dx.doi.org/10.1109/CCC.2010.22}},
doi = {{10.1109/CCC.2010.22}},
year = {{2010}},
}