Overcoming Resolution-Based Lower Bounds for SAT Solvers.
DoRon B. Motter, Igor L. Markov · 2002
Many leading-edge SAT solvers are based on the Davis-Putnam procedure or the Davis-Logemann-Loveland procedure, and thus on unsatisfiable instances they can be viewed as attempting to find refutations by resolution. Therefore, exponential lower bounds on the length of resolution proofs also apply to such solvers. Empirical performance of DLL-based solvers on SAT instances from the pigeonhole and Urquhart family are consistent with this expectation.