Pebble games, proof complexity, and time-space trade-offs

DOI10.2168/LMCS-9(3:15)2013zbMATH Open1285.03070arXiv1307.3913OpenAlexW3101351575MaRDI QIDQ2848360FDOQ2848360

Authors: Jakob Nordstrom 

Publication date: 26 September 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Pebble games were extensively studied in the 1970s and 1980s in a number of different contexts. The last decade has seen a revival of interest in pebble games coming from the field 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. This is a survey of research in proof complexity drawing on results and tools from pebbling, with a focus on proof space lower bounds and trade-offs between proof size and proof space.

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

Recommendations

• On the Relative Strength of Pebbling and Resolution
• On the virtue of succinct proofs
• Cumulative space in black-white pebbling and resolution
• scientific article; zbMATH DE number 4189511
• Theory and Applications of Satisfiability Testing

zbMATH Keywords

survey papercutting planesresolutionproof complexityseparationSAT solvingDPLLPCRpolynomial calculusproof sizepebble gamesCDCLproof space\(k\)-DNF resolutionpebbling formulassize-space trade-offs

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Complexity of proofs (03F20)

Cited In (27)

• Space characterizations of complexity measures and size-space trade-offs in propositional proof systems
• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• A New Pebble Game that Characterizes Parallel Complexity Classes
• Towards an optimal separation of space and length in resolution
• Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
• On semantic cutting planes with very small coefficients
• An Introduction to Lower Bounds on Resolution Proof Systems
• Cumulative space in black-white pebbling and resolution
• A note about \(k\)-DNF resolution
• Total space in resolution
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Pebble games and subroutines in least fixed point logic
• Generalising unit-refutation completeness and SLUR via nested input resolution
• The relation between polynomial calculus, Sherali-Adams, and sum-of-squares proofs
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Space Complexity in Polynomial Calculus
• Propositional proof complexity
• Supercritical space-width trade-offs for resolution
• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• Computing (and Life) Is All about Tradeoffs
• On space and depth in resolution
• Token Swapping on Trees
• Cliques enumeration and tree-like resolution proofs
• The PSPACE-Completeness of Black-White Pebbling
• Title not available (Why is that?)
• Communication lower bounds via critical block sensitivity
• Time and space complexity of reversible pebbling

This page was built for publication: Pebble games, proof complexity, and time-space trade-offs

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