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

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

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

Точная формулировка

Чтобы точно сформулировать задачу распознавания , фиксируется конечный алфавит, с помощью которого задаются экземпляры языка. Хопкрофт , Мотвани и Ульман в книге ( англ. ) предлагают использовать следующий алфавит: ${\displaystyle \{\wedge ,\vee ,\neg ,(,),x,0,1\}}$ .

При использовании такого алфавита скобки и операторы записываются естественным образом, а переменные получают следующие имена: ${\displaystyle x1,x10,x11,x100,\dots }$ , согласно их номерам в двоичной записи .

Пусть некоторая булева формула , записанная в обычной математической нотации, имела длину ${\displaystyle N}$ символов. В ней каждое вхождение каждой переменной было описано хотя бы одним символом, следовательно, всего в данной формуле не более ${\displaystyle N}$ переменных. Значит, в предложенной выше нотации каждая переменная будет записана с помощью ${\displaystyle O\left(\log {N}\right)}$ символов. В таком случае, вся формула в новой нотации будет иметь длину ${\displaystyle O\left(N\log {N}\right)}$ символов, то есть длина строки возрастет в полиномиальное число раз.

Например, формула ${\displaystyle a\wedge \neg (b\vee c)}$ примет вид ${\displaystyle x1\wedge \neg (x10\vee x11)}$ .

Вычислительная сложность

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

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

Частные случаи задачи SAT

Интересными важными частными случаями задачи SAT являются:

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

CDCL-решатели

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

См. также

• Satisfiability Modulo Theories
• SAT@home

Примечания

Ссылки

• — общий сайт о SAT.