DPLL алгоритм
З Вікіпедії, безкоштовно encyclopedia
Алгоритм Девіса-Патнема-Логемана-Лавленд — це повний алгоритм пошуку з поверненням для визначення здійсненності булевих формул, записаних в кон'юнктивній нормальній формі (КНФ) для вирішення завдання CNF-SAT[1].
![Thumb image](http://upload.wikimedia.org/wikipedia/commons/0/07/Poshuk1.png)
Алгоритм був опублікований в 1962 році Мартіном Девісом, Гіларі Патнемом, Джорджем Логеманом й Дональдом Лавленд та є удосконаленням більш раннього алгоритму Девіса-Патнема, методу, заснованого на правилі резолюцій, розробленого Девісом та Патнемом в 1960 році.
DPLL — високо-ефективний алгоритм якому вже 50 років але все ще лежить в основі більшості ефективних вирішувачів для SAT, а також для систем автоматичного доведення теорем та фрагментів логіки першого порядку.