Нормальные формы и алгоритм DPLL

Мотивация: автоматическая проверка выполнимости

Задача SAT (SATisfiability) — проверить, выполнима ли пропозициональная формула — NP-полна, но на практике решается за секунды для миллионов переменных с помощью современных SAT-солверов. Они работают с формулами в конъюнктивной нормальной форме (КНФ) и используют алгоритм DPLL и его расширения. SAT — «рабочая лошадка» формальной верификации, планирования и синтеза.

Нормальные формы

Литерал: переменная p или её отрицание ¬p.

Дизъюнкт: дизъюнкция литералов: (l₁ ∨ l₂ ∨ ... ∨ lₖ). Единичный дизъюнкт: дизъюнкт из одного литерала.

КНФ (конъюнктивная нормальная форма): конъюнкция дизъюнктов: D₁ ∧ D₂ ∧ ... ∧ Dₘ. Любая пропозициональная формула приводима к КНФ (равновыполнимой, если использовать трансформацию Цейтина).

Алгоритм приведения к КНФ:

Устранить → и ↔: p→q ≡ ¬p∨q; p↔q ≡ (¬p∨q)∧(p∨¬q)
Загнать ¬ внутрь (законы де Моргана, двойное отрицание)
Применить дистрибутивность ∨ над ∧

ДНФ (дизъюнктивная нормальная форма): дизъюнкция конъюнктов. Выполнима ⟺ хотя бы один конъюнкт не содержит p ∧ ¬p.

Задача SAT и алгоритм DPLL

DPLL (Davis–Putnam–Logemann–Loveland, 1960/62): рекурсивный алгоритм поиска выполняющей оценки:

Распространение единиц (Unit Propagation): если дизъюнкт содержит ровно один незначенный литерал l → l = 1; удалить все дизъюнкты с l; удалить ¬l из остальных дизъюнктов. Повторять до фиксированной точки.
Чистые литералы (Pure Literal Elimination): если литерал l встречается только положительно (не встречается ¬l) → l = 1; удалить все дизъюнкты с l.
Выбор переменной: выбрать незначенную p; рекурсивно попробовать p=1, затем p=0.
Возврат (Backtrack): при пустом дизъюнкте — противоречие, возврат.

Современные CDCL-солверы: при конфликте добавляют «усвоенный дизъюнкт» (clause learning), исключающий данный конфликт. Решают задачи с миллионами переменных (криптографические схемы, верификация процессоров).

Численный пример

Задача: Применить DPLL к формуле: (p ∨ q) ∧ (¬p ∨ r) ∧ (¬q ∨ ¬r) ∧ (p ∨ ¬r).

Шаг 1. Unit Propagation. Нет единичных дизъюнктов. Нет чистых литералов (p и ¬p оба встречаются; q и ¬q; r и ¬r).

Шаг 2. Выбор: p = 1.

(p ∨ q): удалить (содержит p = 1) ✓
(¬p ∨ r): удалить ¬p из дизъюнкта → (r)
(¬q ∨ ¬r): остаётся
(p ∨ ¬r): удалить ✓ Остаток: (r) ∧ (¬q ∨ ¬r).

Шаг 3. Unit Propagation: (r) → r = 1.

(¬q ∨ ¬r): удалить ¬r → (¬q) Остаток: (¬q).

Шаг 4. Unit Propagation: (¬q) → q = 0. Все дизъюнкты удовлетворены.

Решение: p = 1, q = 0, r = 1. Формула выполнима ✓.

Проверка: (1∨0)∧(0∨1)∧(1∨0)∧(1∨0) = 1∧1∧1∧1 = 1 ✓.

Второй вариант (если бы DPLL зашёл в тупик): если r = 0 → (¬q ∨ 0) = (¬q) → q = 0 → (0∨0) = 0 — противоречие! Возврат.

Реальное приложение

Разработка чипов (Intel, AMD): перед выпуском процессора сотни тысяч свойств проверяются SAT-солверами (аппаратная верификация). Планирование миссий (NASA): задача планирования кодируется в SAT за полиномиальное время, солвер находит последовательность действий.

