We reduce non-deterministic time T2n to a 3SATinstance of size =TlogO(1)T such that there is an explicit circuit C that on inputan index i of log bits outputs the ithclause, and each output bit of C depends on O(1)inputs bits. The previous best result was C in NC1.Even in the simpler setting of =\poly(T) theprevious best result was C in AC0.

More generally, for any time Tn and parameter rn we obtain log2=max(logTnr)+O(logn)+O(loglogT) and each output bit of C isa decision tree of depth O(logr).

As an application, we simplify the proof of Williams'ACC0 lower bound, and tighten his connection betweensatisfiability algorithms and lower bounds.