Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

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
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}},
}