Main idea: an algorithm can be converted to a Boolean circuit

…table…

M accepts w if and only if the tableau can be filled such that:

• The first row is the starting configuration of M on input w
• $\left( {i + 1} \right)^{\text{st}}$ configuration follows from the $i^{\text{th}}$ configuration
• Eventually reach an accepting configuration

So how can this tableau be converted into a boolean formula? We’ll come up with some boolean variables to represent what is happening in the cells.

Let $\text{cell}\left\lbrack {i,j} \right\rbrack$ refer to the according tableau entry.

• Note: row i: time step, column j: head position, $i,j \leq n^{k}$
• Our cell entries are not boolean values: but we still want to encode them as such!
• Create boolean variables $x_{i,j,s}$ where $i,j \leq n^{k}$ and $s \in \gamma \cup Q$
• $\text{cell}\left\lbrack {i,j} \right\rbrack = s\Leftrightarrow x_{i,j,s} = \text{true} \land x_{i,j,s} = \text{false}\ \forall s \neq s$

For a nondeterministic Turing machine:

• The same table as the deterministic Turing machine:
• only the $\left( {i + 1} \right)^{\text{st}}$ configuration follows from the $i^{\text{th}}$ configuration using some nondeterministic choice

$\varphi = \varphi_{\text{cell}} \land \varphi_{\text{start}} \land \varphi_{\text{move}} \land \varphi_{\text{accept}}$

• $\varphi_{\text{cell}} = \land_{i,j}\left( {\vee_{s \in \Gamma \cup Q}\left( {x_{i,j,s} \land \neg\left( {\vee_{t \neq s}x_{i,j,t}} \right)} \right)} \right)$
• $\varphi_{\text{start}} = x_{1,1,\#} \land x_{1,2,q_{0}} \land x_{1,3,w} \land x_{1,4,w}\ldots$
• $\varphi_{\text{accept}} = \vee_{i,j}x_{i,j,q_{\text{accept}}}$: check if any cell is accepting

Window[i,j]: six cells of the table (six cells is convenient: 3x2, we need three to read the current, state, and next items)

• i.e. the window is size 3x2 because that’s exactly what we need to check that it is valid

$\varphi_{\text{move}} = \land_{1 \leq i \leq n^{k} - 1,1 \leq j \leq n^{k} - 2}\left( {\text{Window}\left\lbrack {i,j} \right\rbrack\ \text{is legal}} \right)$

note: pull examples, when there is no head the last two columns cannot change

… online lecture …