Bounds on reducing from NP to SAT

Let M be a non deterministic turing machine.

Suppose M is a TM that runs in T(n) time.

Given an instance of x in {0,1}^n, and the question M(x) accepts?

We can

1) convert M into an oblivious TM that runs in O( T \log T) time. 2) convert the oblivious TM into a circuit SAT instance with O( T \log T ) gates. 3) Convert the circuit SAT into a 3CNF with O (T \log T) vars and O (T \log T) clauses.

Question: is there a way to make this tighter? In particular, can I get a SAT instance of vars/clauses O(n), rather than O( T(n) \log T(n) ) ?

Or is this essentially impossible, as I am forced to have a variable for each non-deterministic step the TM takes, (thus lower bounded to T(n)).

Thanks!

-
It is impossible because it would contradict the nondeterministic time hierarchy theorem. en.wikipedia.org/wiki/… – Tsuyoshi Ito Oct 7 '11 at 2:43
note: there is a meta-discussion about the recent questions in complexity including this one here. – Kaveh Oct 7 '11 at 4:11
My previous comment is wrong, because the time complexity of the reduction can be any polynomial depending on the language. – Tsuyoshi Ito Oct 7 '11 at 10:57