Authors: Samuel R. Buss ; Leszek Aleksander Kolodziejczyk
NULL##NULL
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.
Cambridge University Press eBooks, The Nature of Proof Complexity, pp. 472-480, 2019, 10.1017/9781108242066.024.
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, Feasible Interpolation: A Framework, pp. 353-383, 2019, 10.1017/9781108242066.019.
Cambridge University Press eBooks, Up to EF via the 〈. . .〉 Translation, pp. 197-210, 2019, 10.1017/9781108242066.012.
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.