# algorithm and Cook theorem

Let $A$ be a set of decision algorithms which are running in polynomial time and which takes natural numbers as inputs.

$x\in A$ if and only if

for $i\in N$

$x(i)=0$ or $x(i)=1$

and running time of $x(i)$ is smaller than $n^k$ ($n$ is digit of $i$)

Now consider a $\mathcal{NP}$ problem for the set $A$.

Problem: "For given $x\in A$, is there any $i\in N$, such that $x(i)=0$?"

For this $\mathcal{NP}$ problem, there is a decider of non-deterministic Turing machine $M$

$$M(x) = \left\{ \begin{array}{ll} 1\text{ if there exists i∈ N, such that x(i)=0 }\\ 0\text{ otherwise} \end{array} \right.$$

And for this NDTM, there is a verifier of polynomial Deterministic Turing Machine $V$,

$$V(x,i) = \left\{ \begin{array}{ll} 1\text{ if x(i)=0 }\\ 0\text{ otherwise} \end{array} \right.$$

Question : By the Cook-Levin theorem, I think something can be transformed into a Boolean formula. What is transformed into a Boolean formula?

$M$? $M(x)$? $V$? $V(x)$? $x$? or the NP problem itself?

-
The usual version of the Cook-Levin theorem provides a transformation from the decider $M$, but the truth value of the variables is (partially) set by the input $x$. That is, there are variables of the form $S_{i,\rho}$ which are true if the $i$th symbol on the input tape is $\rho$ (so you have about $n\times|\Sigma|$ of these, where $n$ is the length of encoding of the input and $\Sigma$ is the input alphabet).
It would not be too hard to imagine that there would be an alternate proof that usese $V$ instead of $M$. Indeed, Levin's proof mapped from search problems, rather than decisions problems anyway. The key part in any such proof though is that we need to be able to map any problem in $\mathcal{NP}$ to SAT. Thus we need to use some universal property of all problems in $\mathcal{NP}$, such as that they all have a NDTM that decides them, or a DTM that verifies them.