Can every Turing Machine be translated into a SAT formula?
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.