Small Stone in Pool

Samuel R. Buss; Leszek Aleksander Kolodziejczyk

doi:10.2168/LMCS-10(2:16)2014

Samuel R. Buss ; Leszek Aleksander Kolodziejczyk - Small Stone in Pool

lmcs:852 - Logical Methods in Computer Science, June 27, 2014, Volume 10, Issue 2 - https://doi.org/10.2168/LMCS-10(2:16)2014

Small Stone in PoolArticle

Authors: Samuel R. Buss ; Leszek Aleksander Kolodziejczyk

The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas (regRTI).
Therefore, the Stone tautologies do not separate resolution from DPLL with clause learning.

https://doi.org/10.2168/LMCS-10(2:16)2014

Source: arXiv.org:1405.5626

Volume: Volume 10, Issue 2

Published on: June 27, 2014

Imported on: October 31, 2012

Keywords: Computer Science - Logic in Computer Science, Mathematics - Logic

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

Funding:

Source : OpenAIRE Graph

Complexity of proofs, proof search, and algorithmic complexity; Funder: National Science Foundation; Code: 1101228
AF: Large: Collaborative Research: Exploiting Duality between Meta-Algorithms and Complexity; Funder: National Science Foundation; Code: 1213151

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

32 Documents citing this article

Joshua Blinkhorn;Tomáš Peitl;Friedrich Slivovsky, 2021, Davis and Putnam Meet Henkin: Solving DQBF with Resolution, Lecture notes in computer science, pp. 30-46, 10.1007/978-3-030-80223-3_4.

Chunxiao Li;Noah Fleming;Marc Vinyals;Toniann Pitassi;Vijay Ganesh, 2020, Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers, PubMed Central, pp. 233-249, 10.1007/978-3-030-51825-7_17, https://www.ncbi.nlm.nih.gov/pmc/articles/7326553.

Marc Vinyals, 2020, Hard Examples for Common Variable Decision Heuristics, Proceedings of the AAAI Conference on Artificial Intelligence, 34, 02, pp. 1652-1659, 10.1609/aaai.v34i02.5527, https://doi.org/10.1609/aaai.v34i02.5527.

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, Bibliography, Cambridge University Press eBooks, pp. 481-505, 10.1017/9781108242066.025.

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.

Paul Beame;Vincent Liew, 2019, Toward Verifying Nonlinear Integer Arithmetic, Journal of the ACM, 66, 3, pp. 1-30, 10.1145/3319396.

Jia Hui Liang;Chanseok Oh;Minu Mathew;Ciza Thomas;Chunxiao Li;et al., 2018, Machine Learning-Based Restart Policy for CDCL SAT Solvers, Lecture notes in computer science, pp. 94-110, 10.1007/978-3-319-94144-8_6.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2909 times.

This article's PDF has been downloaded 561 times.