On Proof Systems Behind Efficient SAT Solvers
DoRon B. Motter, Ann Arbor · 2002
Conventional algorithms for Boolean satisfiability (SAT) work within the framework of resolution as a proof system. However it has been known since the 1980s that every resolution proof of the pigeonhole principle (PHP n ), suitably encoded as a CNF instance, includes exponentially many steps[4]. Therefore SAT solvers based upon the DLL procedure [1] or the DP procedure [2] must take exponential time. Polynomial-sized proofs of the PHP exist for more powerful proof systems, but general-purpose SAT solvers often remain confined to resolution.