How convert instances of a language efficiently into 3SAT instances? The following question is from Sanjeev Arora and Boaz Barak ( not homework )


  Show that for every time constructible
  $T:N \to N$, if $L \in NTIME(T(n))$ then we can give a polynomial-time Karp reduction from $L$ to $3SAT$ that transforms instances of size $n$
  into 3CNF formulae of size $O(T(n)logT(n))$. Can you make this reduction also run in $O(T(n)logT(n))$? 


The best I could come up with is a $O(T(n)^3)$ formula. We take each configuration to be of at most length $T(n)$ and the machine runs for $T(n)$ steps. So we have a grid of $T(n)$ rows each with $T(n)$ columns. Each row represents a configuration. We just impose the condition that each row follows from the previous by using $M's$ ( where $M$ is a machine deciding $L$ in $O(T(n))$ time ) transition function in at most one step. The first row should represents start configuration and last row represents the accept configuration. Thus an $O(T(n)^3)$ formula is formed by this approach. 
How can I do better ?
The idea is to reduce an instance  $x$ to $\phi$ that uses only $O(T(n))$ symbols and clauses. $\log T(n)$ will be the length of binary representation of each symbol. This is the upper limit that you cannot cross if you want to solve the problem. So, you will have to optimize quite a bit. See the oblivious TM and state representation in Arora and Barak to get an idea.