10
правок
Изменения
Нет описания правки
=== Определение ===
Проблема <mathtex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</mathtex> — проблема выполнимости булевых формул.
Докажем, что эта проблема <mathtex>NP\,\!</mathtex>-полна.
== Формулировка ==
'''Теорема Кука''' гласит, что <mathtex>SAT \in NPC.</mathtex>
== Доказательство ==
<mathtex>SAT \in NPC</mathtex>, если*<mathtex>SAT \in NP</mathtex>*<mathtex>SAT \in NPH</mathtex>Прежде всего докажем, что <mathtex>SAT \in NP.</mathtex>
Так как <mathtex>NP = \Sigma_1\,\!</mathtex>, то достаточно показать, что <mathtex>SAT \in \Sigma_1</mathtex>
В качестве сертификата берём набор нулей и единиц в количестве <mathtex>n\,\!</mathtex> штук, соответствующих значениям аргументов функции <mathtex>\phi\,\!</mathtex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <mathtex>\phi\,\!</mathtex>.
Верификатор просто подставит эти значения в формулу <mathtex>\phi\,\!</mathtex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.
Если же у нас существует такой сертификат <mathtex>y\,\!</mathtex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.
Теперь докажем, что <mathtex>SAT \in NPH.</mathtex> Для этого сведём проблему <mathtex>BH_{1N}\,\!</mathtex>, которая, как нам известно, <mathtex>NP\,\!</mathtex>-полна, к проблеме <mathtex>SAT.\,\!</mathtex> Тогда получится, что любая проблема из <mathtex>NP\,\!</mathtex> может быть сведена по Карпу к проблеме <mathtex>BH_{1N}\,\!</mathtex>, и, по транзитивности сведения по Карпу, к <mathtex>SAT.\,\!</mathtex>
По условию проблемы <mathtex>BH_{1N}\,\!</mathtex>, у нас есть недетерминированная машина Тьюринга <mathtex>m\,\!</mathtex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <mathtex>x\,\!</mathtex> и время <mathtex>t\,\!</mathtex>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <mathtex>\phi\,\!</mathtex>, что она выполнима тогда, и только тогда, когда <mathtex>m\,\!</mathtex>, получив на вход <mathtex>x\,\!</mathtex>, делает не более <mathtex>t\,\!</mathtex> шагов и допускает это слово.
В любой момент времени мгновенное описание (МО) <mathtex>m\,\!</mathtex> есть строка <mathtex>z\#_qyb</mathtex>, где <mathtex>b\,\!</mathtex> — строка, состоящая из такого количества пробелов, чтобы длина всего МО была <mathtex>t + 1.\,\!</mathtex> Соответственно, начальное МО задаётся так : <mathtex>\#_sx\,\!</mathtex>. Если же <mathtex>|x| > t\,\!</mathtex>, то будем считать, что на ленту записаны лишь первые <mathtex>t\,\!</mathtex> символов, ведь <mathtex>m\,\!</mathtex> не может обработать большее количество символов за <mathtex>t\,\!</mathtex> шагов.
Также нам удобно считать, что все вычисления проходят ровно за <mathtex>t + 1\,\!</mathtex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <mathtex>q \vdash q</mathtex>, если в МО <mathtex>q\,\!</mathtex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <mathtex>q_t\,\!</mathtex>.
Тогда процесс работы машины <mathtex>m\,\!</mathtex> на входе <mathtex>x\,\!</mathtex>, то есть цепочка переходов <mathtex>q_0 \vdash q_1 \vdash ... \vdash q_t</mathtex> может быть представлен следующей таблицей :
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"
|+ '''Процесс работы машины <mathtex>m\,\!</mathtex> на входе <mathtex>x\,\!</mathtex>'''
|-
! width="50" style="border-right:3px solid gray; border-bottom:3px solid gray;" | MO !! width="50" style="border-bottom:3px solid gray;"| 0 !! width="50" style="border-bottom:3px solid gray;" | 1 !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | t
|- style="height:50px;"
! style="border-right:3px solid gray;" | <mathtex>q_0\,\!</mathtex>| <mathtex>q_{0, 0}\,\!</mathtex> || <mathtex>q_{0, 1}\,\!</mathtex> || || || || || || || <mathtex>q_{0, t}\,\!</mathtex>
|- style="height:50px"
! style="border-right:3px solid gray;" | <mathtex>q_1\,\!</mathtex>| <mathtex>q_{1, 0}\,\!</mathtex> || <mathtex>q_{1, 1}\,\!</mathtex> || || || || || || || <mathtex>q_{1, t}\,\!</mathtex>
|- style="height:30px"
! style="border-right:3px solid gray;" | ... || || || || || || || || ||
|- style="height:50px"
! style="border-right:3px solid gray;" | <mathtex>q_i\,\!</mathtex>| || || || <mathtex>q_{i, j - 1}\,\!</mathtex> || <mathtex>q_{i, j}\,\!</mathtex> || <mathtex>q_{i, j + 1\,\!}</mathtex> || <mathtex>q_{i, j + 2\,\!}</mathtex> || ||
|- style="height:50px"
! style="border-right:3px solid gray;" | <mathtex>q_{i + 1}\,\!</mathtex>| || || || <mathtex>q_{i, j - 1}\,\!</mathtex> || <mathtex>q_{i, j}\,\!</mathtex> || <mathtex>q_{i, j + 1\,\!}</mathtex> || || ||
|- style="height:30px"
! style="border-right:3px solid gray;" | ... || || || || || || || || ||
|- style="height:50px"
! style="border-right:3px solid gray;" | <mathtex>q_t\,\!</mathtex>| <mathtex>q_{t, 0}\,\!</mathtex> || <mathtex>q_{t, 1}\,\!</mathtex> || || || || || || || <mathtex>q_{t, t}\,\!</mathtex>
|}
Каждый элемент таблицы <mathtex>q_{i, j}\in \Sigma \cup Q</mathtex>. И для каждого такого элемента заведём <mathtex>|\Sigma| + |Q|\,\!</mathtex> переменных <mathtex>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q\,\!</mathtex>
Общий вид формулы : <mathtex>\phi = S \and land T \and land N \and land C</mathtex>
