DPLL

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

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

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

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

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

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

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

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

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

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

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

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

function DPLL(Φ)
   если Φ - это набор выполняющихся дизъюнкт
       тогда return true;
   если Φ содержит пустую дизъюнкту
       then return false;
   для каждой дизъюнкты из одной переменной l в Φ
      Φ ${\displaystyle \leftarrow }$ unit-propagate(l, Φ);
   для каждой переменной l которая встречается в чистом виде в Φ
      Φ ${\displaystyle \leftarrow }$ pure-literal-assign(l, Φ);
   l ${\displaystyle \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 используются диаграммы решений.

На основе DPLL-алгоритма в середине 1990-х был создан и стал широко применяться CDCL-алгоритм.

• Malay Ganai; Aarti Gupta; Dr. Aarti Gupta. 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. — Т. 3. — С. 89—134. — (Foundations of Artificial Intelligence). — ISBN 9780444522115. — doi:10.1016/S1574-6526(07)03002-7.
• Davis, Martin; Putnam, Hilary. A Computing Procedure for Quantification Theory (англ.) // Journal of the ACM : journal. — 1960. — Vol. 7, no. 3. — P. 201—215. — doi:10.1145/321033.321034.
• Davis, Martin; Logemann, George, and Loveland, Donald. A Machine Program for Theorem Proving (англ.) // Communications of the ACM : journal. — 1962. — Vol. 5, no. 7. — P. 394—397. — doi:10.1145/368273.368557.
• Ouyang, Ming. How Good Are Branching Rules in DPLL? (англ.) // Discrete Applied Mathematics : journal. — 1998. — Vol. 89, no. 1—3. — P. 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.