SAT-решатели

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

История

Ранние этапы

Первые работы по задаче SAT относятся к 1950-м годам, когда она была формализована в контексте логики высказываний. В 1960 году Мартин Дэвис и Хиллари Патнэм предложили алгоритм DP (Davis–Putnam), основанный на правиле резолюции. В 1962 году Дэвис, Логеманн и Ловленд модифицировали его в алгоритм DPLL (Davis–Putnam–Logemann–Loveland), который стал основой для большинства последующих SAT-решателей. DPLL использует поиск с возвратом (backtracking) и эвристики для выбора переменных.

Развитие в 1990-х годах

В 1990-е годы произошёл прорыв благодаря внедрению методов обучения на конфликтах (conflict-driven clause learning, CDCL). Алгоритм CDCL, предложенный в работах Жуана Маркеса-Сильвы и Карима Сакаллаха (1996), позволил SAT-решателям запоминать причины неудачных ветвлений и добавлять новые клаузулы, что радикально сократило пространство поиска. Первые коммерческие и академические CDCL-решатели (например, GRASP, Chaff) продемонстрировали высокую производительность на практических задачах.

Современный этап

С 2000-х годов SAT-решатели стали стандартным инструментом в промышленности. Ежегодные соревнования SAT Competition стимулируют развитие алгоритмов. Современные решатели (например, MiniSat, Glucose, CaDiCaL, Kissat) используют сложные эвристики, такие как VSIDS (Variable State Independent Decaying Sum), фазы перезапуска, и эффективные структуры данных (двухлитеральные наблюдения). В 2020-х годах появились гибридные подходы, сочетающие SAT с методами машинного обучения и параллельными вычислениями.

Алгоритмы и методы

Классические алгоритмы

• Алгоритм DPLL — рекурсивный поиск с возвратом. На каждом шаге выбирается переменная, ей присваивается значение (истина или ложь), затем формула упрощается (правило единичной клаузулы, правило чистого литерала). Если возникает конфликт (пустая клаузула), происходит откат.
• Алгоритм CDCL — развитие DPLL. После конфликта анализируется его причина, строится новая клаузула (clause learning), которая добавляется в формулу. Это предотвращает повторение тех же ошибок. Также используются перезапуски (restarts) — периодический сброс текущего состояния для выхода из локальных тупиков.

Эвристики и оптимизации

• Выбор переменной — эвристика VSIDS (Variable State Independent Decaying Sum) присваивает каждой переменной вес, который увеличивается при участии в конфликтах. Веса периодически уменьшаются, чтобы фокусироваться на недавних конфликтах.
• Двухлитеральные наблюдения (two-watched literals) — структура данных, позволяющая быстро определять, какие клаузулы стали единичными или пустыми после присваивания.
• Фазы перезапуска — стратегии, определяющие, когда и как часто выполнять перезапуск (например, геометрические или Luby-последовательности).
• Предварительная обработка (preprocessing) — упрощение формулы до основного поиска: удаление тавтологий, подстановка единичных клаузул, поглощение, переменное исключение (bounded variable elimination).

Полные и неполные решатели

• Полные SAT-решатели — гарантируют нахождение решения или доказательство невыполнимости (например, все CDCL-решатели). Используются для задач, где требуется точный ответ.
• Неполные SAT-решатели — основаны на локальном поиске (например, WalkSAT, GSAT). Они не гарантируют нахождение решения, но часто быстрее находят выполнимые наборы для больших формул. Применяются в задачах, где важна скорость, а не гарантия.

Архитектура и реализация

Типичная структура

Современный SAT-решатель состоит из:

• Модуля ввода/вывода — чтение формулы в формате DIMACS (стандартный текстовый формат для КНФ).
• Препроцессора — упрощение формулы (например, удаление дублирующихся клаузул, подстановка).
• Ядра поиска — реализация CDCL с эвристиками, управлением памятью и обработкой конфликтов.
• Модуля управления перезапусками — стратегия перезапусков.
• Модуля обучения клаузулам — анализ конфликтов и генерация новых клаузул.

Формат DIMACS

Формат DIMACS (от Center for Discrete Mathematics and Theoretical Computer Science) является стандартом для обмена SAT-задачами. Файл начинается со строки p cnf <число переменных> <число клаузул>, затем следуют строки с клаузулами, где переменные обозначаются целыми числами (отрицательное число — отрицание литерала), каждая клаузула заканчивается нулём. Пример: `` p cnf 3 2 1 -2 0 -1 3 0 `` Эта формула соответствует (x1 ∨ ¬x2) ∧ (¬x1 ∨ x3).

Применение

Верификация и тестирование

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

Планирование и задачи ИИ

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

Криптоанализ

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

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

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

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

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

Производительность и соревнования

SAT Competition

Ежегодное международное соревнование SAT Competition (проводится с 2002 года) является основным бенчмарком для оценки SAT-решателей. Участники предоставляют решатели, которые тестируются на наборах задач из промышленности, криптографии, планирования и случайных формул. Победители в разных категориях (основная, параллельная, инкрементальная) определяют современное состояние области.

Факторы производительности

Производительность SAT-решателя зависит от:

• Качества эвристик — алгоритмы выбора переменных и обучения клаузулам.
• Эффективности структур данных — скорость обработки клаузул и присваиваний.
• Предварительной обработки — степень упрощения формулы.
• Параллельных вычислений — использование нескольких ядер или GPU (например, решатели Plingeling, CryptoMiniSat).

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

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

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

Практические проблемы

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

Список известных SAT-решателей

• MiniSat (2003) — открытый решатель, ставший эталоном для академических исследований. Написан на C++.
• Glucose (2009) — улучшенная версия MiniSat с продвинутыми эвристиками удаления клаузул.
• CaDiCaL (2017) — современный решатель, победитель SAT Competition 2017–2020. Использует адаптивные эвристики.
• Kissat (2020) — решатель, разработанный Армином Биере и Мартином Хоффером. Отличается высокой производительностью на промышленных задачах.
• WalkSAT (1994) — неполный решатель на основе локального поиска, используется для больших выполнимых формул.
• CryptoMiniSat (2010) — решатель с поддержкой инкрементального SAT и специализированными эвристиками для криптографических задач.

Источники

• Marques-Silva, J., & Sakallah, K. A. (1996). GRASP—A new search algorithm for satisfiability. Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design.
• Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). Handbook of Satisfiability. IOS Press.
• Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394–397.
• SAT Competition. (2002–2024). SAT Competition Proceedings.
• Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. Proceedings of the 38th Design Automation Conference.