Conference article and Preprint:
Maria Luisa Bonet and Samuel R. 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.
Download conference version (extended abstract): 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.
A full version of the paper is also available, containing additional results: M.L. Bonet, S. Buss, and J. Johannsen, Improved Separations of Regular Resolution from Clause Learning Proof Systems.
Revised slides from related talks:
An Improved Separation of Regular Resolution from
Pool Resolution and Clause Learning
Workshop on Proof Complexity
BIRS, Banff, Canada
October 5, 2011
Download BIRS 2011 slides: PDF.
An Improved Separation of Regular Resolution from
Pool Resolution and Clause Learning
Conf. on Theory and Applications of Satisfiability Testing
(SAT 2012)
Trento, Italy
June 17, 2012
Download SAT 2012 slides: PDF.