Maria Luisa Bonet, Samuel R. Buss, and Jan Johannsen
    "Improved Separations of Regular Resolution from Clause Learning Proof Systems"
    Journal of Artificial Intelligence Research 49 (2014) 669-703.

    Download article: PDF.

Abstract:  This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. This holds even if the CDCL search is required to greedily process conflicts arising from unit propagation. This refutes the conjecture that the guarded graph tautology clauses or the guarded xor-ified pebbling tautology clauses can be used to separate CDCL without restarts from general resolution. Together with subsequent results by Buss and Kołodziejczyk, this means we lack any good conjectures about how to establish the exact logical strength of conflict-driven clause learning without restarts.

This article is based in part on an earlier conference paper: M.L. Bonet and S. Buss, An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. In Theory and Applications of Satisfiability Testing (SAT 2012), Springer-Verlag Lecture Notes in Computer Science 7317, pp. 44-57, 2012.

Back to Sam Buss's publications page.