Samuel R. Buss and Leszek Kołodziejczyk
    "Small Stone in Pool"
    Logical Methods of Computer Science 10, 2 (2014) paper 16
    DOI: 10.2168/LMCS-10(2:16)2014.

    Download preprint version: PDF.

Abstract:  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.

Back to Sam Buss's publications page.