Задача о выполнимости (SAT): Абсолютный фундамент теории сложности

Формулировка задачи SAT обманчиво проста. На вход дается гигантская логическая формула (булево выражение), состоящая из переменных (принимающих значения 1 или 0) и логических связок И (AND), ИЛИ (OR), НЕ (NOT). Требуется ответить на один вопрос: существует ли такой набор значений переменных, при котором вся формула в целом будет равна 1 (Истина)?

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

В 1971 году математик Стивен Кук (а независимо от него в СССР — Леонид Левин) доказал эпохальную теорему. Теорема Кука-Левина гласит: любая задача из класса NP может быть переведена (сведена) к задаче SAT за полиномиальное время. Доказательство было гениальным: Кук показал, что саму внутреннюю логику работы Машины Тьюринга, ее ленту, состояния и правила перехода можно закодировать одной гигантской булевой формулой. Если мы научимся быстро решать SAT, мы автоматически научимся быстро решать вообще все NP-задачи (произойдет революция P=NP).

Хотя SAT является NP-полной и для нее не существует быстрого математического решения (в худшем случае), на практике индустрия не могла ждать. Инженерам необходимо проверять микросхемы, содержащие миллиарды транзисторов, на отсутствие логических ошибок и замыканий. Для этого были созданы SAT-солверы (SAT solvers).

Современные SAT-солверы не используют тупой полный перебор. Они применяют сложнейшие алгоритмы дискретной оптимизации, такие как CDCL (Conflict-Driven Clause Learning — обучение на конфликтах). Когда алгоритм упирается в логическое противоречие, он анализирует граф зависимостей, находит причину конфликта и математически генерирует новое логическое правило (новый клоз), которое добавляет к исходной формуле. Это правило гарантирует, что алгоритм больше никогда в будущем не наступит на те же грабли. Благодаря этому современные программы способны за минуты решать задачи SAT с миллионами переменных, обеспечивая надежность процессоров от Intel и AMD.