the effectiveness of the cdcl algorithm for sat is complicated to understand, and so far one of the most successful tools for its analysis has been proof complexity. cdcl is easily seen to be limited by the resolution proof system, and furthermore can be thought of as being equivalent to resolution, in the sense that cdcl can reproduce a given resolution proof with only a 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 assumptions, only some of which are reasonable. in addition, in a setting where algorithms are expected to run in near-linear time, a polynomial overhead is too coarse a measure.

in this talk we will discuss how exactly cdcl and resolution are equivalent, what breaks when we try to make the assumptions more realistic, and how much of an overhead cdcl needs in order to simulate resolution.