Дополнительные аспекты

Алгоритм DPLL (Davis–Putnam–Logemann–Loveland) — основа всех современных SAT-решателей. Его улучшения CDCL добавляют обучение клауз: при каждом конфликте формируется новая клауза, исключающая повторение того же тупика. Это даёт экспоненциальный прирост на структурированных задачах. CNF-нормализация Цейтлина вводит вспомогательные переменные для подформул, благодаря чему сохраняет линейный размер преобразования (наивная дистрибутивная нормализация может дать экспоненциальный взрыв). DNF, наоборот, удобна для автоматов и таблиц истинности. Примечательно, что разрешение CNF-формулы в DNF — экспоненциально трудная задача.

Связь с другими разделами математики

Логические нормальные формы неожиданно близки к классическим разделам алгебры. Уже у Гильберта и Акермана логика трактуется как часть универсальной алгебры: булевы формулы — элементы свободной булевой алгебры, а КНФ соответствует представлению этих элементов через пересечение (конъюнкцию) идеалов, задаваемых дизъюнктами. Теорема Стоуна о представлении булевых алгебр через топологические пространства ультрафильтров фактически интерпретирует множество моделей КНФ-формулы как открытое множество в стоуновском пространстве, что связывает SAT с топологией.

В теории вероятностей КНФ возникает в виде логических схем событий: вероятность выполнимости заменяется оценкой вероятности, что хотя бы один дизъюнкт в каждой конъюнкции выполняется. Подходы типа вероятностных методов Ловаса и Эрдёша позволяют оценивать размеры случайных КНФ, почти наверняка невыполнимых, что перекликается с фазовыми переходами в случайных SAT-моделях и методами статистической физики (спин-стеклянные модели Мезара и Паранжина).

Численные методы и дифференциальные уравнения связаны с SAT через гибридные методы оптимизации. С начала 2000‑х годов развиваются дифференциальные приближения к дискретным задачам: траектории динамических систем аппроксимируют процессы поиска; анализ устойчивости стационарных точек опирается на идеи Ляпунова. В вариациях SMT-солверов (Satisfiability Modulo Theories) логические ограничения в КНФ комбинируются с линейной алгеброй и системами дифференциальных уравнений, а проверка выполнимости превращается в смешанную задачу дискретно-непрерывной оптимизации.

С точки зрения вычислительной сложности алгоритм DPLL реализует экспоненциальное дерево поиска, тесно связанное с теоремой Кука–Левина о NP-полноте SAT. Методы резолюции (Рабин, Робинсон) дают логический аналог метода исключения Гаусса, а результаты Харлау–Разборова, Бенаса и других по нижним оценкам длины резолюционных доказательств интерпретируются как пределы для производительности любых DPLL-подобных солверов.

Историческая справка и развитие идеи

Представления логических формул в стандартных нормальных формах появились уже в работах Бооля и Джевонса во второй половине XIX века, однако систематическая теория была оформлена в начале XX века школой Гильберта. В книге «Grundzüge der theoretischen Logik» (1928) Гильберт и Акерман формализовали преобразование формул к эквивалентным КНФ и ДНФ. Вопрос о выполнимости формул впервые был поставлен в контексте общей теории решений логических уравнений (работы Чёрча, Тарского). В 1930‑х Мозес Шёнфинкель и последующие логики рассматривали нормальные формы как инструмент для автоматизации вывода. Переломным моментом стала статья Мартина Дэвиса и Гилберта Патнэма 1960 года в Journal of the ACM, где был предложен алгоритм на основе резолюции и систематического исключения переменных. Через два года Дэвис, Логеман и Лавленд модифицировали подход, введя рекурсивную схему ветвления по литералам с упрощением формулы по ходу поиска; именно этот вариант стал известен как DPLL. Мотивирующими задачами были автоматизация доказательств теорем и проверка корректности программ в ранних системах формальной верификации. В 1971 году Кук, а затем независимо Левин показали NP-полноту SAT, сделав его центральной задачей теории сложности.