Изменения
→Доказательство того, что SAT ∈ NPH
# <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>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_1^`} \lor Y_{i,j-1,c_2^`} \lor \ldots \lor Y_{i,j-1,c_{|\Sigma|-1}^`})) \land</tex> <tex>\land (Y_{i,j,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`})) \land (Y_{i,j+1,c_1^`} \lor Y_{i,j+1,c_2^`} \lor \ldots \lor Y_{i,j+1,c_{|\Sigma|-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|-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>.
