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

---

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

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

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

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

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

---