Задача SAT¶

Задача SAT (от англ. Boolean satisfiability problem, задача выполнимости булевых формул) — это фундаментальная задача теории вычислительной сложности и математической логики, заключающаяся в определении, существует ли набор значений переменных, при котором заданная булева формула принимает значение «истина». Формально, для данной пропозициональной формулы \( F \) над множеством булевых переменных \( x_1, x_2, \dots, x_n \) требуется установить, существует ли такая интерпретация (присваивание каждой переменной значения 0 или 1), что \( F \) истинна. Задача SAT является первой и центральной NP-полной задачей, доказательство чего было получено Стивеном Куком в 1971 году (теорема Кука — Левина). Она лежит в основе теории NP-полноты и имеет огромное практическое значение в автоматическом доказательстве теорем, верификации программного обеспечения, планировании, криптографии и искусственном интеллекте.

¶История

¶Ранние этапы

Истоки задачи SAT восходят к работам Алана Тьюринга и Алонзо Чёрча по разрешимости формальных систем (1930-е годы). В 1950-х годах задача стала рассматриваться в контексте автоматического доказательства теорем в логике высказываний. Первые алгоритмы, такие как метод Дэвиса — Патнема (1960), были предложены для проверки выполнимости формул в конъюнктивной нормальной форме (КНФ).

¶Теорема Кука — Левина

В 1971 году Стивен Кук в работе «The Complexity of Theorem-Proving Procedures» доказал, что задача SAT является NP-полной. Это означает, что любая задача из класса NP может быть сведена к SAT за полиномиальное время, и если для SAT существует полиномиальный алгоритм, то все задачи класса NP решаются за полиномиальное время (P = NP). Независимо от Кука, аналогичный результат получил Леонид Левин в 1973 году. Это открытие сделало SAT центральной задачей теории сложности.

¶Развитие алгоритмов

В 1970–1980-х годах были разработаны первые эффективные алгоритмы для SAT, включая метод DPLL (Дэвис — Патнем — Логеманн — Ловленд, 1962), который стал основой для большинства современных SAT-решателей. В 1990-х годах появились алгоритмы на основе локального поиска (например, GSAT, WalkSAT). С 2000-х годов активно развиваются конфликтно-ориентированные решатели (CDCL, Conflict-Driven Clause Learning), которые значительно превзошли предыдущие методы по производительности.

¶Формальное определение

Пусть задана булева формула \( F \) в конъюнктивной нормальной форме (КНФ), то есть конъюнкция дизъюнктов (клауз), каждый из которых является дизъюнкцией литералов (переменных или их отрицаний). Задача SAT: существует ли такое присваивание значений переменным (0 или 1), что каждый дизъюнкт содержит хотя бы один истинный литерал? Если такое присваивание существует, формула называется выполнимой (SAT), иначе — невыполнимой (UNSAT).

Пример: формула \( (x_1 \lor x_2) \land (\neg x_1 \lor x_3) \land (\neg x_2 \lor \neg x_3) \) выполнима: присваивание \( x_1 = 1, x_2 = 0, x_3 = 0 \) делает все дизъюнкты истинными.

¶Классификация

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

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

¶По типу переменных

• Булева SAT — переменные принимают значения 0/1.
• SAT с целочисленными переменными — обобщение на конечные домены.
• SAT с вещественными переменными — задача выполнимости арифметических формул (SMT, Satisfiability Modulo Theories).

¶По сложности

• NP-полные — SAT, 3-SAT, MAX-SAT (максимизация числа истинных дизъюнктов).
• Полиномиальные — 2-SAT, HORN-SAT (каждый дизъюнкт содержит не более одного положительного литерала).

¶Устройство SAT-решателей

¶Алгоритмы полного перебора (DPLL/CDCL)

• DPLL (Davis–Putnam–Logemann–Loveland) — рекурсивный алгоритм, основанный на последовательном присваивании значений переменным и распространении единичных дизъюнктов (unit propagation). Если возникает конфликт (пустой дизъюнкт), происходит возврат (backtracking).
• CDCL (Conflict-Driven Clause Learning) — развитие DPLL, в котором при конфликте извлекается причина (конфликтная клауза), которая добавляется в базу знаний, что позволяет избегать повторения тех же ошибок. Современные решатели (MiniSAT, Glucose, Lingeling) используют CDCL, эвристики выбора переменных (VSIDS, Variable State Independent Decaying Sum) и перезапуски.

