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

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

References

33 Documents citing this article

Mull, Nathan;Pang, Shuo;Razborov, Alexander, 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.

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.

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.

Cambridge University Press eBooks, Frege Systems, pp. 39-63, 2019, 10.1017/9781108242066.004.

2019, Index, Cambridge University Press eBooks, pp. 510-516, 10.1017/9781108242066.026.

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, Beyond EF via the || . . . || Translation, pp. 233-260, 2019, 10.1017/9781108242066.014.

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

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

Cambridge University Press eBooks, Sequent Calculus, pp. 64-80, 2019, 10.1017/9781108242066.005.

Cambridge University Press eBooks, Resolution, pp. 93-114, 2019, 10.1017/9781108242066.007.

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

Cambridge University Press eBooks, Further Proof Systems, pp. 134-162, 2019, 10.1017/9781108242066.009.

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

Cambridge University Press eBooks, The Nature of Proof Complexity, pp. 472-480, 2019, 10.1017/9781108242066.024.

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

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

2019, Preface, Proof Complexity, pp. xiii-xiv, 10.1017/9781108242066.001.

Cambridge University Press eBooks, Fd and Logical Restrictions, pp. 306-336, 2019, 10.1017/9781108242066.017.

Cambridge University Press eBooks, Model Theory and Lower Bounds, pp. 442-455, 2019, 10.1017/9781108242066.022.

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

Cambridge University Press eBooks, Algebraic and Geometric Proof Systems, pp. 337-352, 2019, 10.1017/9781108242066.018.

Cambridge University Press eBooks, Hard Tautologies, pp. 413-441, 2019, 10.1017/9781108242066.021.

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

Cambridge University Press eBooks, Optimality, pp. 456-471, 2019, 10.1017/9781108242066.023.

Cambridge University Press eBooks, Introduction, pp. 1-8, 2019, 10.1017/9781108242066.002.

Cambridge University Press eBooks, Feasible Interpolation: A Framework, pp. 353-383, 2019, 10.1017/9781108242066.019.

Cambridge University Press eBooks, Feasible Interpolation: Applications, pp. 384-410, 2019, 10.1017/9781108242066.020.

Cambridge University Press eBooks, R and R-Like Proof Systems, pp. 263-295, 2019, 10.1017/9781108242066.015.

Cambridge University Press eBooks, Concepts and Problems, pp. 11-38, 2019, 10.1017/9781108242066.003.

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 1076 times.

This article's PDF has been downloaded 410 times.