Теорема Кука — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показано 30 промежуточных версий 7 участников)
Строка 1: Строка 1:
=== Определение ===
+
== Определение ==
Проблема <math>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</math> &mdash; проблема выполнимости булевых формул.
+
<tex> \mathrm{SAT}</tex> {{---}} язык булевых формул из <tex> n </tex> переменных, для которых существует подстановка, при которой формула истинна.
  
Докажем, что эта проблема <math>NP\,\!</math>-полна.
+
<tex> \mathrm{SAT} = \lbrace \varphi \mid \exists x : \varphi(x) = 1 \rbrace </tex>
 +
== Теорема Кука ==
 +
{{Теорема
 +
|author=Кук
 +
|statement=<tex> \mathrm{SAT}\in \mathrm{NPC} </tex>
 +
|proof=
 +
# <tex> \mathrm{SAT}\in \mathrm{NP} </tex> <br>Можно написать недетерминированную программу <tex>p</tex>, которая распознает язык <tex> \mathrm{SAT} </tex>. Она будет недетерминированно выбирать подстановку, проверять, истинна ли формула при такой подстановке, и выдавать ответ.
 +
# <tex> \mathrm{SAT}\in \mathrm{NPH} </tex> <br> Теперь докажем, что <tex> \mathrm{SAT}\in \mathrm{NPH} </tex>. Для этого сведём задачу <tex> \mathrm{BH_{1N}} </tex>, которая <tex> \mathrm{NP} </tex>-полна, к <tex> \mathrm{SAT} </tex>. Тогда получится, что любой язык из <tex> \mathrm{NP} </tex> может быть [[Сведение относительно класса функций. Сведение по Карпу. Трудные и полные задачи|сведен по Карпу]] к <tex> \mathrm{BH_{1N}} </tex>, и, по транзитивности сведения по Карпу, к <tex> \mathrm{SAT} </tex>. <br> По определению языка <tex> \mathrm{BH_{1N}} </tex>, у нас есть:
 +
#* недетерминированная машина Тьюринга <tex>m</tex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы
 +
#* входное слово <tex>x</tex>
 +
#* время <tex>t</tex>, заданное в унарной системе счисления.
 +
::Нам же надо построить такую булеву формулу <tex>\varphi</tex>, что она выполнима тогда, и только тогда, когда <tex>m</tex>, получив на вход <tex>x</tex>, делает не более <tex>t</tex> шагов и допускает это слово. <br> В любой момент времени мгновенное описание (МО) <tex>m</tex> есть строка <tex>z\#_qyb</tex>, где <tex>b</tex> &mdash; строка, состоящая из такого количества пробелов, чтобы длина всего МО была <tex>t + 1.</tex> Соответственно, начальное МО задаётся так: <tex>\#_sxb</tex>. Если же <tex>|x| > t</tex>, то будем считать, что на ленту записаны лишь первые <tex>t</tex> символов, ведь <tex>m</tex> не может обработать большее количество символов за <tex>t</tex> шагов. <br> Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t</tex>. <br> Тогда процесс работы машины <tex>m</tex> на входе <tex>x</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash \ldots \vdash q_t</tex> может быть представлен следующей таблицей :
 +
<table align="right" border="1" style="text-align:center" cellspacing="0">
 +
<tr>
 +
<td colspan=10>
 +
'''Процесс работы машины <tex>m</tex> на входе <tex>x</tex>'''
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
MO
 +
</td>
 +
<td width="50" >
 +
0
 +
</td>
 +
<td width="50">
 +
1
 +
</td>
 +
<td  width="30">
 +
...
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
...
 +
</td>
 +
<td width="50">
 +
t
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
<tex>q_0</tex>
 +
</td>
 +
<td width="50" >
 +
<tex>q_{0, 0}</tex>
 +
</td>
 +
<td width="50">
 +
<tex>q_{0, 1}</tex>
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
<tex>q_{0, t}</tex>
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
<tex>q_1</tex>
 +
</td>
 +
<td width="50" >
 +
<tex>q_{1, 0}</tex>
 +
</td>
 +
<td width="50">
 +
<tex>q_{1, 1}</tex>
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
<tex>q_{1, t}</tex>
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
...
 +
</td>
 +
<td width="50" >
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
<tex> q_i </tex>
 +
</td>
 +
<td width="50" >
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
<tex> q_{i, j - 1} </tex>
 +
</td>
 +
<td width="50">
 +
<tex> q_{i, j} </tex>
 +
</td>
 +
<td width="50">
 +
<tex> q_{i, j + 1} </tex>
 +
</td>
 +
<td width="50">
 +
<tex> q_{i, j + 2} </tex>
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
<tex> q_{i+1} </tex>
 +
</td>
 +
<td width="50" >
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
<tex> q_{i+1, j - 1} </tex>
 +
</td>
 +
<td width="50">
 +
<tex> q_{i+1, j} </tex>
 +
</td>
 +
<td width="50">
 +
<tex> q_{i+1, j + 1} </tex>
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
...
 +
</td>
 +
<td width="50" >
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
</tr>
 +
<tr>
 +
<td width="50">
 +
<tex>q_t</tex>
 +
</td>
 +
<td width="50" >
 +
<tex>q_{t, 0}</tex>
 +
</td>
 +
<td width="50">
 +
<tex>q_{t, 1}</tex>
 +
</td>
 +
<td  width="30">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="50">
 +
</td>
 +
<td width="30">
 +
</td>
 +
<td width="50">
 +
<tex>q_{t, t}</tex>
 +
</td>
 +
</tr>
 +
</table>
  
== Формулировка ==
+
::Каждый элемент таблицы <tex>q_{i, j}\in \Sigma \cup Q</tex>. И для каждого такого элемента заведём <tex>|\Sigma| + |Q|</tex> переменных <tex>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q</tex> <br> Общий вид формулы: <tex>\varphi = S \land T \land N \land C</tex>.
'''Теорема Кука''' гласит, что <math>SAT \in NPC.</math>
+
::# <tex>S</tex> отвечает за правильный старт, то есть символ <tex>q_{0,0}</tex> должен быть начальным состоянием <tex>\#_s</tex> машины <tex>m</tex>, символы с <tex>q_{0,1}</tex> по <tex>q_{0,|x|}</tex> &mdash; образовывать цепочку <tex>x</tex>, а оставшиеся <tex>q_{0,i}</tex> &mdash; быть пробелами <tex>B</tex>. Таким образом, <tex>S = Y_{0,0,\#_s} \land Y_{0,1,x_1} \land \ldots \land Y_{0,|x|+1,B} \land \ldots \land Y_{0,t,B}</tex>.
 +
::# <tex>T</tex> отвечает за правильный финиш, то есть в МО <tex>q_t</tex> должно присутствовать допускающее состояние <tex>\#_y</tex>, следовательно <tex>T = Y_{t,0,\#_y} \lor Y_{t,1,\#_y} \lor \ldots \lor Y_{t,t,\#_y}</tex>.
 +
::# <tex>N</tex> отвечает за то, что машина <tex>m</tex> делает правильные переходы. <tex>q_{i,j}</tex> зависит только от четырех символов над ним, то есть от <tex>q_{i-1,j-1}, q_{i-1,j}, q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex>. Тогда для проверки корректности переходов требуется перебрать все четверки символов <tex>q_{i-1,j-1}, q_{i-1,j}, q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex> из таблицы и проверить, что из них возможно получить символ <tex>q_{i,j}</tex>. Если четверка символов выходит за границу таблицы, то указывается меньшее количество позиций. С учетом того, что машина <tex>m</tex> недетерминирована и требуется устранить возможность раздвоения ее головки, сделаем все возможные выводы о новых символах <tex>q_{i,j \pm 1}</tex>: <br> <tex>N = \land_{i=0..t,j=0..t} \land_{c_1 \ldots c_4} (( Y_{i-1,j-1,c_1} \land Y_{i-1,j,c_2} \land Y_{i-1,j+1,c_3} \land Y_{i-1,j+2,c_4} ) \to ((Y_{i,j-1,c_0^`} \lor Y_{i,j-1,c_1^`} \lor \ldots \lor Y_{i,j-1,c_{|\Sigma|+|Q|-1}^`}) \land (Y_{i,j,c_0^`} \lor Y_{i,j,c_1^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|+|Q|-1}^`}) \land (Y_{i,j+1,c_0^`} \lor Y_{i,j+1,c_1^`} \lor \ldots \lor Y_{i,j+1,c_{|\Sigma|+|Q|-1}^`})))</tex>.
 +
::# <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''.<br> <tex>C = \land_{i=0..t,j=0..t} ((Y_{i,j,c_1} \land \lnot Y_{i,j,c_2} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|+|Q|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|+|Q|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|+|Q|-2}}))</tex>.
 +
:: Мы построили функцию сведения <tex> f: \langle m, x, 1^t \rangle \mapsto \varphi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\varphi</tex> полиномиально зависит от длины входа &mdash; <tex>|\varphi| = O(n^2)</tex>. <br> Покажем, что <tex>\varphi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle \in  \mathrm{BH_{1N}} </tex>.
 +
:# Пусть <tex>\langle m, x, 1^t \rangle \in  \mathrm{BH_{1N}}</tex>, тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\varphi</tex> примет значение ''истина''.
 +
:# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\varphi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\varphi</tex> на нем принимает значение ''истина''. Тогда по данному набору можем построить таблицу, по которой восстановим допускающую цепочку переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>. Совершив эти переходы машина <tex>m</tex> перейдет в допускающее состояние за время <tex>t</tex>, следовательно <tex>\langle m, x, 1^t\rangle \in \mathrm{BH_{1N}}</tex>.
  
== Доказательство ==
+
:Значит <tex> \mathrm{SAT} \in \mathrm{NPC} </tex>, что и требовалось доказать.
<math>SAT \in NPC</math>, если
 
*<math>SAT \in NP</math>
 
*<math>SAT \in NPH</math>
 
Прежде всего докажем, что <math>SAT \in NP.</math>
 
  
Так как <math>NP = \Sigma_1\,\!</math>, то достаточно показать, что <math>SAT \in \Sigma_1</math>
+
}}
  
