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

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

Версия 21:29, 13 марта 2010

Определение

Проблема [math]SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}[/math] — проблема выполнимости булевых формул.

Докажем, что эта проблема [math]NP\,\![/math]-полна.

Формулировка

Теорема Кука гласит, что [math]SAT \in NPC.[/math]

Доказательство

[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].

Верификатор просто подставит эти значения в формулу [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] — строка, состоящая из такого количества пробелов, чтобы длина всего МО была [math]t + 1.\,\![/math] Соответственно, начальное МО задаётся так : [math]\#_sx\,\![/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 ... \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, j - 1}\,\![/math] [math]q_{i, j}\,\![/math] [math]q_{i, 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]\phi = S \land T \land N \land C[/math]