Abstract
The effectiveness of the CDCL algorithm, the most used to solve SAT in practice, is complicated to understand, and so far one of the most successful tools for that has been proof complexity. CDCL is easily seen to be limited by the resolution proof system, and furthermore it was shown to be equivalent to resolution, in the sense that CDCL can reproduce a given resolution proof with only polynomial overhead. But the question of the power of CDCL with respect to resolution is far from closed. To begin with, the previous equivalence is subject to some assumptions, only some of which are reasonable in practice. In addition, in a world where algorithms are expected to run in linear time, a polynomial overhead is too coarse a measure. In this talk we will discuss what breaks when we try to make the assumptions more realistic, and how much of an overhead CDCL needs in order to simulate resolution.