В качестве сертификата берём набор нулей и единиц в количестве <math>n\,\!</math> штук, соответствующих значениям аргументов функции <math>\phi\,\!</math>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <math>\phi\,\!</math>.
+
== См. также ==
 
+
*[[NP-полнота BH1N]]
Верификатор просто подставит эти значения в формулу <math>\phi\,\!</math> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.
+
*[[Сведение относительно класса функций. Сведение по Карпу. Трудные и полные задачи]]
 
+
*[[Недетерминированные вычисления]]
Если же у нас существует такой сертификат <math>y\,\!</math>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.
+
[[Категория: Теория сложности]]
 
 
Теперь докажем, что <math>SAT \in NPH.</math> Для этого сведём проблему <math>BH_{1N}\,\!</math>, которая, как нам известно, <math>NP\,\!</math>-полна, к проблеме <math>SAT.\,\!</math> Тогда получится, что любая проблема из <math>NP\,\!</math> может быть сведена по Карпу к проблеме <math>BH_{1N}\,\!</math>, и, соответственно, к <math>SAT.\,\!</math>
 
 
 
По условию проблемы <math>BH_{1N}\,\!</math>, у нас есть недетерминированная машина Тьюринга <math>m\,\!</math>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <math>x\,\!</math> и время <math>t\,\!</math>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <math>\phi\,\!</math>, что она выполнима тогда, и только тогда, когда <math>m\,\!</math>, получив на вход <math>x\,\!</math>, делает не более <math>t\,\!</math> шагов и допускает это слово.
 
 
 
