Pebble games, proof complexity, and time-space trade-offs
(2013) In Logical Methods in Computer Science 9(3).- 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.
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/30ed0341-1557-4110-829e-d630a461cd96
- author
- Nordström, Jakob LU
- publishing date
- 2013-09-13
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- CDCL, Cutting planes, DPLL, k-DNF resolution, Length, PCR, Pebble games, Pebbling formulas, Polynomial calculus, Proof complexity, Resolution, SAT solving, Separation, Space, Trade-off, Width
- in
- Logical Methods in Computer Science
- volume
- 9
- issue
- 3
- article number
- 15
- publisher
- Technischen Universitat Braunschweig
- external identifiers
-
- scopus:84879808088
- ISSN
- 1860-5974
- DOI
- 10.2168/LMCS-9(3:15)2013
- language
- English
- LU publication?
- no
- id
- 30ed0341-1557-4110-829e-d630a461cd96
- date added to LUP
- 2020-12-18 22:26:11
- date last changed
- 2022-03-18 21:50:53
@article{30ed0341-1557-4110-829e-d630a461cd96, abstract = {{<p>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.</p>}}, author = {{Nordström, Jakob}}, issn = {{1860-5974}}, keywords = {{CDCL; Cutting planes; DPLL; k-DNF resolution; Length; PCR; Pebble games; Pebbling formulas; Polynomial calculus; Proof complexity; Resolution; SAT solving; Separation; Space; Trade-off; Width}}, language = {{eng}}, month = {{09}}, number = {{3}}, publisher = {{Technischen Universitat Braunschweig}}, series = {{Logical Methods in Computer Science}}, title = {{Pebble games, proof complexity, and time-space trade-offs}}, url = {{http://dx.doi.org/10.2168/LMCS-9(3:15)2013}}, doi = {{10.2168/LMCS-9(3:15)2013}}, volume = {{9}}, year = {{2013}}, }