Изменения

По условию проблемы <math>BH_{1N}\,\!</math>, у нас есть недетерминированная машина Тьюринга <math>m\,\!</math>, причём можно считать, что её лента односторонняя и что машина не пишет на ленту пробелы, входное слово <math>x\,\!</math> и время <math>t\,\!</math>, заданное в унарной системе счисления. Нам же надо построить такую булеву формулу <math>\phi\,\!</math>, что она выполнима тогда, и только тогда, когда <math>m\,\!</math>, получив на вход <math>x\,\!</math>, делает не более <math>t\,\!</math> шагов и допускает это слово. В любой момент времени мгновенное описание (МО) <math>m\,\!</math> есть строка <math>z\#_qyb</math>, где <math>b\,\!</math> &mdash; строка, состоящая из такого количества пробелов, чтобы длина всего МО была <math>t + 1.\,\!</math> Соответственно, начальное МО задаётся так : <math>\#_sx\,\!</math>. Если же <math>|x| > t\,\!</math>, то будем считать, что на ленту записаны лишь первые <math>t\,\!</math> символов, ведь <math>m\,\!</math> не может обработать большее количество символов за <math>t\,\!</math> шагов. Также нам удобно считать, что все вычисления проходят ровно за <math>t + 1\,\!</math> шагов, даже если мы попали в допускающее состояние раньше. То есть, мы разрешим переход <math>q \vdash q</math>, если в МО <math>q\,\!</math> есть допускающее состояние, так что, чтобы проверить, допустила ли машина слово, надо лишь проверить наличие допускающего состояния в МО <math>q_t\,\!</math>. Тогда процесс работы машины <math>m\,\!</math> на входе <math>x\,\!</math>, то есть цепочка переходов <math>q_0 \vdash q_1 \vdash ... \vdash q_t</math> может быть представлен следующей таблицей :  {| border="1" class="wikitable" style="text-align:center" cellspacing="0"|+ '''Процесс работы машины <math>m\,\!</math> на входе <math>x\,\!</math>'''|- ! width="50" style="border-right:3px solid gray; border-bottom:3px solid gray;" | MO !! width="50" style="border-bottom:3px solid gray;"| 0 !! width="50" style="border-bottom:3px solid gray;" | 1 !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="50" style="border-bottom:3px solid gray;" | !! width="30" style="border-bottom:3px solid gray;" | ... !! width="50" style="border-bottom:3px solid gray;" | t|- style="height:50px;"! style="border-right:3px solid gray;" | <math>q_0\,\!</math>| <math>q_{0, 0}\,\!</math> || <math>q_{0, 1}\,\!</math> || || || || || || || <math>q_{0, t}\,\!</math>|- style="height:50px"! style="border-right:3px solid gray;" | <math>q_1\,\!</math>| <math>q_{1, 0}\,\!</math> || <math>q_{1, 1}\,\!</math> || || || || || || || <math>q_{1, t}\,\!</math>|- style="height:30px"! style="border-right:3px solid gray;" | ... || || || || || || || || |||- style="height:50px"! style="border-right:3px solid gray;" | <math>q_i\,\!</math>| || || || <math>q_{i, j - 1}\,\!</math> || <math>q_{i, j}\,\!</math> || <math>q_{i, j + 1\,\!}</math> || <math>q_{i, j + 2\,\!}</math> || |||- style="height:50px"! style="border-right:3px solid gray;" | <math>q_{i + 1}\,\!</math>| || || || <math>q_{i, j - 1}\,\!</math> || <math>q_{i, j}\,\!</math> || <math>q_{i, j + 1\,\!}</math> || || |||- style="height:30px"! style="border-right:3px solid gray;" | ... || || || || || || || || |||- style="height:50px"! style="border-right:3px solid gray;" | <math>q_t\,\!</math>| <math>q_{t, 0}\,\!</math> || <math>q_{t, 1}\,\!</math> || || || || || || || <math>q_{t, t}\,\!</math>|}Каждый элемент таблицы <math>q_{i, j}\in \Sigma \cup Q</math>. И для каждого такого элемента заведём <math>|\Sigma| + |Q|\,\!</math> переменных <math>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q\,\!</math> Общий вид формулы : <math>\phi = S \and T \and N \and C</math>