Алгоритм ДПЛЛ
 После 5 бесплодных попыток (красный) выбор присвоения переменной a =1, b =1 приводит после распространения единицы (внизу) к успеху (зеленый) : верхняя левая формула CNF выполнима. | |
| Сорт | Проблема логической выполнимости |
|---|---|
| Структура данных | Бинарное дерево |
| Худшая производительность | |
| Лучшая производительность | (постоянный) |
| Наихудшая пространственная сложность | (базовый алгоритм) |
В логике и информатике алгоритм Дэвиса-Патнэма-Логеманна-Лавленда ( DPLL ) полный представляет собой алгоритм обратного отслеживания на основе поиска для определения выполнимости формул пропозициональной логики в конъюнктивной нормальной форме , то есть для решения проблемы CNF-SAT .
Он был представлен в 1961 году Мартином Дэвисом , Джорджем Логеманом и Дональдом У. Лавлендом и представляет собой усовершенствование более раннего алгоритма Дэвиса-Патнэма , который представляет собой процедуру, основанную на разрешении, разработанную Дэвисом и Хилари Патнэм в 1960 году. Особенно в старых публикациях алгоритм Алгоритм Дэвиса-Логеманна-Лавленда часто называют «методом Дэвиса-Патнэма» или «алгоритмом DP». Другими распространенными именами, сохраняющими различие, являются DLL и DPLL.
Реализации и приложения [ править ]
Проблема SAT важна как с теоретической, так и с практической точки зрения. В теории сложности это была первая задача, которая оказалась NP-полной и может возникать в самых разных приложениях, таких как проверка моделей , автоматическое планирование и составление графиков , а также диагностика в искусственном интеллекте .
Таким образом, написание эффективных решателей SAT уже много лет является темой исследований. GRASP (1996–1999) был ранней реализацией с использованием DPLL. [1] На международных соревнованиях SAT реализации, основанные на DPLL, такие как zChaff [2] и МиниСат [3] были на первых местах соревнований в 2004 и 2005 годах. [4]
Другое приложение, которое часто использует DPLL, — это автоматизированное доказательство теорем или теории выполнимости по модулю (SMT), которые представляют собой задачу SAT, в которой пропозициональные переменные заменяются формулами другой математической теории .
Алгоритм [ править ]
Базовый алгоритм поиска с возвратом работает путем выбора литерала, присвоения ему значения истинности , упрощения формулы и затем рекурсивной проверки выполнимости упрощенной формулы; если это так, то исходная формула выполнима; в противном случае выполняется та же рекурсивная проверка, предполагающая противоположное значение истинности. Это известно как правило разделения , поскольку оно разбивает проблему на две более простые подзадачи. Шаг упрощения по существу удаляет из формулы все предложения, которые становятся истинными при присваивании, и все литералы, которые становятся ложными, из оставшихся предложений.
Алгоритм DPLL превосходит алгоритм обратного отслеживания за счет активного использования следующих правил на каждом этапе:
- Распространение единицы
- Если предложение является единичным предложением , т.е. оно содержит только один неназначенный литерал, это предложение может быть выполнено только путем присвоения необходимого значения, чтобы сделать этот литерал истинным. Таким образом, никакого выбора не требуется. Распространение единицы состоит в удалении каждого предложения, содержащего литерал предложения единицы, и в отбрасывании дополнения к литералу предложения единицы из каждого предложения, содержащего это дополнение. На практике это часто приводит к детерминированным каскадам модулей, что позволяет избежать значительной части наивного пространства поиска.
- Чисто буквальное исключение
- Если пропозициональная переменная встречается в формуле только с одной полярностью , ее называют чистой . Чистый литерал всегда можно присвоить таким образом, чтобы все содержащие его предложения стали истинными. Таким образом, когда оно назначено таким образом, эти пункты больше не ограничивают поиск и могут быть удалены.
Невыполнимость данного частичного присваивания обнаруживается, если одно предложение становится пустым, т. е. если все его переменные были присвоены таким образом, что соответствующие литералы становятся ложными. Выполнимость формулы обнаруживается либо тогда, когда все переменные присваиваются без создания пустого предложения, либо, в современных реализациях, если все условия удовлетворены. Невыполнимость полной формулы можно обнаружить только после перебора.
Алгоритм DPLL можно резюмировать в следующем псевдокоде, где Φ — формула CNF :
Algorithm DPLL
Input: A set of clauses Φ.
Output: A truth value indicating whether Φ is satisfiable.
function DPLL(Φ)
// unit propagation:
while there is a unit clause {l} in Φ do
Φ ← unit-propagate(l, Φ);
// pure literal elimination:
while there is a literal l that occurs pure in Φ do
Φ ← pure-literal-assign(l, Φ);
// stopping conditions:
if Φ is empty then
return true;
if Φ contains an empty clause then
return false;
// DPLL procedure:
l ← choose-literal(Φ);
return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});
- « ←» означает присвоение . Например, « самый большой ← элемент » означает, что значение самого большого изменяется на значение элемента .
- « return » завершает алгоритм и выводит следующее значение.
В этом псевдокоде unit-propagate(l, Φ) и pure-literal-assign(l, Φ) — это функции, которые возвращают результат применения единичного распространения и правила чистого литерала соответственно к литералу l и формула Φ. Другими словами, они заменяют каждое появление l с «истиной» и каждым появлением not l с «ложью» в формуле Φ, и упростим полученную формулу. or в return оператор является оператором короткого замыкания . Φ ∧ {l} обозначает упрощенный результат замены «истина» на l в Φ.
Алгоритм завершается в одном из двух случаев. Либо формула КНФ Φ пусто, т. е. не содержит никаких предложений. Тогда оно удовлетворяется любым присвоением, поскольку все его положения бессмысленно истинны. В противном случае, когда формула содержит пустое предложение, это предложение является бессмысленно ложным, поскольку для того, чтобы общее множество было истинным, для дизъюнкции требуется хотя бы один член, который является истинным. В этом случае существование такого предложения подразумевает, что формула (рассчитываемая как совокупность всех предложений) не может быть истинной и должна быть невыполнимой.
Функция псевдокода DPLL возвращает только то, удовлетворяет ли окончательное присвоение формуле или нет. В реальной реализации частично удовлетворяющее присваивание обычно также возвращается в случае успеха; это можно получить, отслеживая литералы ветвления и присвоения литералов, выполненные во время распространения единиц и чистого буквального исключения.
Алгоритм Дэвиса-Логеманна-Лавленда зависит от выбора литерала ветвления , который является литералом, рассматриваемым на этапе обратного отслеживания. В результате это не совсем алгоритм, а скорее семейство алгоритмов, по одному для каждого возможного способа выбора литерала ветвления. На эффективность сильно влияет выбор литерала ветвления: существуют случаи, для которых время выполнения является постоянным или экспоненциальным в зависимости от выбора литералов ветвления. Такие функции выбора также называются эвристическими функциями или эвристиками ветвления. [5]
Визуализация [ править ]
Дэвис, Логеманн, Лавленд (1961) разработали этот алгоритм. Некоторые свойства этого оригинального алгоритма:
- Он основан на поиске.
- Это основа почти всех современных решателей SAT.
- Он не использует обучение или нехронологический возврат (введен в 1996 году).
Пример с визуализацией алгоритма DPLL, имеющего хронологический возврат:
-
Все предложения, составляющие формулу CNF -
Выберите переменную -
Примите решение, переменная a = False (0), поэтому зеленые предложения станут True. -
Приняв несколько решений, мы находим граф последствий , который приводит к конфликту. -
Теперь вернитесь на непосредственный уровень и принудительно присвойте этой переменной противоположное значение. -
Но вынужденное решение всё равно приводит к очередному конфликту -
Вернитесь на предыдущий уровень и примите вынужденное решение. -
Принять новое решение, но оно приводит к конфликту -
Принять вынужденное решение, но оно снова приводит к конфликту -
Возврат на предыдущий уровень -
Продолжайте в том же духе и окончательный график последствий
Связанные алгоритмы [ править ]
(пониженно упорядоченные) двоичные диаграммы решений . С 1986 года для решения SAT также используются [ нужна ссылка ]
В 1989–1990 годах был представлен и запатентован метод Стольмарка для проверки формул. Он нашел некоторое применение в промышленности. [6]
DPLL был расширен для автоматического доказательства теорем для фрагментов логики первого порядка с помощью алгоритма DPLL(T) . [1]
В течение десятилетия 2010-2019 годов работа над улучшением алгоритма позволила найти более эффективные стратегии выбора литералов ветвления и новых структур данных, чтобы сделать алгоритм быстрее, особенно в части распространения единиц . Однако основным улучшением стал более мощный алгоритм, Conflict-Driven Clause Learning (CDCL), который похож на DPLL, но после возникновения конфликта «изучает» коренные причины (присвоения переменным) конфликта и использует эту информацию. выполнить нехронологический возврат назад (также известный как возврат назад ), чтобы избежать повторного возникновения того же конфликта. По состоянию на 2019 год большинство современных решателей SAT основаны на платформе CDCL. [7]
Связь с другими понятиями [ править ]
Прогоны алгоритмов на основе DPLL на невыполнимых экземплярах соответствуют доказательствам опровержения разрешения дерева . [8]
См. также [ править ]
Ссылки [ править ]
Общий
- Дэвис, Мартин ; Патнэм, Хилари (1960). «Вычислительная процедура для количественной теории» . Журнал АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376 .
- Дэвис, Мартин; Логеманн, Джордж; Лавленд, Дональд (1961). «Машинная программа для доказательства теорем» . Коммуникации АКМ . 5 (7): 394–397. дои : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
- Оуян, Мин (1998). «Насколько хороши правила ветвления в DPLL?». Дискретная прикладная математика . 89 (1–3): 281–286. дои : 10.1016/S0166-218X(98)00045-6 .
- Джон Харрисон (2009). Справочник по практической логике и автоматизированным рассуждениям . Издательство Кембриджского университета. стр. 79–90. ISBN 978-0-521-89957-4 .
Специфический
- ^ Jump up to: Перейти обратно: а б Ньювенхейс, Роберт; Оливерас, Альберт; Тинелли, Сезар (2004), «Абстрактные теории DPLL и абстрактные теории DPLL по модулю» (PDF) , Proceedings Int. Конф. « Логика программирования, искусственного интеллекта и рассуждения» , LPAR 2004 , стр. 36–50.
- ^ Сайт zChaff
- ^ «Сайт Минисат» .
- ^ Веб-страница международных соревнований SAT , сб! жить
- ^ Маркес-Сильва, Жоау П. (1999). «Влияние эвристики ветвления на алгоритмы пропозициональной выполнимости». В Бараоне Педро; Прапорщик, Хосе Дж. (ред.). Прогресс в области искусственного интеллекта: 9-я португальская конференция по искусственному интеллекту, EPIA '99, Эвора, Португалия, 21–24 сентября 1999 г., материалы . ЛНКС . Том. 1695. стр. 62–63. дои : 10.1007/3-540-48159-1_5 . ISBN 978-3-540-66548-9 .
- ^ Стольмарк, Г.; Сэфлунд, М. (октябрь 1990 г.). «Моделирование и проверка систем и программного обеспечения в логике высказываний». Тома трудов МФБ . 23 (6): 31–36. дои : 10.1016/S1474-6670(17)52173-4 .
- ^ Мёле, Сибилла; Бьер, Армин (2019). «Обратный возврат». Теория и применение тестирования выполнимости – SAT 2019 (PDF) . Конспекты лекций по информатике. Том. 11628. стр. 250–266. дои : 10.1007/978-3-030-24258-9_18 . ISBN 978-3-030-24257-2 . S2CID 195755607 .
- ^ Ван Бик, Питер (2006). «Алгоритмы поиска с возвратом» . В Росси, Франческа; Ван Бик, Питер; Уолш, Тоби (ред.). Справочник по программированию в ограничениях . Эльзевир. п. 122. ИСБН 978-0-444-52726-4 .
Дальнейшее чтение [ править ]
- малайский ганай; Аарти Гупта; Доктор Аарти Гупта (2007). Масштабируемые решения для формальной проверки на основе SAT . Спрингер. стр. 23–32. ISBN 978-0-387-69166-4 .
- Гомес, Карла П.; Каутц, Генри; Сабхарвал, Ашиш; Селман, Барт (2008). «Решатели выполнимости». В Ван Хармелен, Фрэнк; Лифшиц, Владимир; Портер, Брюс (ред.). Справочник по представлению знаний . Основы искусственного интеллекта. Том. 3. Эльзевир. стр. 89–134. дои : 10.1016/S1574-6526(07)03002-7 . ISBN 978-0-444-52211-5 .