В любой момент времени мгновенное описание (МО) <math>m\,\!</math> есть строка <math>z\#_qyb</math>, где <math>b\,\!</math> &mdash; строка, состоящая из такого количества пробелов, чтобы длина всего МО была <math>t + 1.\,\!</math> Соответственно, начальное МО задаётся так : <math>\#_sx\,\!</math>. Если же <math>|x| > t\,\!</math>, то будем считать, что на ленту записаны лишь первые <math>t\,\!</math> символов, ведь <math>m\,\!</math> не может обработать большее количество символов за <math>t\,\!</math> шагов.
 
 
 
Также нам удобно считать, что все вычисления проходят ровно за <math>t + 1\,\!</math> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <math>q \vdash q</math>, если в МО <math>q\,\!</math> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <math>q_t\,\!</math>.
 
 
 
Тогда процесс работы машины <math>m\,\!</math> на входе <math>x\,\!</math>, то есть цепочка переходов <math>q_0 \vdash q_1 \vdash ... \vdash q_t</math> может быть представлен следующей таблицей :
 
 
 
{| border="1" class="wikitable" style="text-align:center" cellspacing="0"
 
|+ '''Процесс работы машины <math>m\,\!</math> на входе <math>x\,\!</math>'''
 
|-
 
! 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;" | <math>q_0\,\!</math>
 
| <math>q_{0, 0}\,\!</math> || <math>q_{0, 1}\,\!</math> || || || || || || || <math>q_{0, t}\,\!</math>
 
|- style="height:50px"
 
! style="border-right:3px solid gray;" | <math>q_1\,\!</math>
 
| <math>q_{1, 0}\,\!</math> || <math>q_{1, 1}\,\!</math> || || || || || || || <math>q_{1, t}\,\!</math>
 
|- style="height:30px"
 
! style="border-right:3px solid gray;" | ... || || || || || || || || ||
 
|- style="height:50px"
 
! style="border-right:3px solid gray;" | <math>q_i\,\!</math>
 
| || || || <math>q_{i, j - 1}\,\!</math> || <math>q_{i, j}\,\!</math> || <math>q_{i, j + 1\,\!}</math> || <math>q_{i, j + 2\,\!}</math> || ||
 
|- style="height:50px"
 
! style="border-right:3px solid gray;" | <math>q_{i + 1}\,\!</math>
 
| || || || <math>q_{i, j - 1}\,\!</math> || <math>q_{i, j}\,\!</math> || <math>q_{i, j + 1\,\!}</math> || || ||
 
|- style="height:30px"
 
! style="border-right:3px solid gray;" | ... || || || || || || || || ||
 
|- style="height:50px"
 
! style="border-right:3px solid gray;" | <math>q_t\,\!</math>
 
| <math>q_{t, 0}\,\!</math> || <math>q_{t, 1}\,\!</math> || || || || || || || <math>q_{t, t}\,\!</math>
 
|}
 
