Оглавление
Алгоритм DPLL
-
История и реализация
- Алгоритм Дэвиса–Патнэма–Логемана–Лавленда (DPLL) был представлен в 1961 году.
- Он основан на обратном отслеживании и является усовершенствованием алгоритма Дэвиса–Патнэма.
- DPLL часто упоминается как “метод Дэвиса–Патнэма” или “алгоритм DP”.
- Ранние реализации, такие как GRASP, заняли первые места на международных соревнованиях.
-
Применение и сложность
- Проблема SAT важна для теории сложности и практических приложений.
- DPLL используется в автоматическом доказательстве теорем и теории выполнимости по модулю (SMT).
- Алгоритм DPLL превосходит обратное отслеживание за счет активного использования правил.
-
Алгоритм DPLL
- Базовый алгоритм обратного отслеживания выполняется путем выбора литерала и упрощения формулы.
- DPLL использует правила для обнаружения неудовлетворительности и выполнимости.
- Алгоритм завершается, когда формула пуста или содержит пустое предложение.
-
Визуализация и связанные алгоритмы
- DPLL основан на поиске и является основой для современных SAT-решателей.
- С 1986 года используются бинарные диаграммы принятия решений.
- В 1989-1990 годах был представлен метод Столмарка.
- DPLL был расширен для автоматизированного доказательства теорем.
-
Современные улучшения
- В 2010-2019 годах улучшена политика выбора литералов и структуры данных.
- CDCL, основанный на изучении конфликтных предложений, стал главным улучшением.
- Большинство современных SAT-решателей основаны на CDCL.
-
Связь с другими понятиями
- Запуск DPLL на неудовлетворительных экземплярах соответствует доказательствам опровержения.