¶Алгоритмы локального поиска

• GSAT (Greedy SAT) — начинается со случайного присваивания, затем переворачивает значение переменной, максимизирующее число истинных дизъюнктов.
• WalkSAT — добавляет элемент случайности: с вероятностью \( p \) выбирает случайную переменную из невыполненного дизъюнкта, иначе — переменную, минимизирующую число нарушенных дизъюнктов. Эти алгоритмы не гарантируют полноты (могут не найти решение, даже если оно существует), но эффективны для больших случайных формул.

¶Решатели на основе SMT

• SMT-решатели (Z3, CVC4, Yices) расширяют SAT на более выразительные теории: арифметику, массивы, битовые векторы, равенства. Они используют SAT-решатель как ядро, а для каждой теории применяют специализированные процедуры (теории).

¶Применение

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

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

¶Планирование и составление расписаний

• Планирование задач (SAT-планирование) — задачи планирования действий (например, в робототехнике) сводятся к SAT, где переменные кодируют состояния и действия во времени.
• Составление расписаний — задачи календарного планирования, распределения ресурсов (например, в логистике).

¶Криптография

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

¶Искусственный интеллект

• Автоматическое доказательство теорем — SAT-решатели используются в системах логического вывода (например, в системе E, Vampire).
• Рассуждения о знаниях — задачи логического вывода в базах знаний (например, в описательных логиках).

¶Биоинформатика

• Анализ генетических данных — задачи гаплотипирования, предсказания структуры белков, проверки согласованности генетических моделей.

¶Примеры

¶2-SAT

Задача 2-SAT, где каждый дизъюнкт содержит ровно два литерала, решается за полиномиальное время с помощью построения графа импликаций и поиска сильно связных компонент (алгоритм Косарайю или Тарьяна). Пример: формула \( (x_1 \lor x_2) \land (\neg x_1 \lor x_3) \) выполнима.

¶3-SAT

3-SAT является NP-полной. Пример: формула \( (x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor \neg x_2 \lor x_3) \land (x_1 \lor \neg x_2 \lor \neg x_3) \) — выполнима при \( x_1 = 1, x_2 = 0, x_3 = 1 \).

¶MAX-SAT

Задача MAX-SAT заключается в нахождении присваивания, максимизирующего число истинных дизъюнктов. Это NP-трудная задача, используемая в задачах оптимизации.

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

• Вычислительная сложность — SAT является NP-полной, поэтому в худшем случае все известные алгоритмы требуют экспоненциального времени. Для больших формул (миллионы переменных) современные решатели могут быть неэффективны.
• Практическая применимость — хотя SAT-решатели успешно решают многие задачи, они чувствительны к структуре формулы: случайные формулы большого размера могут быть трудноразрешимыми, а структурированные (например, из верификации) — решаются быстрее.
• Зависимость от эвристик — эффективность решателей сильно зависит от эвристик выбора переменных и перезапусков, что делает их поведение непредсказуемым для некоторых классов формул.
• Проблема памяти — CDCL-решатели могут генерировать огромное количество конфликтных клауз, что приводит к переполнению памяти.

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

• В 2010 году SAT-решатель MiniSAT был использован для решения задачи о раскраске карты (четырехцветная теорема), что подтвердило её корректность.
• Ежегодно проводится международный конкурс SAT-решателей (SAT Competition), где соревнуются лучшие алгоритмы.
• Задача SAT является одной из семи «задач тысячелетия» (гипотеза P vs NP), решение которой принесёт миллион долларов от Института Клэя.
• Существует проект «SAT@home» (распределённые вычисления), где добровольцы помогают решать сложные SAT-задачи.

¶Источники

• Cook, S. A. (1971). «The Complexity of Theorem-Proving Procedures». Proceedings of the 3rd 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.
• Marques-Silva, J., & Sakallah, K. A. (1999). «GRASP: A Search Algorithm for Propositional Satisfiability». IEEE Transactions on Computers.