Алгоритм Дэвиса-Патнема-Логемана-Лавленда (DPLL) — это полный алгоритм поиска с возвратом для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме, то есть для решения задачи CNF-SAT.
Алгоритм был опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, Джорджем Логеманом и Дональдом Лавлендом и представлял собой усовершенствование более раннего алгоритма Дэвиса-Патнема, метода, основанного на правиле резолюций, разработанного Дэвисом и Патнемом в 1960 году.
DPLL является высоко-эффективным алгоритмом и спустя 50 лет все ещё представляет собой основу для большинства эффективных решателей для SAT, а также для систем автоматического доказательства теорем для фрагментов логики первого порядка.[1]
Задача выполнимости булевых формул важна как с теоретической, так и с практической точек зрения. В теории сложности это первая задача, для которой было доказана принадлежность классу NP-полных задач. Также она может появляться в самых различных практических приложений, например проверка моделей, составление расписаний, диагностика.
Данное направление было и до сих пор является развивающейся областью исследований, ежегодно проводятся соревнования между различными решателями SAT.[2] Современные реализации алгоритма DPLL, такие как Chaff and zChaff[3][4], GRASP или Minisat[5] оказываются в числе первых мест в течение последних лет.
Другой тип приложений, в которых часто используется DPLL — это системы автоматического доказательства теорем.
Основной алгоритм с возвратом начинается с выбора переменной, присвоения ей значения «истина», упрощения формулы и затем рекурсивным образом проверки упрощенной формулы на выполнимость; если она выполнима, то исходная формула тоже выполнима; иначе, процедура повторяется, но выбранной переменной задается значение «ложь». Этот подход называется «правилом разбиения», так как он разбивает задачу на две более простые подзадачи. Шаг упрощения заключается в том, что из формулы удаляются все дизъюнкты, которые становятся истинными после присвоения выбранной переменной значения «истина» и удаления из оставшихся дизъюнкт всех вхождений этой переменной, которые становятся ложными.
Алгоритм DPLL позволяет улучшить основной алгоритм с возвратом за счет использования следующих правил на каждом шаге:
Невыполнимость при данных конкретных значениях переменных определяется, когда одна из дизъюнкт становится «пустой», то есть всем её переменным задаются значения таким образом, что их вхождения (с отрицанием или без него) становятся ложными. Выполнимость формулы констатируется или когда всем переменным заданы значения так, что не возникает «пустых» дизъюнкт, или, в современных реализациях, если все дизъюнкты равны истине. Невыполнимость всей формулы может быть установлена только после окончания исчерпывающего перебора.
Алгоритм DPLL может быть выражен с помощью следующего псевдокода, где знаком Φ обозначена формула в конъюнктивной нормальной форме:
Входные данные: Набор дизъюнкт формулы Φ. Выходные данные: Значение истинности
function DPLL(Φ) если Φ - это набор выполняющихся дизъюнкт тогда return true; если Φ содержит пустую дизъюнкту then return false; для каждой дизъюнкты из одной переменной l в Φ Φ unit-propagate(l, Φ); для каждой переменной l которая встречается в чистом виде в Φ Φ pure-literal-assign(l, Φ); l choose-literal(Φ); return DPLL(Φ&l) or DPLL(Φ¬(l));
В этом псевдокоде unit-propagate(l, Φ)
и pure-literal-assign(l, Φ)
— это функции, которые возвращают результат применения к переменной l
и формуле Φ
распространения переменной и правила исключения «чистой переменной» соответственно. Другими словами, они заменяют каждое вхождение переменной l
значением «истина» и каждое вхождение переменной с отрицанием not l
значением «ложь» в формуле Φ
, а затем упрощают получившуюся формулу. Приведенный псевдокод возвращает только ответ — выполняет ли формулу последний из присвоенных наборов значений. В современных реализациях частичные выполняющие наборы тоже возвращаются в случае успеха.
Алгоритм зависит от выбора «переменной ветвления», то есть переменной, которая выбирается на очередном шаге алгоритма с возвратом. для присвоения ей определённого значения. Таким образом, это не один алгоритм, а целое семейство алгоритмов, по одному на каждый возможный способ выбора «переменных ветвления». Эффективность алгоритма сильно зависит от этого выбора: существуют примеры задач, время работы алгоритма для которых может быть константой или расти экспоненциально, в зависимости от выбора «переменных ветвления». Методы выбора представляют собой эвристические техники и называются также «эвристиками для ветвления» (branching heuristics)[6].
Текущие исследования по улучшению алгоритма выполняются в трех направлениях: определению различных оптимизирующих методов выбора «переменной ветвления»; разработка новых структур данных для ускорения работы алгоритма, особенно для распространения переменной; и разработка различных вариантов базового алгоритма перебора с возвратом. Последнее направление включает «нехронологические возвраты» и запоминание плохих случаев. Эти улучшения можно описать как метод возврата после достижения ложной дизъюнкты, при котором запоминается, какое именно присвоение значения переменной повлекло этот результат, чтобы в дальнейшем избежать точно такой же последовательности вычислений, тем самым сократив время работы.
Более новый алгоритм — метод Сталмарка — известен с 1990 года. Также с 1986 года для решения задачи SAT используются диаграммы решений.
На основе DPLL-алгоритма в середине 1990-х был создан и стал широко применяться CDCL-алгоритм.
|doi=
(справка на английском).|coauthors=
(справка)|coauthors=
(справка)Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .