Local reductions

We reduce non-deterministic time T ≥ 2^n to a 3SAT instance ϕ of quasilinear size |ϕ| = T ·log^O(1) T such that there is an explicit circuit C that on input an index i of log |ϕ| bits outputs the ith clause, and each output bit of C depends on O(1) input bits. The previous best result was C in NC^1. Even in the simpler setting of polynomial size |ϕ| = (T) the previous best result was C in AC^0. More generally, for any time T ≥ n and parameter r ≤ n we obtain log_2 |ϕ| = max(log T, n/r) + O(log n) + O(loglog T) and each output bit of C is a decision tree of depth O(log r). As an application, we tighten Williams' connection between satisfiability algorithms and circuit lower bounds (STOC 2010; SIAM J. Comput. 2013).