Advanced

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

Nordström, Jakob LU (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:
author
publishing date
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
2021-02-17 01:47:14
@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},
  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},
}