Каждый элемент таблицы <math>q_{i, j}\in \Sigma \cup Q</math>. И для каждого такого элемента заведём <math>|\Sigma| + |Q|\,\!</math> переменных <math>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q\,\!</math>
 
 
 
Общий вид формулы : <math>\phi = S \and T \and N \and C</math>
 

Текущая версия на 19:26, 4 сентября 2022

Определение

[math] \mathrm{SAT}[/math] — язык булевых формул из [math] n [/math] переменных, для которых существует подстановка, при которой формула истинна.

[math] \mathrm{SAT} = \lbrace \varphi \mid \exists x : \varphi(x) = 1 \rbrace [/math]

Теорема Кука

Теорема (Кук):
[math] \mathrm{SAT}\in \mathrm{NPC} [/math]
Доказательство:
[math]\triangleright[/math]
  1. [math] \mathrm{SAT}\in \mathrm{NP} [/math]
    Можно написать недетерминированную программу [math]p[/math], которая распознает язык [math] \mathrm{SAT} [/math]. Она будет недетерминированно выбирать подстановку, проверять, истинна ли формула при такой подстановке, и выдавать ответ.
  2. [math] \mathrm{SAT}\in \mathrm{NPH} [/math]
    Теперь докажем, что [math] \mathrm{SAT}\in \mathrm{NPH} [/math]. Для этого сведём задачу [math] \mathrm{BH_{1N}} [/math], которая [math] \mathrm{NP} [/math]-полна, к [math] \mathrm{SAT} [/math]. Тогда получится, что любой язык из [math] \mathrm{NP} [/math] может быть сведен по Карпу к [math] \mathrm{BH_{1N}} [/math], и, по транзитивности сведения по Карпу, к [math] \mathrm{SAT} [/math].
    По определению языка [math] \mathrm{BH_{1N}} [/math], у нас есть:
    • недетерминированная машина Тьюринга [math]m[/math], причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы
    • входное слово [math]x[/math]
    • время [math]t[/math], заданное в унарной системе счисления.
