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.

  • $\begingroup$ 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? $\endgroup$
    – MLStudent
    Jun 12 '19 at 18:46
  • $\begingroup$ 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.) $\endgroup$
    – dkaeae
    Jun 13 '19 at 6:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.