Pebble Games, Proof Complexity, and Time-Space Trade-offs

Jakob Nordstrom

doi:10.2168/LMCS-9(3:15)2013

Jakob Nordstrom - Pebble Games, Proof Complexity, and Time-Space Trade-offs

lmcs:1111 - Logical Methods in Computer Science, September 13, 2013, Volume 9, Issue 3 - https://doi.org/10.2168/LMCS-9(3:15)2013

Pebble Games, Proof Complexity, and Time-Space Trade-offsArticle

Authors: Jakob Nordstrom

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.

https://doi.org/10.2168/LMCS-9(3:15)2013

Source: arXiv.org:1307.3913

Volume: Volume 9, Issue 3

Published on: September 13, 2013

Imported on: March 30, 2010

Keywords: Computer Science - Computational Complexity,Computer Science - Discrete Mathematics,Computer Science - Logic in Computer Science,Mathematics - Combinatorics,Mathematics - Logic

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Understanding the Hardness of Theorem Proving; Funder: European Commission; Code: 279611

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

56 Documents citing this article

Nathan Mull;Shuo Pang;Alexander Razborov, 2022, On CDCL-Based Proof Systems with the Ordered Decision Strategy, arXiv (Cornell University), 51, 4, pp. 1368-1399, 10.1137/20m1362528, http://arxiv.org/abs/1909.04135.

Jo Devriendt;Ambros Gleixner;Jakob Nordström, 2021, Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search, Constraints, 26, 1-4, pp. 26-55, 10.1007/s10601-020-09318-x, https://doi.org/10.1007/s10601-020-09318-x.

Susanna F. De Rezende;Or Meir;Jakob Nordström;Robert Robere, 2021, Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling, Leibniz-Zentrum für Informatik (Schloss Dagstuhl), 30, 1, 10.1007/s00037-020-00201-y, https://drops.dagstuhl.de/opus/volltexte/2019/10840/.

Christoph Berkholz;Jakob Nordström, 2020, Supercritical Space-Width Trade-offs for Resolution, Leibniz-Zentrum für Informatik (Schloss Dagstuhl), 49, 1, pp. 98-118, 10.1137/16m1109072, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.57.

Dmitry Chistikov;Mikhail Vyalyi, Warwick Research Archive Portal (University of Warwick), Re-pairing brackets, 4, pp. 312-326, 2020, Saarbrücken Germany, 10.1145/3373718.3394752, http://wrap.warwick.ac.uk/137788/1/WRAP-re-pairing-brackets-Chistikov-2020.pdf.

Ian D. Kivlichan;Craig Gidney;Dominic W. Berry;Nathan Wiebe;Jarrod McClean;et al., 2020, Improved Fault-Tolerant Quantum Simulation of Condensed-Phase Correlated Electrons via Trotterization, Quantum, 4, pp. 296, 10.22331/q-2020-07-16-296, https://doi.org/10.22331/q-2020-07-16-296.

Florent Capelli, arXiv (Cornell University), Knowledge Compilation Languages as Proof Systems, pp. 90-99, 2019, 10.1007/978-3-030-24258-9_6, https://arxiv.org/abs/1903.04039.

Jan Krajíček, Cambridge University Press eBooks, Resolution, pp. 93-114, 2019, 10.1017/9781108242066.007.

Jan Krajíček, Cambridge University Press eBooks, LKd+1/2 and Combinatorial Restrictions, pp. 296-305, 2019, 10.1017/9781108242066.016.

Jan Krajíček, Cambridge University Press eBooks, Further Proof Systems, pp. 134-162, 2019, 10.1017/9781108242066.009.

Jan Krajíček, Cambridge University Press eBooks, Bibliography, pp. 481-505, 2019, 10.1017/9781108242066.025.

Jan Krajíček, 2019, Index, Cambridge University Press eBooks, pp. 510-516, 10.1017/9781108242066.026.

Jan Krajíček, Cambridge University Press eBooks, The Nature of Proof Complexity, pp. 472-480, 2019, 10.1017/9781108242066.024.

Jan Krajíček, Cambridge University Press eBooks, Basic Example of the Correspondence between Theories and Proof Systems, pp. 165-184, 2019, 10.1017/9781108242066.010.

