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