On the Relative Strength of Pebbling and Resolution

DOI10.1145/2159531.2159538MaRDI QIDQ2946664zbMATH OpenOpenAlexFDO

Authors Jakob Nordstrom

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1003.3047

zbMATH Keywords

pebble gamespebbling formulaproof complexityresolutionspace lower boundstrade-off

Mathematics Subject Classification ID

Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Abstract: The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven 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].

Recommendations

• Theory and Applications of Satisfiability Testing
• Resolvability vs. almost resolvability
• The complexity of resolution refinements
• On resolvability and extraresolvability
• Improved pebbling bounds
• scientific article; zbMATH DE number 1223618
• The Complexity of Graph Pebbling
• Completeness of resolution revisited
• Pebbling in Hypercubes
• A note on resolvability

Cited in

(9)

• Static-memory-hard functions, and modeling the cost of space vs. time
• Reversible pebble games and the relation between tree-like and general resolution space
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Pebble games, proof complexity, and time-space trade-offs
• Cumulative space in black-white pebbling and resolution
• Nullstellensatz size-degree trade-offs from reversible pebbling
• An Introduction to Lower Bounds on Resolution Proof Systems
• Theory and Applications of Satisfiability Testing
• Pebble games and algebraic proof systems

This page was built for publication: On the Relative Strength of Pebbling and Resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946664)