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!