DPLL

DPLL (алгоритм Дэвиса — Патнема — Логемана — Лавленда) — полный алгоритм поиска с возвратом для решения задачи CNF-SAT — определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме.

Опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, Джорджем Логеманом^[англ.] и Дональдом Лавлендом^[англ.] как усовершенствование более раннего алгоритма Дэвиса — Патнема, основанного на правиле резолюций.

Является высокоэффективным алгоритмом и спустя полвека сохраняет актуальность и используется в большинстве решателей для SAT и системах автоматического доказательства для фрагментов логики первого порядка^[1].

1. ↑ Nieuwenhuis, Robert; Oliveras, Albert; Tinelly, Cesar (2004), "Abstract DPLL and Abstract DPLL Modulo Theories" (PDF), Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings: 36—50, Архивировано (PDF) 17 ноября 2011, Дата обращения: 26 января 2012 {{citation}}: Неизвестный параметр |urltype= игнорируется (справка) Источник  (неопр.). Дата обращения: 26 января 2012. Архивировано 17 ноября 2011 года.