# Can every Turing Machine be translated into a SAT formula?

For the proof of "Cook-Levin Theorem", for a Turing Machine $$M$$ that accepts a language $$L \in NP$$ and input $$x \in \{0,1\}^*$$, we can create a SAT Formula, that is satisfiable if and only if $$M$$ accepts $$x$$. Could we adopt this construction so that for any Turing Machine $$M$$ and input $$x \in \{0,1\}^*$$ we can create a SAT Formula $$\phi$$ that is satisfiable if and only if $$M$$ accepts $$x$$ (even if this SAT Formula has more than polynomial length of $$|M|$$)? Or would that contradicts Rice's Theorem?

Edit: As dkaeae correctly pointed out, defining a SAT formula that is satisfiable iff a TM $$M$$ accepts an input $$x$$ is indeed possible. What I meant to ask though is, whether a reduction in the sense of a computable function exists (albeit not being limited to running in polynomial time, but indeed being somehow limited in the running time).

The proof of the Cook-Levin theorem shows that for any nondeterministic Turing machine $$M$$, any input $$x$$, and any (reasonable) time bound $$t(n)$$, we can construct (efficiently) a SAT formula of size proportional to $$t(|x|)^2$$ that is satisfiable iff $$M$$ accepts $$x$$ within $$t(|x|)$$ steps.
If you know that $$M$$ is supposed to halt within $$t(n)$$ steps, then the SAT formula captures the behavior of $$M$$ on $$x$$. But for a general Turing machine we don't possess any a priori bound on the running time. This is why you cannot solve the halting problem in this way.
Certainly you can. Given $$M$$ and an input $$w \in \{ 0,1 \}^\ast$$, produce $$x \lor x$$ if $$M$$ accepts $$x$$ and $$x \land \lnot x$$ otherwise.
• Thanks! I will edit my question to add: Can we define a reduction, which has a running time somehow bounded by the input length (not necessarily by a polynomial though), but still outputs a sat formula that is satisfiable iff $M$ accepts $x$? I think in this case, Yuval's answer holds, correct? Jun 12 '19 at 18:46
• Indeed. It seems the (only?) requirement for the reduction to work is that the time of $M$ is bounded by a computable function. (This implies, among other things, that $M$ always halts on every input.) Jun 13 '19 at 6:56