Can every Turing Machine be translated into a SAT formula?

Question

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).

Answer 1

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.

Answer 2

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.