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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.