Введение
Тип алгоритма поиска
В логике и информатике алгоритм Дэвиса–Путнама–Логеманна–Лавленда (DPLL) — это полный алгоритм поиска с возвратом для определения выполнимости формул логики высказываний в конъюнктивной нормальной форме, то есть для решения задачи CNF SAT. Он был представлен в 1961 году Мартином Дэвисом, Джорджем Логеманном и Дональдом В. Лавлендом и является усовершенствованием более раннего алгоритма Дэвиса–Путнама, который представляет собой процедуру, основанную на разрешении, разработанную Дэвисом и Хилари Путнамом в 1960 году. Особенно в более ранних публикациях алгоритм Дэвиса–Логеманна–Лавленда часто называют «методом Дэвиса–Путнама» или «алгоритмом DP». Другие распространенные названия, сохраняющие это различие, — DLL и DPLL.
Реализация и применение
Проблема SAT важна как с теоретической, так и с практической точек зрения. В теории сложности она стала первой проблемой, доказанной NP-полной, и находит применение в самых разных областях, таких как проверка моделей, автоматическое планирование и составление расписаний, а также диагностика в искусственном интеллекте. Поэтому разработка эффективных решателей SAT является предметом исследований на протяжении многих лет. GRASP (1996–1999) была одной из первых реализаций, использующих алгоритм DPLL, а MiniSat занимала первые места на соревнованиях в 2004 и 2005 годах. Другой областью применения, часто использующей DPLL, является автоматическое доказательство теорем или проверка выполнимости с учетом теорий (SMT), которая представляет собой задачу SAT, в которой пропозициональные переменные заменяются формулами из другой математической теории.
Связанные алгоритмы
С 1986 года для решения задач SAT также используются (упорядоченные с уменьшением размера) бинарные диаграммы решений. В 1989–1990 годах был представлен и запатентован метод проверки формул Stålmarck. Он нашёл некоторое применение в промышленных задачах. Алгоритм DPLL был расширен для автоматического доказательства теорем для фрагментов логики первого порядка посредством алгоритма DPLL(T). В 2010–2019 годах работы по улучшению алгоритма позволили разработать более эффективные стратегии выбора переменных для ветвления и новые структуры данных для повышения скорости работы алгоритма, особенно в части распространения единичных литералов. Однако основным улучшением стал более мощный алгоритм – обучение на основе анализа конфликтов (CDCL), который аналогичен DPLL, но после возникновения конфликта "выявляет" его первопричины (значения переменных, приведшие к конфликту) и использует эту информацию для выполнения нехронологического возврата (также известного как "скачок назад") с целью избежать повторного возникновения того же конфликта. По состоянию на 2019 год большинство современных решателей SAT основаны на фреймворке CDCL.
Связь с другими понятиями
Выполнение алгоритмов на основе DPLL на неудовлетворимых экземплярах соответствует доказательствам опровержения методом резолюций в виде дерева.