Задача выполнимости булевых формул

Задача выполнимости булевых формул (SAT, от англ. Boolean satisfiability problem) — это фундаментальная задача теории вычислительной сложности и математической логики, состоящая в определении, существует ли набор значений переменных (истина или ложь), при котором заданная булева формула принимает значение «истина». Если такой набор существует, формула называется выполнимой, в противном случае — невыполнимой. SAT является первой задачей, для которой была доказана NP-полнота (теорема Кука — Левина, 1971 год), что делает её центральной в теории сложности вычислений и ключевой для понимания класса NP.

История и происхождение

Корни задачи SAT восходят к работам по булевой алгебре, разработанной Джорджем Булем в середине XIX века. Однако как вычислительная проблема она оформилась в середине XX века с развитием теории алгоритмов и электронно-вычислительных машин. В 1971 году американский учёный Стивен Кук в своей статье «Сложность процедур вывода теорем» доказал, что задача SAT является NP-полной. Независимо от него, в 1973 году советский математик Леонид Левин опубликовал аналогичный результат, что привело к признанию SAT одной из самых важных задач в информатике.

Доказательство NP-полноты SAT означает, что любая задача из класса NP может быть сведена к SAT за полиномиальное время, и если для SAT будет найден эффективный (полиномиальный) алгоритм, то все задачи класса NP будут решаться за полиномиальное время. Это напрямую связано с проблемой равенства классов P и NP, одной из семи «задач тысячелетия» Математического института Клэя.

Формальная постановка

Задача SAT формулируется для булевых формул, представленных в конъюнктивной нормальной форме (КНФ). Формула в КНФ представляет собой конъюнкцию (логическое «И») нескольких дизъюнктов (логических «ИЛИ»), каждый из которых состоит из литералов — переменных или их отрицаний. Например, формула \((x_1 \lor \neg x_2) \land (x_2 \lor x_3)\) является КНФ. Задача заключается в том, чтобы найти значения переменных \(x_1, x_2, x_3\), при которых вся формула истинна.

В общем случае формула может быть произвольной, но стандартная постановка SAT рассматривает именно КНФ, так как любая булева формула может быть приведена к КНФ за полиномиальное время (хотя при этом возможно экспоненциальное увеличение размера формулы). Частным случаем является задача 3-SAT, где каждый дизъюнкт содержит ровно три литерала; 3-SAT также является NP-полной.

Классификация и варианты

Задача SAT имеет множество модификаций и ограничений, которые влияют на её сложность:

По форме формулы

• SAT в КНФ — стандартная постановка.
• SAT в ДНФ (дизъюнктивная нормальная форма) — задача тривиально решается за полиномиальное время, так как достаточно проверить каждый дизъюнкт.
• SAT для произвольных формул — общий случай, NP-полный.

По количеству литералов в дизъюнкте

• 2-SAT — каждый дизъюнкт содержит два литерала; решается за полиномиальное время (например, с помощью графа импликаций).
• 3-SAT — три литерала; NP-полная задача.
• k-SAT для \(k \ge 3\) — NP-полная.

По структуре

• Монотонный SAT — все литералы неотрицательны (нет отрицаний); задача тривиально выполнима, если нет пустых дизъюнктов.
• Хорновский SAT — каждый дизъюнкт содержит не более одного положительного литерала; решается за полиномиальное время (алгоритм единичного распространения).

По количеству решений

• SAT — задача существования хотя бы одного решения.
• #SAT (задача подсчёта) — подсчёт количества всех выполняющих наборов; является #P-полной.
• MAJSAT — определение, выполнима ли формула для большинства наборов; также сложна.

Алгоритмы решения

Несмотря на NP-полноту, на практике SAT-решатели (SAT-солверы) способны обрабатывать формулы с миллионами переменных и дизъюнктов. Основные подходы:

Полные алгоритмы

• Поиск с возвратом (backtracking) — основа алгоритма DPLL (Davis–Putnam–Logemann–Loveland). Рекурсивно выбирается переменная, ей присваивается значение, и формула упрощается. При противоречии происходит возврат.
• CDCL (Conflict-Driven Clause Learning) — современное развитие DPLL. При обнаружении конфликта анализируется его причина, и в формулу добавляется новый дизъюнкт (обучение), предотвращающий повторение того же конфликта. CDCL лежит в основе большинства современных SAT-солверов (например, MiniSat, Glucose, Lingeling).

Неполные алгоритмы

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

Алгоритмы для специальных классов

• Для 2-SAT — алгоритм на основе графа импликаций (линейное время).
• Для Хорновского SAT — алгоритм единичного распространения (линейное время).

Применение

Задача SAT имеет широкое практическое применение в различных областях, несмотря на теоретическую сложность. Современные SAT-солверы используются для:

• Верификация аппаратного и программного обеспечения — проверка корректности цифровых схем, программных модулей и протоколов. Формальная верификация часто сводится к задаче SAT.
• Планирование и составление расписаний — задачи планирования действий (например, в логистике или робототехнике) могут быть сведены к SAT.
• Криптоанализ — атаки на криптографические системы, такие как поиск коллизий хеш-функций или взлом шифров, часто формулируются как SAT.
• Автоматическое доказательство теорем — SAT-солверы являются ядром многих систем автоматического доказательства.
• Биоинформатика — задачи анализа генетических последовательностей, например, поиск гаплотипов или моделирование метаболических путей.
• Искусственный интеллект — решение задач логического вывода, планирования и конфигурации.

Связь с другими задачами

SAT тесно связана с другими NP-полными задачами, такими как задача о клике, задача о вершинном покрытии, задача коммивояжёра. Благодаря NP-полноте, любая из них может быть сведена к SAT, что позволяет использовать SAT-солверы для их решения. Существуют также задачи, сводящиеся к SAT в обратную сторону, например, задача выполнимости квантовых булевых формул (QSAT) для квантовых компьютеров.

Критика и ограничения

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

Критики также отмечают, что многие SAT-солверы оптимизированы под определённые типы формул, и их производительность может сильно варьироваться. В сообществе SAT проводятся ежегодные соревнования (SAT Competition), где сравниваются различные солверы на наборах тестовых задач.

Интересные факты

• В 2019 году группа исследователей из Массачусетского технологического института (MIT) и других университетов представила SAT-солвер, способный решать некоторые задачи, которые ранее считались практически неразрешимыми, включая задачи из области комбинаторной математики.
• Задача SAT используется в некоторых системах искусственного интеллекта для автоматического планирования, например, в планировщике STRIPS.
• Существует версия SAT для квантовых компьютеров — квантовая задача выполнимости (QSAT), которая является QMA-полной (квантовый аналог NP).

Источники

• Cook, S. A. (1971). «The complexity of theorem-proving procedures». Proceedings of the Third Annual ACM Symposium on Theory of Computing.
• Levin, L. A. (1973). «Universal search problems». Problems of Information Transmission.
• Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). «Handbook of Satisfiability». IOS Press.
• Gomes, C. P., Kautz, H., Sabharwal, A., & Selman, B. (2008). «Satisfiability Solvers». Handbook of Knowledge Representation.
• Arora, S., & Barak, B. (2009). «Computational Complexity: A Modern Approach». Cambridge University Press.