DPLL-Алгоритм

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

Алгоритм был опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, Джорджем Логеманом и Дональдом Лавлендом и представлял собой усовершенствование более раннего алгоритма Дэвиса-Патнема, метода, основанного на правиле резолюций, разработанного Дэвисом и Патнемом в 1960 году.

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

Алгоритм поиска с возвратом.

Реализации и приложения

Задача выполнимости булевых формул важна как с теоретической, так и с практической точек зрения. В теории сложности это первая задача, для которой было доказана принадлежность классу NP-полных задач. Также она может появляться в самых различных практических приложений, например проверка моделей, составление расписаний, диагностика.

Данное направление было и до сих пор является развивающейся областью исследований, ежегодно проводятся соревнования между различными решателями SAT.^[2] Современные реализации алгоритма DPLL, такие как Chaff and zChaff^[3][4], GRASP или Minisat^[5] оказываются в числе первых мест в течение последних лет.

Другой тип приложений, в которых часто используется DPLL - это системы автоматического доказательства теорем.

Описание алгоритма

Основной алгоритм с возвратом начинается с выбора переменной, присвоения ей значения "истина", упрощения формулы и затем рекурсивным образом проверки упрощенной формулы на выполнимость; если она выполнима, то исходная формула тоже выполнима; иначе, процедура повторяется, но выбранной переменной задается значение "ложь". Этот подход называется "правилом разбиения", так как он разбивает задачу на две более простые подзадачи. Шаг упрощения заключается в том, что из формулы удаляются все дизъюнкты, которые становятся истинными после присвоения выбранной переменной значения "истина" и удаления из оставшихся дизъюнкт всех вхождений этой переменной, которые становятся ложными.

Алгоритм DPLL позволяет улучшить основной алгоритм с возвратом за счет использования следующих правил на каждом шаге:

Распространение переменной 

Если дизъюнкта содержит ровно одну переменную, которой еще не задали значение, эта дизъюнкта может принять значение "истина" только в случае присвоения переменной значения, которое сделает ее истинной ("истина", если переменная входит в дизъюнкту без отрицания, и "ложь", если переменная с отрицанием) (см. en:Unit propagation). Таким образом, не нужно делать выбор на данном шаге. На практике за этим следует каскад присвоений переменным значений, таким образом существенно сокращается количество вариантов перебора.

Исключение "чистых" переменных 

Если некоторая переменная входит в формулу только с одной "полярностью" (т.е. либо только без отрицаний, либо только с отрицаниями), она называется чистой. "Чистым" переменным всегда можно задать значение так, что все содержащие их дизъюнкты станут истинными. Таким образом, эти дизъюнкты не будут влиять на пространство вариантов, и их можно удалить.

Невыполнимость при данных конкретных значениях переменных определяется, когда одна из дизъюнкт становится "пустой", т.е. всем ее переменным задаются значения таким образом, что их вхождения (с отрицанием или без него) становятся ложными. Выполнимость формулы констатируется или когда всем переменным заданы значения так, что не возникает "пустых" дизъюнкт, или, в современных реализациях, если все дизъюнкты равны истине. Невыполнимость всей формулы может быть установлена только после окончания исчерпывающего перебора.

Алгоритм DPLL может быть выражен с помощью следующего псевдокода, где знаком Φ обозначена формула в конъюнктивной нормальной форме:

  Входные данные: Набор дизъюнкт формулы Φ.
  Выходные данные: Значение истинности

function DPLL(Φ)
   если Φ - это набор выполняющихся дизъюнкт
       тогда return true;
   если Φ содержит пустую дизъюнкту
       then return false;
   для каждой дизъюнкты из одной переменной l в Φ
      Φ $\leftarrow$ unit-propagate(l, Φ);
   для каждой переменной l которая встречается в чистом виде в Φ
      Φ $\leftarrow$ pure-literal-assign(l, Φ);
   l $\leftarrow$ choose-literal(Φ);
   return DPLL(Φ&l) or DPLL(Φ&not(l));

