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

Bibliographic References

33 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.

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

Chunxiao Li;Noah Fleming;Marc Vinyals;Toniann Pitassi;Vijay Ganesh, Lecture notes in computer science, Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers, pp. 233-249, 2020, 10.1007/978-3-030-51825-7_17, https://doi.org/10.1007/978-3-030-51825-7_17.

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

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

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1166 times.

This article's PDF has been downloaded 426 times.