Нам же надо построить такую булеву формулу [math]\varphi[/math], что она выполнима тогда, и только тогда, когда [math]m[/math], получив на вход [math]x[/math], делает не более [math]t[/math] шагов и допускает это слово.
В любой момент времени мгновенное описание (МО) [math]m[/math] есть строка [math]z\#_qyb[/math], где [math]b[/math] — строка, состоящая из такого количества пробелов, чтобы длина всего МО была [math]t + 1.[/math] Соответственно, начальное МО задаётся так: [math]\#_sxb[/math]. Если же [math]|x| \gt t[/math], то будем считать, что на ленту записаны лишь первые [math]t[/math] символов, ведь [math]m[/math] не может обработать большее количество символов за [math]t[/math] шагов.
Также нам удобно считать, что все вычисления проходят ровно за [math]t + 1[/math] шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход [math]q \vdash q[/math], если в МО [math]q[/math] есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО [math]q_t[/math].
Тогда процесс работы машины [math]m[/math] на входе [math]x[/math], то есть цепочка переходов [math]q_0 \vdash q_1 \vdash \ldots \vdash q_t[/math] может быть представлен следующей таблицей :

Процесс работы машины [math]m[/math] на входе [math]x[/math]

MO

0

1

...

...

t

[math]q_0[/math]

[math]q_{0, 0}[/math]

[math]q_{0, 1}[/math]

[math]q_{0, t}[/math]

[math]q_1[/math]

[math]q_{1, 0}[/math]

[math]q_{1, 1}[/math]

[math]q_{1, t}[/math]

...

[math] q_i [/math]

[math] q_{i, j - 1} [/math]

[math] q_{i, j} [/math]

[math] q_{i, j + 1} [/math]

[math] q_{i, j + 2} [/math]

[math] q_{i+1} [/math]

[math] q_{i+1, j - 1} [/math]

[math] q_{i+1, j} [/math]

[math] q_{i+1, j + 1} [/math]

...

[math]q_t[/math]

[math]q_{t, 0}[/math]

[math]q_{t, 1}[/math]

[math]q_{t, t}[/math]

