Формулировка
Теорема Кука—Левина: язык выполнимых КНФ является NP-полным. Эквивалентно, SAT принадлежит \(NP\), и всякий язык \(L\in NP\) полиномиально сводится к SAT.1, 2
Кодирование вычисления КНФ
Пусть НМТ \(M\) распознаёт язык \(L\) за время, ограниченное полиномом \(p(n)\). Для слова \(w\) длины \(n\) рассматривают первые \(T=p(n)\) шагов и первые \(T\) ячеек ленты. Вводятся булевы переменные трёх типов: переменная \(P^i_{s,t}\) сообщает, что в ячейке \(s\) на шаге \(t\) записан символ \(a_i\). Переменная \(Q^j_t\) задаёт состояние \(q_j\). Переменная \(S_{s,t}\) указывает положение головки.1
Затем строится КНФ, выражающая условия корректной таблицы вычисления. Одни группы скобок требуют ровно одного обозреваемого места, одного символа в ячейке и одного состояния. Другие фиксируют начальную конфигурацию. Локальные условия проверяют соответствие переходов программе машины. Заключительная часть требует появления принимающего состояния.
Такая КНФ выполнима тогда и только тогда, когда существует принимающая ветвь вычисления \(M\) на \(w\). При \(T=p(n)\) пространственно-временная таблица имеет порядка \(T^2\) позиций; алфавит, множество состояний и локальное правило фиксированы, поэтому число переменных и локальных ограничений растёт лишь полиномиально. Размер формулы и время её построения полиномиальны по \(|w|\), поэтому получается сведение \(L\prec SAT\). Именно этот подсчёт исключает скрытый экспоненциальный рост редукции.1
Принадлежность SAT классу NP
Удовлетворяющий набор значений переменных служит кратким свидетельством выполнимости. В модели НМТ значения можно недетерминированно выбрать, после чего вычислить значение КНФ за полиномиальное время. Поэтому \(SAT\in NP\).2