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

DOI10.2168/LMCS-9(3:15)2013MaRDI QIDQ2848360zbMATH OpenOpenAlexFDO

Authors Jakob Nordstrom

Publication date 26 September 2013

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

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

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)

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.

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

Cited in

(28)

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

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)