Notes

Chapter 12: The Principle of Computational Equivalence

Section 8: Undecidability and Intractability


Satisfiability [emulating Turing machines]

Given variables \[DoubleStruckS][t, s], \[DoubleStruckA][t, x, a], \[DoubleStruckN][t, n] representing whether at step t a non-deterministic Turing machine is in state s, the tape square at position x has color a, and the head is at position n, the following CNF expression represents the assertion that a Turing machine with stot states and ktot possible colors follows the specified rules and halts after at most t steps:

NDTMToCNF[rules_, {s_, a_, n_}, t_] := {Table[Or @@ Table[\[DoubleStruckS][i, j], {j, stot}], {i, t - 1}], Table[ !\[DoubleStruckS][i, j] || !\[DoubleStruckS][i, k], {i, 0, t - 1}, {j, stot}, {k, j + 1, stot}], Table[Or @@ Table[\[DoubleStruckN][i, j], {j, n + i, Max[0, n - i], -2}], {i, 0, t}], Table[ !\[DoubleStruckN][i, j] || !\[DoubleStruckN][i, k], {i, 0, t}, {j, n + i, Max[0, n - i], -2}, {k, j + 2, n + i}], Table[Or @@ Table[\[DoubleStruckA][i, j, k], {k, 0, ktot - 1}], {i, 0, t - 1}, {j, Max[1, n - i], n + i}], Table[ !\[DoubleStruckA][i, j, k] || !\[DoubleStruckA][i, j, m], {i, 0, t - 1}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}, {m, k + 1, ktot - 1}], \[DoubleStruckS][0, s], Cases[MapIndexed[\[DoubleStruckA][Abs[n - First[#2]], First[#2], #1] & , a], \[DoubleStruckA][x_, _, _] /; x < t], Table[\[DoubleStruckA][Abs[n - i], i, 0], {i, Length[a] + 1, n + t - 1}], Table[ !\[DoubleStruckA][i, j, k] || If[EvenQ[n + i - j], \[DoubleStruckN][i, j], False] || \[DoubleStruckA][i + 1, j, k], {i, 0, t - 2}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}], Table[Function[z, Outer[ !\[DoubleStruckN][i, j] || !\[DoubleStruckS][i, z[[1,1]]] || !\[DoubleStruckA][i, j, z[[1,2]]] || ##1 & , Sequence @@ (If[i < t - 1, {\[DoubleStruckS][i + 1, #1[[1]]], \[DoubleStruckN][i + 1, j - #1[[3]]], \[DoubleStruckA][i + 1, j, #1[[2]]]}, {\[DoubleStruckN][i + 1, j - #1[[3]]]}] & ) /@ z[[2]]]] /@ rules, {i, 0, t - 1}, {j, n + i, Max[1, n - i], -2}], Or @@ Table[\[DoubleStruckN][i, 0], {i, n, t, 2}]} /. List -> And


From Stephen Wolfram: A New Kind of Science [citation]