11
правок
Изменения
м
→Доказательство того, что SAT ∈ NPH
В любой момент времени мгновенное описание (МО) <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> шагов.
Также нам удобно считать, что все вычисления проходят ровно за <tex>t + 1</tex> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <tex>q \vdash qq_t</tex>, если в МО <tex>q</tex> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <tex>q_t</tex>.
Тогда процесс работы машины <tex>m</tex> на входе <tex>x</tex>, то есть цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex> может быть представлен следующей таблицей :
|- style="height:40px"
! style="border-right:3px solid gray;" | <tex>q_{i + 1}</tex>
| || || || <tex>q_{i+1, j - 1}</tex> || <tex>q_{i+1, j}</tex> || <tex>q_{i+1, j + 1}</tex> || || ||
|- style="height:20px"
! style="border-right:3px solid gray;" | ... || || || || || || || || ||
# <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>: <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>.# <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>.
Мы построили функцию сведения <tex>f: \langle m, x, 1^t \rangle \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от длины входа — <tex>|\phi| = O(n^2)</tex>.
