Implementations and Applications
The SAT problem is important both from theorical and practical points of view. In complexity theory it is the first NP-complete proved problem, and can appear in a broad variety of applications such as model checking, automated planning and scheduling, diagnosis in artificial intelligence.
As such, it was and still is a hot topic in research for many years, and competitions between SAT solvers regularly take place. DPLL's modern implementations like Chaff and zChaff, GRASP or Minisat are in the first places of the competitions these last years.
Another application which often involves DPLL is automated theorem proving or Satisfiability Modulo Theories (SMT) which is a SAT problem in which propositional variables are replaced with formulas of another mathematical theory.
Read more about this topic: DPLL Algorithm