Conference article and Preprint:

    Maria Luisa Bonet and Samuel R. Buss
    "An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)"
    To appear in Theory and Applications of Satisfiability Testing (SAT), 2012..

Both the extended abstract and the full preprint version of the paper are available here.

    Download conference version (extended abstract): PDF.

    Download full version of paper (preprint): PDF.

Abstract:  We prove that the graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations using only input lemmas as learned clauses and without degenerate resolution inferences. These graph tautology principles can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search.

Revised slides from related talk:

   An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
   Workshop on Proof Complexity
   BIRS, Banff, Canada
   October 5, 2011

  Download slides: PDF.

Back to Sam Buss's publications page.