Алгоритм DPLL - DPLL algorithm

DPLL
Dpll11.png
В формуле CNF-SAT : 1-Выберите литерал 2-Присвойте ему значение истинности 3-Упростите формулу 4-Проверьте выполнение; 5-Если не устраивает, сделайте возврат
Класс Проблема логической выполнимости
Структура данных Двоичное дерево
Наихудшая производительность
Лучшая производительность (постоянный)
Сложность пространства в наихудшем случае (базовый алгоритм)

В логике и информатике , то Дэвис-Putnam-Logemann-Loveland ( DPLL ) алгоритм является полным , возвраты - алгоритмом поиска для принятия решения о выполнимости из пропозициональных формул логики в конъюнктивной нормальной форме , то есть для решения CNF-SAT проблемы.

Он был введен в 1961 году Мартином Дэвисом , Джорджем Логеманном и Дональдом В. Лавлендом и является усовершенствованием более раннего алгоритма Дэвиса – Патнэма , основанного на разрешающей способности процедуры, разработанной Дэвисом и Хилари Патнэм в 1960 году. Алгоритм Дэвиса – Логеманна – Ловленда часто называют «методом Дэвиса – Патнэма» или «алгоритмом DP». Другие общие имена, поддерживающие различие, - это DLL и DPLL.

По прошествии более чем 50 лет процедура DPLL по-прежнему является основой для наиболее эффективных полных решателей SAT. Недавно он был расширен для автоматического доказательства теорем для фрагментов логики первого порядка с помощью алгоритма DPLL (T) .

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

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

Таким образом, это была горячая тема в исследованиях в течение многих лет, и соревнования между решателями SAT проводятся регулярно. Современные реализации DPLL, такие как Chaff и zChaff , GRASP или MiniSat, в последние годы занимают первые места в соревнованиях.

Другое приложение, которое часто включает DPLL, - это автоматическое доказательство теорем или выполнимость по модулю теорий (SMT), которое представляет собой задачу SAT, в которой пропозициональные переменные заменяются формулами другой математической теории .

Алгоритм

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

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

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

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

Алгоритм DPLL можно резюмировать в следующем псевдокоде, где Φ - формула CNF :

Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A Truth Value.
function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    lchoose-literal(Φ);
    return DPLL {l}) or DPLL {not(l)});
  • «←» обозначает присвоение . Например, « самый большойэлемент » означает, что значение самого большого элемента изменяется на значение элемента .
  • « return » завершает алгоритм и выводит следующее значение.

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

Алгоритм завершается в одном из двух случаев. Либо формула CNF Φсодержит согласованный набор литералов, то есть в формуле нет литерала lи ¬lдля любого литерала l(есть только чистые литералы). Если это так, переменные можно тривиально удовлетворить, установив для них соответствующую полярность охватывающего литерала в оценке. В противном случае, когда формула содержит пустое предложение, это предложение является пустым ложным, поскольку дизъюнкция требует, чтобы хотя бы один член был истинным, чтобы весь набор был истинным. В этом случае наличие такого предложения подразумевает, что формула (оцениваемая как совокупность всех предложений) не может быть истинной и должна быть невыполнимой.

Функция псевдокода DPLL возвращает только то, удовлетворяет ли окончательное присвоение формуле или нет. В реальной реализации частичное удовлетворяющее присвоение обычно также возвращается в случае успеха; это может быть получено из согласованного набора литералов первого ifоператора функции.

Алгоритм Дэвиса – Логеманна – Ловленда зависит от выбора литерала ветвления , который является литералом, учитываемым на этапе поиска с возвратом. В результате это не совсем алгоритм, а скорее семейство алгоритмов, по одному для каждого возможного способа выбора литерала ветвления. На эффективность сильно влияет выбор литерала ветвления: существуют экземпляры, для которых время работы является постоянным или экспоненциальным, в зависимости от выбора литералов ветвления. Такие функции выбора также называются эвристическими функциями или эвристиками ветвления.

Визуализация

Дэвис, Логеманн, Лавленд (1961) разработали этот алгоритм. Некоторые свойства этого оригинального алгоритма:

  • Он основан на поиске.
  • Это основа почти всех современных решателей SAT.
  • Он не использует обучение или не хронологический возврат (введен в 1996 г.).

Пример с визуализацией алгоритма DPLL с хронологическим возвратом:

Текущая работа

В 2010-е годы работа по совершенствованию алгоритма велась по трем направлениям:

  1. Определение различных политик для выбора литералов ветвления.
  2. Определение новых структур данных для ускорения алгоритма, особенно в части распространения единиц .
  3. Определение вариантов базового алгоритма поиска с возвратом. Последнее направление включает в себя нехронологический возврат с возвратом (также известный как обратный переход ) и изучение предложений . Эти уточнения описывают метод отслеживания с возвратом после достижения пункта конфликта, который «изучает» основные причины (присваивания переменным) конфликта, чтобы избежать повторения того же конфликта снова. Получившиеся в результате решатели SAT для изучения положений о конфликтах являются самыми современными в 2014 году.

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

Отношение к другим понятиям

Выполнение алгоритмов на основе DPLL на неудовлетворительных экземплярах соответствует доказательствам опровержения разрешения дерева .

Смотрите также

Рекомендации

Общий

  • Дэвис, Мартин ; Патнэм, Хилари (1960). «Вычислительная процедура для теории количественной оценки» . Журнал ACM . 7 (3): 201–215. DOI : 10.1145 / 321033.321034 .
  • Дэвис, Мартин; Логеманн, Джордж; Ловленд, Дональд (1961). "Машинная программа для доказательства теорем" . Коммуникации ACM . 5 (7): 394–397. DOI : 10.1145 / 368273.368557 . hdl : 2027 / mdp.39015095248095 .
  • Оуян, Мин (1998). "Насколько хороши правила ветвления в DPLL?" . Дискретная прикладная математика . 89 (1–3): 281–286. DOI : 10.1016 / S0166-218X (98) 00045-6 .
  • Джон Харрисон (2009). Справочник по практической логике и автоматизированным рассуждениям . Издательство Кембриджского университета. С. 79–90. ISBN 978-0-521-89957-4.

Конкретный

дальнейшее чтение

  • Малайский ганай; Аарти Гупта; Доктор Арти Гупта (2007). Масштабируемые решения для формальной проверки на основе SAT . Springer. С. 23–32. ISBN 978-0-387-69166-4.
  • Gomes, Carla P .; Каутц, Генри; Сабхарвал, Ашиш; Селман, Барт (2008). «Решатели выполнимости». В Ван Хармелен, Франк; Лифшиц, Владимир; Портер, Брюс (ред.). Справочник по представлению знаний . Основы искусственного интеллекта. 3 . Эльзевир. С. 89–134. DOI : 10.1016 / S1574-6526 (07) 03002-7 . ISBN 978-0-444-52211-5.