http://neerc.ifmo.ru/wiki/api.php?action=feedcontributions&user=Alexey&feedformat=atomВикиконспекты - Вклад участника [ru]2024-03-29T05:37:41ZВклад участникаMediaWiki 1.30.0http://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=2656Теорема Кука2010-09-10T02:00:01Z<p>Alexey: /* Доказательство того, что SAT ∈ NPH */</p>
<hr />
<div>=== Определение ===<br />
Проблема '''SAT''' = <tex>\{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема [[NP-полнота|'''NP'''-полна.]]<br />
<br />
== Формулировка теоремы Кука ==<br />
<br />
'''SAT''' ∈ '''NPC'''<br />
<br />
== Доказательство ==<br />
<br />
'''SAT''' ∈ '''NPC''', если<br />
*'''SAT''' ∈ '''NP''' <ref>[[NP|Класс '''NP''']]</ref><br />
*'''SAT''' ∈ '''NPH''' <ref>[[NP-полнота|'''NP'''-трудные задачи]]</ref><br />
<br />
=== Доказательство того, что SAT ∈ NP ===<br />
Прежде всего докажем, что '''SAT''' ∈ '''NP'''.<br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n</tex> штук, соответствующих значениям аргументов функции <tex>\phi</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
=== Доказательство того, что SAT ∈ NPH ===<br />
Теперь докажем, что '''SAT''' ∈ '''NPH'''. Для этого сведём проблему '''BH<sub>1N</sub>'''<ref>[[NP-полнота_задачи_BH1N|'''NP'''-полнота задачи '''BH<sub>1N</sub>''']]</ref>, которая, как нам известно, '''NP'''-полна, к проблеме '''SAT'''. Тогда получится, что любая проблема из '''NP''' может быть [[Сведение_по_Карпу|сведена по Карпу]] к проблеме '''BH<sub>1N</sub>''', и, по транзитивности сведения по Карпу, к '''SAT'''.<br />
<br />
По условию проблемы '''BH<sub>1N</sub>''', у нас есть недетерминированная машина Тьюринга <tex>m</tex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <tex>x</tex> и время <tex>t</tex>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <tex>\phi</tex>, что она выполнима тогда, и только тогда, когда <tex>m</tex>, получив на вход <tex>x</tex>, делает не более <tex>t</tex> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t</tex>.<br />
<br />
Тогда процесс работы машины <tex>m</tex> на входе <tex>x</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m</tex> на входе <tex>x</tex>'''<br />
|- <br />
! 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<br />
|- style="height:40px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0</tex><br />
| <tex>q_{0, 0}</tex> || <tex>q_{0, 1}</tex> || || || || || || || <tex>q_{0, t}</tex><br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_1</tex><br />
| <tex>q_{1, 0}</tex> || <tex>q_{1, 1}</tex> || || || || || || || <tex>q_{1, t}</tex><br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_i</tex><br />
| || || || <tex>q_{i, j - 1}</tex> || <tex>q_{i, j}</tex> || <tex>q_{i, j + 1}</tex> || <tex>q_{i, j + 2}</tex> || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}</tex><br />
| || || || <tex>q_{i+1, j - 1}</tex> || <tex>q_{i+1, j}</tex> || <tex>q_{i+1, j + 1}</tex> || || ||<br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_t</tex><br />
| <tex>q_{t, 0}</tex> || <tex>q_{t, 1}</tex> || || || || || || || <tex>q_{t, t}</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы: <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
# <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>.<br />
# <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>.<br />
# <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>: <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</tex> <tex>\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>.<br />
# <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <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>.<br />
<br />
Мы построили функцию сведения <tex>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от длины входа &mdash; <tex>|\phi| = O(n^2)</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle</tex> ∈ '''BH<sub>1N</sub>'''.<br />
<br />
# Пусть <tex>\langle m, x, 1^t \rangle</tex> ∈ '''BH<sub>1N</sub>''', тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.<br />
# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</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</tex> ∈ '''BH<sub>1N</sub>'''.<br />
<br />
Значит, '''SAT''' ∈ '''NPH''' и из доказанного ранее следует, что '''SAT''' ∈ '''NPC''', что и требовалось доказать.<br />
<br />
== Ссылки ==<br />
<references/><br />
<br />
== Внешние ссылки ==<br />
* [http://infolab.stanford.edu/~ullman/ialc.html Хопкрофт Дж., Мотвани Р., Ульман Дж., "Введение в теорию автоматов, языков и вычислений"]</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=2655Теорема Кука2010-09-10T01:58:48Z<p>Alexey: /* Доказательство того, что SAT ∈ NPH */</p>
<hr />
<div>=== Определение ===<br />
Проблема '''SAT''' = <tex>\{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема [[NP-полнота|'''NP'''-полна.]]<br />
<br />
== Формулировка теоремы Кука ==<br />
<br />
'''SAT''' ∈ '''NPC'''<br />
<br />
== Доказательство ==<br />
<br />
'''SAT''' ∈ '''NPC''', если<br />
*'''SAT''' ∈ '''NP''' <ref>[[NP|Класс '''NP''']]</ref><br />
*'''SAT''' ∈ '''NPH''' <ref>[[NP-полнота|'''NP'''-трудные задачи]]</ref><br />
<br />
=== Доказательство того, что SAT ∈ NP ===<br />
Прежде всего докажем, что '''SAT''' ∈ '''NP'''.<br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n</tex> штук, соответствующих значениям аргументов функции <tex>\phi</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
=== Доказательство того, что SAT ∈ NPH ===<br />
Теперь докажем, что '''SAT''' ∈ '''NPH'''. Для этого сведём проблему '''BH<sub>1N</sub>'''<ref>[[NP-полнота_задачи_BH1N|'''NP'''-полнота задачи '''BH<sub>1N</sub>''']]</ref>, которая, как нам известно, '''NP'''-полна, к проблеме '''SAT'''. Тогда получится, что любая проблема из '''NP''' может быть [[Сведение_по_Карпу|сведена по Карпу]] к проблеме '''BH<sub>1N</sub>''', и, по транзитивности сведения по Карпу, к '''SAT'''.<br />
<br />
По условию проблемы '''BH<sub>1N</sub>''', у нас есть недетерминированная машина Тьюринга <tex>m</tex>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <tex>x</tex> и время <tex>t</tex>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <tex>\phi</tex>, что она выполнима тогда, и только тогда, когда <tex>m</tex>, получив на вход <tex>x</tex>, делает не более <tex>t</tex> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q_t</tex>, если в МО <tex>q</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t</tex>.<br />
<br />
Тогда процесс работы машины <tex>m</tex> на входе <tex>x</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m</tex> на входе <tex>x</tex>'''<br />
|- <br />
! 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<br />
|- style="height:40px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0</tex><br />
| <tex>q_{0, 0}</tex> || <tex>q_{0, 1}</tex> || || || || || || || <tex>q_{0, t}</tex><br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_1</tex><br />
| <tex>q_{1, 0}</tex> || <tex>q_{1, 1}</tex> || || || || || || || <tex>q_{1, t}</tex><br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_i</tex><br />
| || || || <tex>q_{i, j - 1}</tex> || <tex>q_{i, j}</tex> || <tex>q_{i, j + 1}</tex> || <tex>q_{i, j + 2}</tex> || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}</tex><br />
| || || || <tex>q_{i+1, j - 1}</tex> || <tex>q_{i+1, j}</tex> || <tex>q_{i+1, j + 1}</tex> || || ||<br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_t</tex><br />
| <tex>q_{t, 0}</tex> || <tex>q_{t, 1}</tex> || || || || || || || <tex>q_{t, t}</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы: <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
# <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>.<br />
# <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>.<br />
# <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>: <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</tex> <tex>\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>.<br />
# <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <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>.<br />
<br />
Мы построили функцию сведения <tex>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от длины входа &mdash; <tex>|\phi| = O(n^2)</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle</tex> ∈ '''BH<sub>1N</sub>'''.<br />
<br />
# Пусть <tex>\langle m, x, 1^t \rangle</tex> ∈ '''BH<sub>1N</sub>''', тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.<br />
# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</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</tex> ∈ '''BH<sub>1N</sub>'''.<br />
<br />
Значит, '''SAT''' ∈ '''NPH''' и из доказанного ранее следует, что '''SAT''' ∈ '''NPC''', что и требовалось доказать.<br />
<br />
== Ссылки ==<br />
<references/><br />
<br />
== Внешние ссылки ==<br />
* [http://infolab.stanford.edu/~ullman/ialc.html Хопкрофт Дж., Мотвани Р., Ульман Дж., "Введение в теорию автоматов, языков и вычислений"]</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A3%D0%BC%D0%B5%D0%BD%D1%8C%D1%88%D0%B5%D0%BD%D0%B8%D0%B5_%D0%BE%D1%88%D0%B8%D0%B1%D0%BA%D0%B8_%D0%B2_%D0%BA%D0%BB%D0%B0%D1%81%D1%81%D0%B5_RP,_%D1%81%D0%B8%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%B8_%D1%81%D0%BB%D0%B0%D0%B1%D0%BE%D0%B5_%D0%BE%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5&diff=790Уменьшение ошибки в классе RP, сильное и слабое определение2010-04-14T18:47:27Z<p>Alexey: /* Доказательство эквивалентности определений */</p>
<hr />
<div>==Определение классов <tex>PR, RP_1, RP_2</tex>==<br />
Множество языков [[Сложностные_классы_RP_и_coRP |'''RP''']] определяется следующим образом:<br />
<br />
<tex>RP = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{2}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
Определим множества языков <tex>RP_1</tex> и <tex>RP_2</tex>:<br />
<br />
<tex>RP_1 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{p(|x|)}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
<tex>RP_2 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq 1 - \frac{1}{2^{p(|x|)}}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
В приведенных определениях <tex>p(|x|)</tex> &mdash; некий полином, а <tex>m</tex> &mdash; [[Вероятностные машины Тьюринга | вероятностная машина Тьюринга]], время работы которой в худшем случае составляет полином от длины входа.<br />
<br />
В классе <tex>RP_1</tex> ослаблено ограничение на вероятность ошибки ответа, а в классе <tex>RP_2</tex> усилено. Соответственно <tex>RP_1</tex> называется слабым определением класса <tex>RP</tex>, а <tex>RP_2</tex> &mdash; сильным.<br />
<br />
==Доказательство эквивалентности определений==<br />
Включение <tex>RP_2 \subset RP \subset RP_1</tex> очевидно, следовательно осталось доказать обратное включение <tex>RP_1 \subset RP \subset RP_2</tex>. Доказательство данного утверждения проводится с помощью метода уменьшения ошибки в классе <tex>RP</tex>.<br />
<br />
* Докажем включение <tex>RP_1 \subset RP</tex><br />
<br />
Выясним, сколько раз требуется запустить машину Тьюринга <tex>m</tex> из <tex>RP_1</tex>, для того, чтобы вероятность ошибки была меньше <tex>\frac{1}{2}</tex>. Запустим машину <tex>m</tex> <tex>k</tex> раз, тогда вероятность ошибки составит <tex>(1 - \frac{1}{p(n)})^k</tex>. Получим неравенство: <tex>(1 - \frac{1}{p(n)})^k < \frac{1}{2}</tex><br />
<br />
Логарифмируя, сведем к следующему: <tex>k\ ln(1 - \frac{1}{p(n)}) < ln(\frac{1}{2})</tex><br />
<br />
Разложив логарифм в левой части в ряд, получим: <tex>k(-\frac{1}{p(n)} + o(\frac{1}{p(n)})) < ln(\frac{1}{2})</tex><br />
<br />
Откуда <tex>k > p(n)ln(2)</tex>, где <tex>n</tex> &mdash; длина входа. То есть при <tex>k</tex>, удовлетворяющем полученному неравенству, вероятность ошибки не будет превышать <tex>\frac{1}{2}</tex>, а значит <tex>RP_1 \subset RP</tex>.<br />
<br />
* Докажем включение <tex>RP \subset RP_2</tex><br />
<br />
Доказательство проводится аналогично приведенному в первой части. Запустим машину <tex>m</tex> из <tex>RP</tex> <tex>k</tex> раз. С учетом ограничения, введенного в определении класса <tex>RP_2</tex>, получим неравенство: <tex>(\frac{1}{2})^k < \frac{1}{2^{p(n)}}</tex>.<br />
<br />
Прологарифмировав и сократив обе части неравенства на <tex>ln(\frac{1}{2})</tex>, получим неравенство: <tex>k > p(n)</tex>. То есть машина <tex>m</tex>, запущенная <tex>k</tex> раз, выдает неверный ответ с вероятностью, удовлетворяющей определению класса <tex>RP_2</tex>, а значит <tex>RP \subset RP_2</tex>.<br />
<br />
Эквивалентность определений класса <tex>RP</tex> доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A3%D0%BC%D0%B5%D0%BD%D1%8C%D1%88%D0%B5%D0%BD%D0%B8%D0%B5_%D0%BE%D1%88%D0%B8%D0%B1%D0%BA%D0%B8_%D0%B2_%D0%BA%D0%BB%D0%B0%D1%81%D1%81%D0%B5_RP,_%D1%81%D0%B8%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%B8_%D1%81%D0%BB%D0%B0%D0%B1%D0%BE%D0%B5_%D0%BE%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5&diff=789Уменьшение ошибки в классе RP, сильное и слабое определение2010-04-14T18:43:23Z<p>Alexey: </p>
<hr />
<div>==Определение классов <tex>PR, RP_1, RP_2</tex>==<br />
Множество языков [[Сложностные_классы_RP_и_coRP |'''RP''']] определяется следующим образом:<br />
<br />
<tex>RP = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{2}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
Определим множества языков <tex>RP_1</tex> и <tex>RP_2</tex>:<br />
<br />
<tex>RP_1 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{p(|x|)}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
<tex>RP_2 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq 1 - \frac{1}{2^{p(|x|)}}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
В приведенных определениях <tex>p(|x|)</tex> &mdash; некий полином, а <tex>m</tex> &mdash; [[Вероятностные машины Тьюринга | вероятностная машина Тьюринга]], время работы которой в худшем случае составляет полином от длины входа.<br />
<br />
В классе <tex>RP_1</tex> ослаблено ограничение на вероятность ошибки ответа, а в классе <tex>RP_2</tex> усилено. Соответственно <tex>RP_1</tex> называется слабым определением класса <tex>RP</tex>, а <tex>RP_2</tex> &mdash; сильным.<br />
<br />
==Доказательство эквивалентности определений==<br />
Включение <tex>RP_2 \subset RP \subset RP_1</tex> очевидно, следовательно осталось доказать обратное включение: <tex>RP_1 \subset RP \subset RP_2</tex>. Доказательство данного утверждения проводится с помощью метода уменьшения ошибки в классе <tex>RP</tex>.<br />
<br />
* Докажем включение <tex>RP_1 \subset RP</tex><br />
<br />
Выясним, сколько раз требуется запустить машину Тьюринга <tex>m</tex> из <tex>RP_1</tex>, для того, чтобы вероятность ошибки была меньше <tex>\frac{1}{2}</tex>. Запустим машину <tex>m</tex> <tex>k</tex> раз, тогда вероятность ошибки составит <tex>(1 - \frac{1}{p(n)})^k</tex>. Получим неравенство: <tex>(1 - \frac{1}{p(n)})^k < \frac{1}{2}</tex><br />
<br />
Логарифмируя, сведем к следующему: <tex>k\ ln(1 - \frac{1}{p(n)}) < ln(\frac{1}{2})</tex><br />
<br />
Разложив логарифм в левой части в ряд, получим: <tex>k(-\frac{1}{p(n)} + o(\frac{1}{p(n)})) < ln(\frac{1}{2})</tex><br />
<br />
Откуда <tex>k > p(n)ln(2)</tex>, где <tex>n</tex> &mdash; длина входа. То есть при <tex>k</tex>, удовлетворяющем полученному неравенству, вероятность ошибки не будет превышать <tex>\frac{1}{2}</tex>, а значит <tex>RP_1 \subset RP</tex>.<br />
<br />
* Докажем включение <tex>RP \subset RP_2</tex><br />
<br />
Доказательство проводится аналогично приведенному в первой части. Запустим машину <tex>m</tex> из <tex>RP</tex> <tex>k</tex> раз. С учетом ограничения, введенного в определении класса <tex>RP_2</tex>, получим неравенство: <tex>(\frac{1}{2})^k < \frac{1}{2^{p(n)}}</tex>.<br />
<br />
Прологарифмировав и сократив обе части неравенства на <tex>ln(\frac{1}{2})</tex>, получим неравенство: <tex>k > p(n)</tex>. То есть машина <tex>m</tex>, запущенная <tex>k</tex> раз, выдает неверный ответ с вероятностью, удовлетворяющей определению класса <tex>RP_2</tex>, а значит <tex>RP \subset RP_2</tex>.<br />
<br />
Эквивалентность определений класса <tex>RP</tex> доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A3%D0%BC%D0%B5%D0%BD%D1%8C%D1%88%D0%B5%D0%BD%D0%B8%D0%B5_%D0%BE%D1%88%D0%B8%D0%B1%D0%BA%D0%B8_%D0%B2_%D0%BA%D0%BB%D0%B0%D1%81%D1%81%D0%B5_RP,_%D1%81%D0%B8%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%B8_%D1%81%D0%BB%D0%B0%D0%B1%D0%BE%D0%B5_%D0%BE%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5&diff=788Уменьшение ошибки в классе RP, сильное и слабое определение2010-04-14T18:26:28Z<p>Alexey: Новая страница: «==Определение классов <tex>PR, RP_1, RP_2</tex>== Множество языков '''RP''' оп…»</p>
<hr />
<div>==Определение классов <tex>PR, RP_1, RP_2</tex>==<br />
Множество языков [[Сложностные_классы_RP_и_coRP |'''RP''']] определяется следующим образом:<br />
<br />
<tex>RP = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{2}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
Определим множества языков <tex>RP_1</tex> и <tex>RP_2</tex>:<br />
<br />
<tex>RP_1 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq \frac{1}{p(|x|)}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
<tex>RP_2 = \{L \mid \exists m: P(m(x) = 1 \mid x \in L) \geq 1 - \frac{1}{2^{p(|x|)}}, P(m(x) = 0 \mid x \notin L) = 1\}</tex><br />
<br />
В приведенных определениях <tex>p(|x|)</tex> &mdash; некий полином, а <tex>m</tex> &mdash; [[Вероятностные машины Тьюринга | вероятностная машина Тьюринга]], время работы которой в худшем случае составляет полином от длины входа.<br />
<br />
В классе <tex>RP_1</tex> ослаблено ограничение на вероятность ошибки ответа, а в классе <tex>RP_2</tex> усилено. Соответственно <tex>RP_1</tex> называется слабое определением класса <tex>RP</tex>, а <tex>RP_2</tex> &mdash; сильным.<br />
<br />
==Доказательство эквивалентности определений==<br />
Включение <tex>RP_2 \subset RP \subset RP_1</tex> очевидно, следовательно осталось доказать обратное включение: <tex>RP_1 \subset RP \subset RP_2</tex>. Доказательство данного утверждения проводится с помощью метода уменьшения ошибки в классе <tex>RP</tex>.<br />
<br />
* Докажем включение <tex>RP_1 \subset RP</tex><br />
<br />
Выясним, сколько раз требуется запустить машину Тьюринга <tex>m</tex> из <tex>RP_1</tex>, для того, чтобы вероятность ошибки была меньше <tex>\frac{1}{2}</tex>. Запустим машину <tex>m</tex> <tex>k</tex> раз, тогда вероятность ошибки составит <tex>(1 - \frac{1}{p(n)})^k</tex>. Получим неравенство:<br />
<br />
<tex>(1 - \frac{1}{p(n)})^k < \frac{1}{2}</tex><br />
<br />
Логарифмируя, сведем к следующему: <tex>k\ ln(1 - \frac{1}{p(n)}) < ln(\frac{1}{2})</tex><br />
<br />
Разложив логарифм в левой части в ряд, получим: <tex>k(-\frac{1}{p(n)} + o(\frac{1}{p(n)})) < ln(\frac{1}{2})</tex><br />
<br />
Откуда <tex>k > p(n)ln(2)</tex>, где <tex>n</tex> &mdash; длина входа. То есть при <tex>k</tex>, удовлетворяющем полученному неравенству вероятность ошибки не будет превышать <tex>\frac{1}{2}</tex>, а следовательно <tex>RP_1 \subset RP</tex>.<br />
<br />
* Докажем включение <tex>RP \subset RP_2</tex></div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D1%81%D0%BB%D0%BE%D0%B6%D0%BD%D0%BE%D1%81%D1%82%D0%B8_(%D1%81%D1%82%D0%B0%D1%80%D0%B0%D1%8F_%D1%82%D1%80%D0%B5%D1%88%D0%BE%D0%B2%D0%B0%D1%8F_%D0%B2%D0%B5%D1%80%D1%81%D0%B8%D1%8F)&diff=787Теория сложности (старая трешовая версия)2010-04-14T17:29:44Z<p>Alexey: /* Практика 7 */</p>
<hr />
<div>== Лекция 1 ==<br />
*[[Класс DSPACE]]<br />
*[[Класс DTIME]]<br />
*[[Теорема о емкостной иерархии]]<br />
*[[Теорема о временной иерархии]]<br />
*[[Сведение по Карпу]]<br />
*[[Сведение по Куку]]<br />
*[[Класс P]]<br />
*[[Класс NP]]<br />
*[[Класс coNP]]<br />
<br />
== Практика 1 ==<br />
*[[Сведение по Куку задачи факторизации к языку из NP]]<br />
<br />
== Лекция 2 ==<br />
*[[Теорема Кука]]<br />
<br />
== Практика 2 ==<br />
*[[Понятие NP-трудной и NP-полной задачи]]<br />
*[[NP-полнота задачи BH1N]]<br />
*[[NP-полнота задачи о выполнимости булевой формулы в форме КНФ]]<br />
*[[NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]<br />
*[[NP-полнота задачи о клике]]<br />
*[[NP-полнота задачи о независимом множестве]]<br />
*[[NP-полнота задачи о вершинном покрытии]]<br />
<br />
== Лекция 3 ==<br />
*[[Теорема Ладнера]]<br />
*[[Теорема Левина]]<br />
*[[Теорема Бейкера-Гилла-Соловэя]]<br />
<br />
== Практика 3 ==<br />
*[[NP-полнота задач о гамильтоновом цикле и пути в графах]]<br />
*[[NP-полнота задачи о сумме подмножества]]<br />
*[[NP-полнота задачи о рюкзаке]]<br />
<br />
== Практика, которой на самом деле не было ==<br />
*[[NP-полнота задачи о раскраске графа]]<br />
<br />
== Лекция 4 ==<br />
*[[Класс PS]]<br />
*[[Теорема Сэвича]]<br />
*[[PS-полнота задачи Generalized geography]]<br />
<br />
== Лекция 6 ==<br />
*Классы [[L]], [[NL]], [[NL-полнота|NLC]]<br />
*[[NL-полнота задачи о достижимости в графе]]<br />
*[[Классы EXP, NEXP. Полнота языков EXP и NEXP]]<br />
*[[Теорема о связи вопросов EXP=NEXP и P=NP]]<br />
*[[Теорема Иммермана]]<br />
<br />
== Практика 6 ==<br />
*[[Классы Sigma_i и Pi_i]]<br />
*[[Класс PH]]<br />
*[[Полиномиальная иерархия]]<br />
*[[Теоремы о коллапсе полиномиальной иерархии]]<br />
<br />
== Практика 7 ==<br />
*[[Вероятностная машина Тьюринга]]<br />
*[[Класс ZPP]]<br />
*[[Сложностные классы RP и coRP]]<br />
*[[Уменьшение ошибки в классе RP, сильное и слабое определение]]<br />
*[[Класс BPP]]<br />
<br />
== Лекция 8 ==<br />
*[[Теорема Лаутемана]]<br />
<br />
== Практика 8 ==<br />
*[[Лемма Шварца-Зиппеля]]</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=447Теорема Кука2010-03-18T19:45:24Z<p>Alexey: /* Доказательство того, что SAT ∈ NPH */</p>
<hr />
<div>=== Определение ===<br />
Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема <tex>NP\,\!</tex>-полна.<br />
<br />
== Формулировка ==<br />
'''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex><br />
<br />
== Доказательство ==<br />
<tex>SAT \in NPC</tex>, если<br />
*<tex>SAT \in NP</tex><br />
*<tex>SAT \in NPH</tex><br />
<br />
=== Доказательство того, что ''SAT'' ∈ ''NP'' ===<br />
Прежде всего докажем, что <tex>SAT \in NP.</tex><br />
<br />
Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex><br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
=== Доказательство того, что ''SAT'' ∈ ''NPH'' ===<br />
Теперь докажем, что <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><br />
<br />
По условию проблемы <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> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.<br />
<br />
Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>'''<br />
|- <br />
! 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<br />
|- style="height:40px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex><br />
| <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex><br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex><br />
| <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex><br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || ||<br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex><br />
| <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы: <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
# <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>.<br />
# <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>.<br />
# <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>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,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.<br />
# <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <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|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.<br />
<br />
Мы построили функцию сведения <tex>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от длины входа &mdash; <tex>|\phi| = O(n^2)</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle \in BH_{1N}</tex>.<br />
<br />
# Пусть <tex>\langle m, x, 1^t \rangle \in BH_{1N}</tex>, тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.<br />
# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</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 BH_{1N}</tex>.<br />
<br />
Значит, <tex>SAT \in NPH</tex> и из доказанного ранее следует,что <tex>SAT \in NPC</tex>.<br />
<br />
Теорема доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=446Теорема Кука2010-03-18T19:35:53Z<p>Alexey: /* Доказательство того, что SAT ∈ NPH */</p>
<hr />
<div>=== Определение ===<br />
Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема <tex>NP\,\!</tex>-полна.<br />
<br />
== Формулировка ==<br />
'''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex><br />
<br />
== Доказательство ==<br />
<tex>SAT \in NPC</tex>, если<br />
*<tex>SAT \in NP</tex><br />
*<tex>SAT \in NPH</tex><br />
<br />
=== Доказательство того, что ''SAT'' ∈ ''NP'' ===<br />
Прежде всего докажем, что <tex>SAT \in NP.</tex><br />
<br />
Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex><br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
=== Доказательство того, что ''SAT'' ∈ ''NPH'' ===<br />
Теперь докажем, что <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><br />
<br />
По условию проблемы <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> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.<br />
<br />
Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>'''<br />
|- <br />
! 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<br />
|- style="height:40px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex><br />
| <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex><br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex><br />
| <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex><br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || ||<br />
|- style="height:20px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:40px"<br />
! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex><br />
| <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы: <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
# <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>.<br />
# <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>.<br />
# <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>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,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.<br />
# <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <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|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.<br />
<br />
Мы построили функцию сведения <tex>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от <tex>|1^t| = t</tex>, а именно: <tex>|\phi| = O(t^2)</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex>\langle m, x, 1^t \rangle \in BH_{1N}</tex>.<br />
<br />
# Пусть <tex>\langle m, x, 1^t \rangle \in BH_{1N}</tex>, тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> и можем построить таблицу, аналогичную приведенной выше, следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.<br />
# Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</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 BH_{1N}</tex>.<br />
<br />
Значит, <tex>SAT \in NPH</tex> и из доказанного ранее следует,что <tex>SAT \in NPC</tex>.<br />
<br />
Теорема доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=254Теорема Кука2010-03-16T07:57:17Z<p>Alexey: /* Доказательство */</p>
<hr />
<div>=== Определение ===<br />
Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема <tex>NP\,\!</tex>-полна.<br />
<br />
== Формулировка ==<br />
'''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex><br />
<br />
== Доказательство ==<br />
<tex>SAT \in NPC</tex>, если<br />
*<tex>SAT \in NP</tex><br />
*<tex>SAT \in NPH</tex><br />
Прежде всего докажем, что <tex>SAT \in NP.</tex><br />
<br />
Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex><br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
Теперь докажем, что <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><br />
<br />
По условию проблемы <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> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.<br />
<br />
Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>'''<br />
|- <br />
! 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<br />
|- style="height:50px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex><br />
| <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex><br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex><br />
| <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex><br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || ||<br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex><br />
| <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы : <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
1) <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>.<br />
<br />
2) <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>.<br />
<br />
3) <tex>N</tex> отвечает за то, что машина <tex>m</tex> делает правильные переходы. <tex>q_{i,j}</tex> зависит только от четырех символов над ним, то есть от <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex>. Тогда для проверки корректности переходов требуется перебрать все четверки символов <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex> из таблицы и проверить, что из них возможно получить символ <tex>q_{i,j}</tex>. Если четверка символов выходит за границу таблицы, то указывается меньшее количество позиций. <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,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.<br />
<br />
4) <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <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|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.<br />
<br />
Мы построили функцию сведения <tex>f: <m, x, 1^t> \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от <tex>|1^t| = t</tex>, а именно: <tex>|\phi| = O(t^3)</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex><m, x, 1^t> \in BH_{1N}</tex>.<br />
<br />
1) Пусть <tex><m, x, 1^t> \in BH_{1N}</tex>, тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> (в МО <tex>q_t</tex> присутствует допускающее состояние <tex>\#_y</tex>), следовательно можем найти такое присваивание 0 и 1 переменным <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> примет значение ''истина''.<br />
<br />
2) Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> на нем принимает значение ''истина''. Тогда можем по данному набору построить таблицу, аналогичную приведенной выше, по которой можно восстановить допускающую цепочку переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>. Совершив эти переходы машина <tex>m</tex> перейдет в допускающее состояние за время <tex>t</tex>, следовательно <tex><m, x, 1^t> \in BH_{1N}</tex>.<br />
<br />
Значит, <tex>SAT \in NPH</tex> и из доказанного ранее следует,что <tex>SAT \in NPC</tex>.<br />
<br />
Теорема доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=252Теорема Кука2010-03-15T22:16:00Z<p>Alexey: /* Доказательство */ часть 2</p>
<hr />
<div>=== Определение ===<br />
Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема <tex>NP\,\!</tex>-полна.<br />
<br />
== Формулировка ==<br />
'''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex><br />
<br />
== Доказательство ==<br />
<tex>SAT \in NPC</tex>, если<br />
*<tex>SAT \in NP</tex><br />
*<tex>SAT \in NPH</tex><br />
Прежде всего докажем, что <tex>SAT \in NP.</tex><br />
<br />
Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex><br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
Теперь докажем, что <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><br />
<br />
По условию проблемы <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> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.<br />
<br />
Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>'''<br />
|- <br />
! 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<br />
|- style="height:50px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex><br />
| <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex><br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex><br />
| <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex><br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || ||<br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex><br />
| <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы : <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
<tex>S</tex> отвечает за правильный старт, то есть символ <tex>q_{0,0}</tex> должен быть начальным состоянием <tex>q_0\,\!</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>.<br />
<br />
<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>.<br />
<br />
<tex>N</tex> отвечает за то, что машина <tex>m\,\!</tex> делает правильные переходы. <tex>q_{i,j}</tex> зависит только от четырех символов над ним, то есть от <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex>. Тогда для проверки корректности переходов требуется перебрать все четверки символов <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex> из таблицы и проверить, что из них возможно получить символ <tex>q_{i,j}</tex>. Если четверка символов выходит за границу таблицы, то указывается меньшее количество позиций. <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,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.<br />
<br />
<tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. <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|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.<br />
<br />
Мы построили функцию сведения <tex>f: <m, x, 1^t> \mapsto \phi = S \land T \land N \land C</tex>.<br />
Покажем, что <tex>\phi</tex> выполнима тогда и только тогда, когда <tex><m, x, 1^t> \in BH_{1N}</tex>.<br />
<br />
1) Пусть <tex><m, x, 1^t> \in BH_{1N}</tex>, тогда существует цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>, где в <tex>q_t</tex> присутствует допускающее состояние <tex>\#_y\,\!</tex>, следовательно можем построить таблицу, аналогичную приведенной выше, а значит можем построить выполнимую формулу <tex>\phi</tex>.<br />
<br />
2) Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> на нем принимает значение <tex>1</tex>. Тогда можем по данному набору построить непротиворечивую таблицу, по которой можно восстановить цепочку переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>. Совершив эти переходы машина <tex>m</tex> перейдет в допускающее состояние за время <tex>t</tex>, следовательно <tex><m, x, 1^t> \in BH_{1N}</tex>.<br />
<br />
Значит, <tex>SAT \in NPH</tex> и из доказанного ранее следует,что <tex>SAT \in NPC</tex>.<br />
<br />
Теорема доказана.</div>Alexeyhttp://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D1%83%D0%BA%D0%B0&diff=240Теорема Кука2010-03-15T21:43:56Z<p>Alexey: /* Доказательство */ часть 2</p>
<hr />
<div>=== Определение ===<br />
Проблема <tex>SAT = \{\phi(x_1, ..., x_n)\ |\ \exists \{y_1, ..., y_n\} : \phi(y_1, ..., y_n) = 1\}</tex> &mdash; проблема выполнимости булевых формул.<br />
<br />
Докажем, что эта проблема <tex>NP\,\!</tex>-полна.<br />
<br />
== Формулировка ==<br />
'''Теорема Кука''' гласит, что <tex>SAT \in NPC.</tex><br />
<br />
== Доказательство ==<br />
<tex>SAT \in NPC</tex>, если<br />
*<tex>SAT \in NP</tex><br />
*<tex>SAT \in NPH</tex><br />
Прежде всего докажем, что <tex>SAT \in NP.</tex><br />
<br />
Так как <tex>NP = \Sigma_1\,\!</tex>, то достаточно показать, что <tex>SAT \in \Sigma_1</tex><br />
<br />
В качестве сертификата берём набор нулей и единиц в количестве <tex>n\,\!</tex> штук, соответствующих значениям аргументов функции <tex>\phi\,\!</tex>. Длина этого сертификата явно будет меньше или равна, чем полином от длины строки, кодирующей формулу <tex>\phi\,\!</tex>.<br />
<br />
Верификатор просто подставит эти значения в формулу <tex>\phi\,\!</tex> и выдаст значение формулы на данном входе. Таким образом, если формула действительно удовлетворима, то для неё найдётся такой сертификат, на котором она, и, соответственно, верификатор, выдадут единицу.<br />
<br />
Если же у нас существует такой сертификат <tex>y\,\!</tex>, на котором верификатор выдаёт единицу, то, значит, и формула является удовлетворимой.<br />
<br />
Теперь докажем, что <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><br />
<br />
По условию проблемы <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> шагов и допускает это слово.<br />
<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 />
<br />
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1\,\!</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash q</tex>, если в МО <tex>q\,\!</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t\,\!</tex>.<br />
<br />
Тогда процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей : <br />
{| align="right" border="1" class="wikitable" style="text-align:center" cellspacing="0"<br />
|+ '''Процесс работы машины <tex>m\,\!</tex> на входе <tex>x\,\!</tex>'''<br />
|- <br />
! 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<br />
|- style="height:50px;"<br />
! style="border-right:3px solid gray;" | <tex>q_0\,\!</tex><br />
| <tex>q_{0, 0}\,\!</tex> || <tex>q_{0, 1}\,\!</tex> || || || || || || || <tex>q_{0, t}\,\!</tex><br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_1\,\!</tex><br />
| <tex>q_{1, 0}\,\!</tex> || <tex>q_{1, 1}\,\!</tex> || || || || || || || <tex>q_{1, t}\,\!</tex><br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_i\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || <tex>q_{i, j + 2\,\!}</tex> || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_{i + 1}\,\!</tex><br />
| || || || <tex>q_{i, j - 1}\,\!</tex> || <tex>q_{i, j}\,\!</tex> || <tex>q_{i, j + 1\,\!}</tex> || || ||<br />
|- style="height:30px"<br />
! style="border-right:3px solid gray;" | ... || || || || || || || || ||<br />
|- style="height:50px"<br />
! style="border-right:3px solid gray;" | <tex>q_t\,\!</tex><br />
| <tex>q_{t, 0}\,\!</tex> || <tex>q_{t, 1}\,\!</tex> || || || || || || || <tex>q_{t, t}\,\!</tex><br />
|}<br />
Каждый элемент таблицы <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 />
<br />
Общий вид формулы : <tex>\phi = S \land T \land N \land C</tex>.<br />
<br />
<tex>S</tex> отвечает за правильный старт, то есть символ <tex>q_{0,0}</tex> должен быть начальным состоянием <tex>q_0\,\!</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>.<br />
<br />
<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>.<br />
<br />
<tex>N</tex> отвечает за то, что машина <tex>m\,\!</tex> делает правильные переходы. <tex>q_{i,j}</tex> зависит только от четырех символов над ним, то есть от <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex>. Тогда для проверки корректности переходов требуется перебрать все четверки символов <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex> из таблицы и проверить, что из них возможно получить символ <tex>q_{i,j}</tex>. Следовательно <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,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.<br />
<br />
<tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. <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|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.</div>Alexey