|
DPLLDPLL (алгоритм Дэвиса — Патнема — Логемана — Лавленда) — полный алгоритм поиска с возвратом для решения задачи CNF-SAT — определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, Джорджем Логеманом[англ.] и Дональдом Лавлендом[англ.] как усовершенствование более раннего алгоритма Дэвиса — Патнема, основанного на правиле резолюций. Является высокоэффективным алгоритмом и спустя полвека сохраняет актуальность и используется в большинстве решателей для SAT и системах автоматического доказательства для фрагментов логики первого порядка[1].  Реализации и приложенияЗадача выполнимости булевых формул важна как с теоретической, так и с практической точек зрения. В теории сложности это первая задача, для которой было доказана принадлежность классу NP-полных задач. Также она может появляться в самых различных практических приложений, например проверка моделей, составление расписаний, диагностика. Данное направление было и до сих пор является развивающейся областью исследований, ежегодно проводятся соревнования между различными решателями SAT[2]; современные реализации алгоритма DPLL, такие как Chaff[англ.], 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));
В этом псевдокоде Алгоритм зависит от выбора «переменной ветвления», то есть переменной, которая выбирается на очередном шаге алгоритма с возвратом. для присвоения ей определённого значения. Таким образом, это не один алгоритм, а целое семейство алгоритмов, по одному на каждый возможный способ выбора «переменных ветвления». Эффективность алгоритма сильно зависит от этого выбора: существуют примеры задач, время работы алгоритма для которых может быть константой или расти экспоненциально, в зависимости от выбора «переменных ветвления». Методы выбора представляют собой эвристические техники и называются также «эвристиками для ветвления» (branching heuristics)[6]. Современные исследованияТекущие исследования по улучшению алгоритма выполняются в трех направлениях: определению различных оптимизирующих методов выбора «переменной ветвления»; разработка новых структур данных для ускорения работы алгоритма, особенно для распространения переменной; и разработка различных вариантов базового алгоритма перебора с возвратом. Последнее направление включает «нехронологические возвраты» и запоминание плохих случаев. Эти улучшения можно описать как метод возврата после достижения ложной дизъюнкты, при котором запоминается, какое именно присвоение значения переменной повлекло этот результат, чтобы в дальнейшем избежать точно такой же последовательности вычислений, тем самым сократив время работы. Более новый алгоритм — метод Сталмарка — известен с 1990 года. Также с 1986 года для решения задачи SAT используются диаграммы решений. На основе DPLL-алгоритма в середине 1990-х был создан и стал широко применяться CDCL-алгоритм. Примечания
Литература
|