Jan Krajíček, Cambridge University Press eBooks, Quantified Propositional Calculus, pp. 81-92, 2019, 10.1017/9781108242066.006.

Jan Krajíček, Cambridge University Press eBooks, Feasible Interpolation: A Framework, pp. 353-383, 2019, 10.1017/9781108242066.019.

Jan Krajíček, Cambridge University Press eBooks, Up to EF via the 〈. . .〉 Translation, pp. 197-210, 2019, 10.1017/9781108242066.012.

Jan Krajíček, Cambridge University Press eBooks, Introduction, pp. 1-8, 2019, 10.1017/9781108242066.002.

Jan Krajíček, Cambridge University Press eBooks, Optimality, pp. 456-471, 2019, 10.1017/9781108242066.023.

Jan Krajíček, Cambridge University Press eBooks, Algebraic and Geometric Proof Systems, pp. 115-133, 2019, 10.1017/9781108242066.008.

Jan Krajíček, Cambridge University Press eBooks, Hard Tautologies, pp. 413-441, 2019, 10.1017/9781108242066.021.

Jan Krajíček, Cambridge University Press eBooks, The Two Worlds of Bounded Arithmetic, pp. 185-196, 2019, 10.1017/9781108242066.011.

Jan Krajíček, Cambridge University Press eBooks, Beyond EF via the || . . . || Translation, pp. 233-260, 2019, 10.1017/9781108242066.014.

Jan Krajíček, Cambridge University Press eBooks, Examples of Upper Bounds and p-Simulations, pp. 211-232, 2019, 10.1017/9781108242066.013.

Jan Krajíček, Cambridge University Press eBooks, Model Theory and Lower Bounds, pp. 442-455, 2019, 10.1017/9781108242066.022.

Jan Krajíček, Cambridge University Press eBooks, Fd and Logical Restrictions, pp. 306-336, 2019, 10.1017/9781108242066.017.

Jan Krajíček, 2019, Preface, Proof Complexity, pp. xiii-xiv, 10.1017/9781108242066.001.

Jan Krajíček, Cambridge University Press eBooks, Frege Systems, pp. 39-63, 2019, 10.1017/9781108242066.004.

Jan Krajíček, Cambridge University Press eBooks, Feasible Interpolation: Applications, pp. 384-410, 2019, 10.1017/9781108242066.020.

Jan Krajíček, Cambridge University Press eBooks, Algebraic and Geometric Proof Systems, pp. 337-352, 2019, 10.1017/9781108242066.018.

Jan Krajíček, Cambridge University Press eBooks, R and R-Like Proof Systems, pp. 263-295, 2019, 10.1017/9781108242066.015.

Jan Krajíček, Cambridge University Press eBooks, Concepts and Problems, pp. 11-38, 2019, 10.1017/9781108242066.003.

Jan Krajíček, Cambridge University Press eBooks, Sequent Calculus, pp. 64-80, 2019, 10.1017/9781108242066.005.

Jan Krajíček, 2019, Proof Complexity, 10.1017/9781108242066.

Marc Vinyals;Jan Elffers;Jesús Giráldez-Cru;Stephan Gocht;Jakob Nordström, Lecture notes in computer science, In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving, pp. 292-310, 2018, 10.1007/978-3-319-94144-8_18.

Massimo Lauria, 2018, A note about k -DNF resolution, Information Processing Letters, 137, pp. 33-39, 10.1016/j.ipl.2018.04.014.

Massimo Lauria, 2018, Cliques enumeration and tree-like resolution proofs, Information Processing Letters, 135, pp. 62-67, 10.1016/j.ipl.2018.03.001.

Massimo Lauria;Neil Thapen, 2018, On semantic cutting planes with very small coefficients, Information Processing Letters, 136, pp. 70-75, 10.1016/j.ipl.2018.04.007.

Mika Göös;Toniann Pitassi, 2018, Communication Lower Bounds via Critical Block Sensitivity, arXiv (Cornell University), 47, 5, pp. 1778-1806, 10.1137/16m1082007, http://arxiv.org/abs/1311.2355.

