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

Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача.

Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций  (И),  (ИЛИ) и  (HE).
Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.

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

Точная формулировка 
Чтобы точно сформулировать задачу распознавания, фиксируется конечный алфавит, с помощью которого задаются экземпляры языка. Хопкрофт, Мотвани и Ульман в книге  предлагают использовать следующий алфавит: .

При использовании такого алфавита скобки и операторы записываются естественным образом, а переменные получают следующие имена: , согласно их номерам в двоичной записи.

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

Например, формула  примет вид .

Вычислительная сложность 
В 1970-м году в статье Стивена Кука был впервые введен термин «NP-полная задача», и задача SAT была первой задачей, для которой доказывалось это свойство.

В доказательстве теоремы Кука каждая задача из класса NP в явном виде сводится к SAT. После появления результатов Кука была доказана NP-полнота для множества других задач. При этом чаще всего для доказательства NP-полноты некоторой задачи приводится полиномиальная сводимость задачи SAT к данной задаче, возможно в несколько шагов, то есть с использованием нескольких промежуточных задач.

Частные случаи задачи SAT 
Интересными важными частными случаями задачи SAT являются:
 задача выполнимости булевых формул в конъюнктивной нормальной форме (SATCNF или ВКНФ) — аналогичная задача, с наложенным на формулу условием: она должна быть записана в конъюнктивной нормальной форме; также NP-полна;
 задача выполнимости булевых формул в k-конъюнктивной нормальной форме (k-SAT или k-ВЫП) — задача выполнимости при условии, что формула записана в k-конъюнктивной нормальной форме; эта задача является NP-полной при . Для решения задачи можно воспользоваться вероятностным алгоритмом Шёнинга;
 задача выполнимости булевых формул в 2-конъюнктивной нормальной форме имеет полиномиальное решение, то есть принадлежит классу P.

CDCL-решатели 

Одним из наиболее эффективных методов распараллеливания задач SAT являются CDCL-решатели (CDCL, ), основывающиеся на нехронологических вариантах алгоритма DPLL.

См. также 
 Satisfiability Modulo Theories
 SAT@home

Примечания

Ссылки 
 The international SAT Competitions web page
 Sat Live — общий сайт о SAT.

Булева алгебра
NP-полные задачи
Формальные методы
Задача выполнимости булевых формул