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

Secondary volumes: Selected Papers of the 23rd International Workshop on Computer Science Logic and the 18th Annual Conference of the EACSL (CSL 2009)

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

58 Documents citing this article

Shuichi Hirahara;Naoto Ohsaka, 2024, Probabilistically Checkable Reconfiguration Proofs and Inapproximability of Reconfiguration Problems, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, pp. 1435-1445, 10.1145/3618260.3649667.

Zhijie Lyu;Anurag Purwar, 2024, Point-Based Models: A Unified Approach for Geometric Constraint Analysis of Planar n -Bar Mechanisms With Rotary, Sliding, and Rolling Joints, Journal of Mechanisms and Robotics, 17, 4, 10.1115/1.4066963.

Christoph Berkholz;Jakob Nordström, 2023, Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler–Leman Refinement Steps, Journal of the ACM, 70, 5, pp. 1-32, 10.1145/3195257, https://doi.org/10.1145/3195257.

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, arXiv (Cornell University), 30, 1, 10.1007/s00037-020-00201-y, http://arxiv.org/abs/2001.02481.

Christoph Berkholz;Jakob Nordström, 2020, Supercritical Space-Width Trade-offs for Resolution, arXiv (Cornell University), 49, 1, pp. 98-118, 10.1137/16m1109072, http://arxiv.org/abs/1612.07162.

Dmitry Chistikov;Mikhail Vyalyi, 2020, Re-pairing brackets, arXiv (Cornell University), pp. 312-326, 10.1145/3373718.3394752, http://arxiv.org/abs/1904.08402.

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.

2019, Bibliography, Cambridge University Press eBooks, pp. 481-505, 10.1017/9781108242066.025.

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

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

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

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

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

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

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

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

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

Jan Krajíček, 2019, Proof Complexity, Cambridge University Press eBooks, 10.1017/9781108242066.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Marc Vinyals;Jan Elffers;Jesús Giráldez-Cru;Stephan Gocht;Jakob Nordström, 2018, In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving, Lecture notes in computer science, pp. 292-310, 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, Zenodo (CERN European Organization for Nuclear Research), 135, pp. 62-67, 10.1016/j.ipl.2018.03.001, https://zenodo.org/record/3502481.

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, SIAM Journal on Computing, 47, 5, pp. 1778-1806, 10.1137/16m1082007.

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.

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

Olaf Beyersdorff;Leroy Chew;Meena Mahajan;Anil Shukla, 2017, Are Short Proofs Narrow? QBF Resolution Is Not So Simple, ACM Transactions on Computational Logic, 19, 1, pp. 1-26, 10.1145/3157053, https://doi.org/10.1145/3157053.

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

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

Christoph Berkholz;Jakob Nordström, 2016, Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps, Lund University Publications (Lund University), pp. 267-276, 10.1145/2933575.2934560.

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, 2015, Hardness of Approximation in PSPACE and Separation Results for Pebble Games, IRIS Research product catalog (Sapienza University of Rome), pp. 466-485, 10.1109/focs.2015.36.

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, http://hdl.handle.net/11573/957543.

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

Mika Göös;Toniann Pitassi, 2014, Communication lower bounds via critical block sensitivity, Proceedings of the forty-sixth annual ACM symposium on Theory of computing, pp. 847-856, 10.1145/2591796.2591838.

Mladen Mikša;Jakob Nordström, 2014, Long Proofs of (Seemingly) Simple Formulas, Lecture notes in computer science, pp. 121-137, 10.1007/978-3-319-09284-3_10.

Olaf Beyersdorff;Oliver Kullmann, 2014, Unified Characterisations of Resolution Hardness Measures, Lecture notes in computer science, pp. 170-187, 10.1007/978-3-319-09284-3_13.

Allan Borodin, 2013, Computing (and Life) Is All about Tradeoffs, Lecture notes in computer science, pp. 112-132, 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ý, 2012, Relating Proof Complexity Measures and Practical Hardness of SAT, Lecture notes in computer science, pp. 316-331, 10.1007/978-3-642-33558-7_25.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 5240 times.

This article's PDF has been downloaded 1063 times.