В этом псевдокоде unit-propagate(l, Φ) и pure-literal-assign(l, Φ) - это функции, которые возвращают результат применения к переменной l и формуле Φ распространения переменной и правила исключения "чистой переменной" соответственно. Другими словами, они заменяют каждое вхождение переменной l значением "истина" и каждое вхождение переменной с отрицанием not l значением "ложь" в формуле Φ, а затем упрощают получившуюся формулу. Приведенный псевдокод возвращает только ответ - выполняет ли формулу последний из присвоенных наборов значений. В современных реализациях частичные выполнящие наборы тоже возвращаются в случае успеха.

Алгоритм зависит от выбора "переменной ветвления", т.е. переменной, которая выбирается на очередном шаге алгоритма с возвратом. для присвоения ей определенного значения. Таким образом, это не один алгоритм, а целое семейство алгоритмов, по одному на каждый возможный способ выбора "переменных ветвления". Эффективность алгоритма сильно зависит от этого выбора: существуют примеры задач, время работы алгоритма для которых может быть константой или расти экспоненциально, в зависимости от выбора "переменных ветвления". Методы выбора представляют собой эвристические техники и называются также "эвристиками для ветвления" (branching heuristics)^[6].

Современные исследования

Текущие исследования по улучшению алгоритма выполняются в трех направлениях: определению различных оптимизирующих методов выбора "переменной ветвления"; разработка новых структур данных для ускорения работы алгоритма, особенно для распространения переменной; и разработка различных вариантов базового алгоритма перебора с возвратом. Последнее направление включает "нехронологические возвраты" и запоминание плохих случаев. Эти улучшения можно описать как метод возврата после достижения ложной дизъюнкты, при котором запоминается, какое именно присвоение значения переменной повлекло этот результат, чтобы в дальнейшем избежать точно такой же последовательности вычислений, тем самым сократив время работы.

Более новый алгоритм - метод Сталмарка - известен с 1990 года. Также с 1986 года для решения задачи SAT используются диаграммы решений.

Ссылки

General

• Davis, Martin; Putnam, Hilary (1960). «A Computing Procedure for Quantification Theory». Journal of the ACM 7 (3): 201–215. DOI:10.1145/321033.321034.
• Davis, Martin; Logemann, George, and Loveland, Donald (1962). «A Machine Program for Theorem Proving». Communications of the ACM 5 (7): 394–397. DOI:10.1145/368273.368557.
• Ouyang, Ming (1998). «How Good Are Branching Rules in DPLL?». Discrete Applied Mathematics 89 (1–3): 281–286. DOI:10.1016/S0166-218X(98)00045-6.
• John Harrison Handbook of practical logic and automated reasoning. — Cambridge University Press, 2009. — P. 79–90. — ISBN 9780521899574

1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), "«Abstract DPLL and Abstract DPLL Modulo Theories»", Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings: 36–50, <http://www.lsi.upc.edu/~roberto/papers/lpar04.pdf> 
2. ↑ «The international SAT Competitions web page», sat! live, <http://www.satcompetition.org/> 
3. ↑ «zChaff website», <http://www.princeton.edu/~chaff/zchaff.html> 
4. ↑ «Chaff website», <http://www.princeton.edu/~chaff/> 
5. ↑ Minisat website. Архивировано из первоисточника 20 апреля 2012.
6. ↑ (1999) «The impact of branching heuristics in propositional satisfiability algorithms». In 9th Portuguese Conference on Artificial Intelligence (EPIA). DOI:10.1.1.111.9184.

Для дальнейшего чтения

• SAT-based scalable formal verification solutions. — Springer, 2007. — P. 23–32. — ISBN 9780387691664
• Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart Selman Satisfiability Solvers // Handbook of knowledge representation / Frank Van Harmelen, Vladimir Lifschitz, Bruce Porter. — Elsevier, 2008. — Vol. 3. — P. 89–134. — ISBN 9780444522115