Alexander Razborov, 2017, On Space and Depth in Resolution, Computational Complexity, 27, 3, pp. 511-559, 10.1007/s00037-017-0163-1.

Alexander Razborov, 2017, On the Width of Semialgebraic Proofs and Algorithms, Mathematics of Operations Research, 42, 4, pp. 1106-1134, 10.1287/moor.2016.0840.

Olaf Beyersdorff;Leroy Chew;Meena Mahajan;Anil Shukla, 2017, Are Short Proofs Narrow? QBF Resolution Is Not So Simple, White Rose Research Online (University of Leeds), 19, 1, pp. 1-26, 10.1145/3157053, http://eprints.whiterose.ac.uk/123219/1/width-full-journal-final.pdf.

Alexander Razborov, 2016, Guest Column, ACM SIGACT News, 47, 2, pp. 66-86, 10.1145/2951860.2951875.

Alexander Razborov, 2016, A New Kind of Tradeoffs in Propositional Proof Complexity, Journal of the ACM, 63, 2, pp. 1-14, 10.1145/2858790.

Christoph Berkholz;Jakob Nordström, arXiv (Cornell University), Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps, 242, pp. 267-276, 2016, New York NY USA, 10.1145/2933575.2934560, https://arxiv.org/abs/1608.08704.

Ilario Bonacina;Nicola Galesi;Neil Thapen, 2016, Total Space in Resolution, SIAM Journal on Computing, 45, 5, pp. 1894-1909, 10.1137/15m1023269.

Kazuhisa SETO, 2015, An Introduction to Lower Bounds on Resolution Proof Systems, Interdisciplinary Information Sciences, 21, 4, pp. 307-328, 10.4036/iis.2015.l.02, https://doi.org/10.4036/iis.2015.l.02.

Siu Man Chan;Massimo Lauria;Jakob Nordstrom;Marc Vinyals, arXiv (Cornell University), Hardness of Approximation in PSPACE and Separation Results for Pebble Games, 2015, Berkeley, CA, USA, 10.1109/focs.2015.36, https://arxiv.org/abs/2305.19104.

Yuval Filmus;Massimo Lauria;Jakob Nordström;Noga Ron-Zewi;Neil Thapen, 2015, Space Complexity in Polynomial Calculus, IRIS Research product catalog (Sapienza University of Rome), 44, 4, pp. 1119-1153, 10.1137/120895950, https://hdl.handle.net/11573/957543.

Jakob Nordström, Lecture notes in computer science, A (Biased) Proof Complexity Survey for SAT Practitioners, pp. 1-6, 2014, 10.1007/978-3-319-09284-3_1.

Mika Göös;Toniann Pitassi, arXiv (Cornell University), Communication lower bounds via critical block sensitivity, pp. 847-856, 2014, New York New York, 10.1145/2591796.2591838.

Mladen Mikša;Jakob Nordström, CiteSeer X (The Pennsylvania State University), Long Proofs of (Seemingly) Simple Formulas, pp. 121-137, 2014, 10.1007/978-3-319-09284-3_10, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.588.4626.

Olaf Beyersdorff;Oliver Kullmann, Cronfa (Swansea University), Unified Characterisations of Resolution Hardness Measures, pp. 170-187, 2014, 10.1007/978-3-319-09284-3_13, https://cronfa.swan.ac.uk/Record/cronfa18004/Download/0018004-15052015115552.pdf.

Allan Borodin, Lecture notes in computer science, Computing (and Life) Is All about Tradeoffs, pp. 112-132, 2013, 10.1007/978-3-642-40273-9_9.

Matthew Gwynne;Oliver Kullmann, 2013, Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution, arXiv (Cornell University), 52, 1, pp. 31-65, 10.1007/s10817-013-9275-8, http://arxiv.org/abs/1204.6529.

Matti Järvisalo;Arie Matsliah;Jakob Nordström;Stanislav Živný, CiteSeer X (The Pennsylvania State University), Relating Proof Complexity Measures and Practical Hardness of SAT, pp. 316-331, 2012, 10.1007/978-3-642-33558-7_25, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.257.7494.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2871 times.

This article's PDF has been downloaded 712 times.