It occurred to me that if a given SAT is unsatisfiable, then a DPLL algorithm must try true/false settings for all literals to determine that there does not exist any satisfying literal combination. All newer fast algorithms are enhancements to DPLL and provide only a partial speedup. Does this fact not imply a lower bound for SAT of O(2^n)?
-
$\begingroup$ Nope. The lower bound is only valid for DPLL (or its variant/improvement such as CDCL ; for which we know explicit exponential lower bounds such as pigeon hole principle). It does not rule out the existence of efficient algorithms based on approaches that are completely different. $\endgroup$ – holf Jan 9 at 19:16
-
$\begingroup$ And that's not an accurate description of what DPLL does. The unit rule prunes large parts of the search tree without trying all its assignments. $\endgroup$ – Kyle Jones Jan 12 at 1:39
