Pebble games, proof complexity, and time-space trade-offs
2013 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, Vol. 9, no 3, 15- p.Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
2013. Vol. 9, no 3, 15- p.
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
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-133371DOI: 10.2168/LMCS-9(3:15)2013ISI: 000327472100012ScopusID: 2-s2.0-84879808088OAI: oai:DiVA.org:kth-133371DiVA: diva2:661655
FunderEU, FP7, Seventh Framework Programme, 279611Swedish Research Council, 621-2010-4797 621-2012-5645
QC 201311042013-11-042013-10-312014-01-09Bibliographically approved