DPLL (алгоритм Дэвиса — Патнема — Логемана — Лавленда) — полный алгоритм поиска с возвратом для решения задачи CNF-SAT — определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме.
Опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, Джорджем Логеманом и Дональдом Лавлендом как усовершенствование более раннего алгоритма Дэвиса — Патнема, основанного на правиле резолюций.
Является высокоэффективным алгоритмом и спустя полвека сохраняет актуальность и используется в большинстве решателей для SAT и системах автоматического доказательства для фрагментов логики первого порядка[1].
Задача выполнимости булевых формул важна как с теоретической, так и с практической точек зрения. В теории сложности это первая задача, для которой было доказана принадлежность классу NP-полных задач. Также она может появляться в самых различных практических приложений, например проверка моделей, составление расписаний, диагностика.
Данное направление было и до сих пор является развивающейся областью исследований, ежегодно проводятся соревнования между различными решателями SAT[2]; современные реализации алгоритма DPLL, такие как Chaff, zChaff[3][4], GRASP и Minisat[5], занимают первые места на таких соревнованиях.
Другой тип приложений, в которых часто используется DPLL — это системы автоматического доказательства теорем.