Каждый элемент таблицы [math]q_{i, j}\in \Sigma \cup Q[/math]. И для каждого такого элемента заведём [math]|\Sigma| + |Q|[/math] переменных [math]Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q[/math]
Общий вид формулы: [math]\varphi = S \land T \land N \land C[/math].
  1. [math]S[/math] отвечает за правильный старт, то есть символ [math]q_{0,0}[/math] должен быть начальным состоянием [math]\#_s[/math] машины [math]m[/math], символы с [math]q_{0,1}[/math] по [math]q_{0,|x|}[/math] — образовывать цепочку [math]x[/math], а оставшиеся [math]q_{0,i}[/math] — быть пробелами [math]B[/math]. Таким образом, [math]S = Y_{0,0,\#_s} \land Y_{0,1,x_1} \land \ldots \land Y_{0,|x|+1,B} \land \ldots \land Y_{0,t,B}[/math].
  2. [math]T[/math] отвечает за правильный финиш, то есть в МО [math]q_t[/math] должно присутствовать допускающее состояние [math]\#_y[/math], следовательно [math]T = Y_{t,0,\#_y} \lor Y_{t,1,\#_y} \lor \ldots \lor Y_{t,t,\#_y}[/math].
  3. [math]N[/math] отвечает за то, что машина [math]m[/math] делает правильные переходы. [math]q_{i,j}[/math] зависит только от четырех символов над ним, то есть от [math]q_{i-1,j-1}, q_{i-1,j}, q_{i-1,j+1}[/math] и [math]q_{i-1,j+2}[/math]. Тогда для проверки корректности переходов требуется перебрать все четверки символов [math]q_{i-1,j-1}, q_{i-1,j}, q_{i-1,j+1}[/math] и [math]q_{i-1,j+2}[/math] из таблицы и проверить, что из них возможно получить символ [math]q_{i,j}[/math]. Если четверка символов выходит за границу таблицы, то указывается меньшее количество позиций. С учетом того, что машина [math]m[/math] недетерминирована и требуется устранить возможность раздвоения ее головки, сделаем все возможные выводы о новых символах [math]q_{i,j \pm 1}[/math]:
    [math]N = \land_{i=0..t,j=0..t} \land_{c_1 \ldots c_4} (( Y_{i-1,j-1,c_1} \land Y_{i-1,j,c_2} \land Y_{i-1,j+1,c_3} \land Y_{i-1,j+2,c_4} ) \to ((Y_{i,j-1,c_0^`} \lor Y_{i,j-1,c_1^`} \lor \ldots \lor Y_{i,j-1,c_{|\Sigma|+|Q|-1}^`}) \land (Y_{i,j,c_0^`} \lor Y_{i,j,c_1^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|+|Q|-1}^`}) \land (Y_{i,j+1,c_0^`} \lor Y_{i,j+1,c_1^`} \lor \ldots \lor Y_{i,j+1,c_{|\Sigma|+|Q|-1}^`})))[/math].
  4. [math]C[/math] отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки [math]q_{i,j}[/math] проверяется, что только одна переменная [math]Y_{i,j,c}[/math] принимает значение истина.
    [math]C = \land_{i=0..t,j=0..t} ((Y_{i,j,c_1} \land \lnot Y_{i,j,c_2} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|+|Q|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|+|Q|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|+|Q|-2}}))[/math].
Мы построили функцию сведения [math] f: \langle m, x, 1^t \rangle \mapsto \varphi = S \land T \land N \land C[/math]. Она является полиномиальной, так как длина формулы [math]\varphi[/math] полиномиально зависит от длины входа — [math]|\varphi| = O(n^2)[/math].
Покажем, что [math]\varphi[/math] выполнима тогда и только тогда, когда [math]\langle m, x, 1^t \rangle \in \mathrm{BH_{1N}} [/math].
  1. Пусть [math]\langle m, x, 1^t \rangle \in \mathrm{BH_{1N}}[/math], тогда существует допускающая цепочка переходов [math]q_0 \vdash q_1 \vdash ... \vdash q_t[/math] и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным [math]Y_{i,j,c}[/math], что [math]\varphi[/math] примет значение истина.
  2. Пусть в результате работы функции [math]f[/math] получили выполнимую формулу [math]\varphi[/math], следовательно существует такой набор переменных [math]Y_{i,j,c}[/math], что [math]\varphi[/math] на нем принимает значение истина. Тогда по данному набору можем построить таблицу, по которой восстановим допускающую цепочку переходов [math]q_0 \vdash q_1 \vdash ... \vdash q_t[/math]. Совершив эти переходы машина [math]m[/math] перейдет в допускающее состояние за время [math]t[/math], следовательно [math]\langle m, x, 1^t\rangle \in \mathrm{BH_{1N}}[/math].
Значит [math] \mathrm{SAT} \in \mathrm{NPC} [/math], что и требовалось доказать.
[math]\triangleleft[/math]

См. также