It's questionable whether SAT solvers really work well for "the vast majority of the cases". They work very well for the problems they are tasked with. DPLL-bas

It's questionable whether SAT solvers really work well for "the vast majority of the cases". They work very well for the problems they are tasked with. DPLL-based SAT solvers don't work well with randomly generated SAT instances which survey-propagation-based solvers excel on. On SAT-instances that arise in the verification of CPUs the opposite is true. Both approaches break down where SAT instances have more than 10^7 variables, and that's almost all cases. ;) Still, it never ceases to amaze me just how well DPLL-based solvers work on the instances that I feed them, and that despite all the theoretical limitations that we know they have.