# NEXP Cook-Levin

I've come across the following lemma (without proof):

The first part of the lemma states that for any $x$, there's a 3CNF exponential Boolean formula $f(x)$ that is satisfiable if and only if $x \in L \in \mathsf{NEXP}$ (the same as in the Cook-Levin theorem for NP), while the second part states that there's a polynomial algorithm which given $x$ outputs a circuit $C_x$ such that when evaluated on input $i$ the circuit $C_x$ outputs the $i$-th clause of $f(x)$.

I am not sure how one can output that circuit, since the formula depends on th $x$, and we need kind of "bookmark" to the $i$-th clause.

-
if you remember the textbook proof of Cook-Levin, this is not very hard. see the brief sketch of a proof after thm 2.2. here for example: arxiv.org/pdf/1111.1261v1.pdf –  Sasho Nikolov Feb 29 '12 at 16:52
@SashoNikolov that should be an answer! –  Daniel Apon Mar 2 '12 at 10:43

By definition, a language $L$ is in $\mathsf{NEXP}$ if there exists a (single tape) nondeterministic Turing machine $M_L$ that on input $x$ outputs $1$ if and only if $x \in L$, and runs in time bounded by $2^{p(|x|)}$. For any $x$ we can think of a tableau of the computation of some accepting path of $M_L$: make a table of size $2^{p(|x|)} \times 2^{p(|x|)}$ and in cell $(i, j)$ write down the contents of the $j$-th cell of the tape at time step $i$ (at time step 1 we assume the tape contains $x$ and at the final time step we want the tape to only contain 1, indicating acceptance). Also, there is a special symbol where the head of the Turing machine is at each time step, and the internal state is also indicated in that cell. So the question "does there exist an accepting path of $M_L$ for $x$" boils down to "can we fill out the tableau for $x$ correctly according to the transition table of $M_L$?" The main idea of Cook-Levin is that whether the tableau is filled out correctly can be checked by verifying a number of local constraints, because each cell of the tableau only depends on the three cells above it. Thus each local constraint can be checked by a constant size 3CNF and the conjunction of the 3CNFs is the formula $f(x)$. The new observation for the $\mathsf{NEXP}$ version is that, except for the first $|x|$ entries of the first row and the first entry of the last row of the tableau (where we check that the tape starts off with containing $x$ and ends with containing $1$), each 3CNF checking local constraints is exactly the same, up to the labeling of variables. So, given the index of a 3CNF clause of $f(x)$, we need the circuit $C(x)$ to:
2. if it corresponds to the first $|x|$ entries of the first row or the first entry of the last row of the tableau, output the clause
Steps 1 and 3 are basically arithmetic based on the index of the clause of $f(x)$ and the index of the tableau cell it corresponds to. Both these indexes can be written in $O(p(|x|))$ bits and steps 1 and 3 therefore can be done in time polynomial in $|x|$. Since any function computable in polynomial time can be computed using a polynomial size circuit, we have poly size circuits for 1 and 3. For step 2 we need to just hard-wire $O(|x|)$ 3CNF terms into the circuit. Put all these together, and we're done.