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

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

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

Пусть дана булева формула \( \varphi \), построенная из переменных \( x_1, x_2, \dots, x_n \), логических связок (конъюнкция \( \land \), дизъюнкция \( \lor \), отрицание \( \lnot \)) и, возможно, скобок. Задача SAT состоит в ответе на вопрос: существует ли такое присваивание значений истинности (0 или 1, «ложь» или «истина») каждой переменной, что \( \varphi \) принимает значение 1? Если такое присваивание существует, формула называется выполнимой; в противном случае — невыполнимой (противоречием).

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

История и значение

Происхождение

Задача SAT восходит к работам по логике и теории алгоритмов середины XX века. В 1971 году Стивен Кук в своей знаковой статье «Сложность процедур доказательства теорем» сформулировал понятие NP-полноты и доказал, что задача SAT является NP-полной (теорема Кука — Левина). Это открытие показало, что SAT — одна из самых «трудных» задач в классе NP, и что если для неё будет найден эффективный (полиномиальный) алгоритм, то все задачи класса NP будут решаться за полиномиальное время.

Влияние на теорию сложности

SAT стала эталоном для доказательства NP-полноты других задач. Метод сведения (редукции) любой задачи из NP к SAT лёг в основу классификации вычислительной сложности. Вопрос о том, существует ли полиномиальный алгоритм для SAT, эквивалентен знаменитому вопросу «P = NP?», который остаётся одной из главных нерешённых проблем современной математики и информатики.

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

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

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

По ограничениям на переменные

• MAX-SAT: задача поиска присваивания, максимизирующего количество выполняемых дизъюнктов (NP-трудная задача оптимизации).
• #SAT: задача подсчёта количества выполняющих присваиваний (сложнее NP — #P-полная).
• Weighted SAT: переменным и/или дизъюнктам приписаны веса, и требуется найти присваивание с максимальным суммарным весом.

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

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

Полные алгоритмы гарантированно находят выполняющее присваивание или доказывают невыполнимость. Основной метод — алгоритм DPLL (Davis–Putnam–Logemann–Loveland), предложенный в 1960-х годах. Он основан на рекурсивном переборе с возвратом (backtracking) и включает два ключевых правила:

• Единичное распространение (unit propagation): если дизъюнкт состоит из одного литерала, то этот литерал должен быть истинным.
• Чистый литерал (pure literal rule): если переменная встречается только с одной полярностью (только положительно или только отрицательно), то она может быть установлена так, чтобы удовлетворить все содержащие её дизъюнкты.

Современные SAT-решатели (например, MiniSat, Glucose, Z3) используют усовершенствованные версии DPLL, включая:

• Запоминание конфликтов (conflict-driven clause learning, CDCL): при обнаружении конфликта решатель анализирует его причины и добавляет новый дизъюнкт (запрещающий данное сочетание значений), что предотвращает повторение ошибки.
• Эвристики выбора переменной (например, VSIDS — Variable State Independent Decaying Sum).
• Рестарты: периодический сброс состояния поиска для выхода из локальных минимумов.

Приближённые и эвристические алгоритмы

Для больших формул, где точные алгоритмы могут работать экспоненциально долго, применяются:

• Локальный поиск (например, алгоритм GSAT, WalkSAT): случайным образом выбирается присваивание, затем оно итеративно улучшается путём переворота значения одной переменной, минимизирующего число невыполненных дизъюнктов.
• Методы Монте-Карло и генетические алгоритмы.

Применение

Верификация аппаратного и программного обеспечения

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

Автоматизированное доказательство теорем

SAT-решатели лежат в основе систем SMT (Satisfiability Modulo Theories), которые расширяют SAT на более выразительные логики (арифметика, теория массивов, строки). SMT-решатели (например, Z3, CVC4) применяются в статическом анализе кода, генерации тестов и синтезе программ.

Планирование и задачи оптимизации

Задачи планирования в искусственном интеллекте (например, планирование действий робота) часто кодируются как SAT-формулы. Аналогично, задачи составления расписаний, назначения ресурсов и упаковки (bin packing) сводятся к SAT.

Криптография и безопасность

Анализ криптосистем, поиск коллизий в хеш-функциях и атаки на протоколы аутентификации могут быть сведены к SAT. Например, атака на шифр AES с помощью SAT-решателей требует построения гигантской КНФ-формулы, описывающей все раунды шифрования.

Сложность и открытые вопросы

NP-полнота

SAT — NP-полная задача, что означает: если существует полиномиальный алгоритм для SAT, то P = NP. На практике, несмотря на экспоненциальную сложность в худшем случае, современные SAT-решатели успешно обрабатывают формулы с миллионами переменных и дизъюнктов благодаря развитым эвристикам и структурированности реальных задач.

Теоретическая граница

Существуют классы формул, для которых SAT решается быстро (например, 2-SAT, Horn-SAT). Однако для 3-SAT и общего случая не известно алгоритмов, работающих быстрее экспоненциального времени \( O(2^n) \). Лучшие известные алгоритмы для 3-SAT имеют сложность около \( O(1.307^n) \) (алгоритм Шёнинга).

Практическая эффективность

Современные SAT-решатели (например, Kissat, CaDiCaL) демонстрируют впечатляющую производительность на задачах из промышленности и верификации. Ежегодные соревнования SAT Competition стимулируют развитие новых алгоритмов и эвристик.

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

• Задача SAT была введена Стивеном Куком в 1971 году, но её частные случаи изучались ещё в 1950-х годах в контексте логических схем.
• Первый эффективный SAT-решатель, основанный на CDCL, — GRASP (1996) — произвёл революцию в области автоматического доказательства.
• В 2010 году SAT-решатели помогли доказать гипотезу о раскраске графов (проблема четырёх красок) для некоторых частных случаев.
• Задача SAT является одной из немногих NP-полных задач, для которых существуют коммерчески успешные инструменты, используемые в промышленности.

Источники

• Кук С. Сложность процедур доказательства теорем (1971).
• Arora S., Barak B. Computational Complexity: A Modern Approach (2009).
• Biere A., Heule M., van Maaren H., Walsh T. Handbook of Satisfiability (2009).
• Gomes C. P., Selman B. Algorithmic Methods for Satisfiability (2001).
• Документация SAT-решателей MiniSat, Glucose, Z3.