We reduce non-deterministic time $T \ge 2^n$ to a 3SAT
instance $\phi$ of size $|\phi| = T \cdot \log^{O(1)} T$
such that there is an explicit circuit $C$ that on input
an index $i$ of $\log |\phi|$ bits outputs the $i$th
clause, and each output bit of $C$ depends on $O(1)$
inputs bits. The previous best result was $C$ in NC$^1$.
Even in the simpler setting of $|\phi| = \poly(T)$ the
previous best result was $C$ in AC$^0$.

More generally, for any time $T \ge n$ and parameter $r
\leq n$ we obtain $\log_2 |\phi| = \max(\log T, n/r) +
O(\log n) + O(\log\log T)$ and each output bit of $C$ is
a decision tree of depth $O(\log r)$.

As an application, we simplify the proof of Williams'
ACC$^0$ lower bound, and tighten his connection between
satisfiability algorithms and lower bounds.

We reduce non-deterministic time $T \ge 2^n$ to a 3SAT
instance $\phi$ of size $|\phi| = T \cdot \log^{O(1)} T$
such that there is an explicit circuit $C$ that on input
an index $i$ of $\log |\phi|$ bits outputs the $i$th
clause, and each output bit of $C$ depends on $O(1)$
inputs bits. The previous best result was $C$ in NC$^1$.
Even in the simpler setting of $|\phi| = \poly(T)$ the
previous best result was $C$ in AC$^0$.

More generally, for any time $T \ge n$ and parameter $r
\leq n$ we obtain $\log_2 |\phi| = \max(\log T, n/r) +
O(\log n) + O(\log\log T)$ and each output bit of $C$ is
a decision tree of depth $O(\log r)$.

As an application, we simplify the proof of Williams'
ACC$^0$ lower bound, and tighten his connection between
satisfiability algorithms and lower bounds.

We reduce non-deterministic time $T \ge 2^n$ to a 3SAT
instance $\phi$ of size $|\phi| = T \cdot \log^{O(1)} T$
such that there is an explicit circuit $C$ that on input
an index $i$ of $\log |\phi|$ bits outputs the $i$th
clause, and each output bit of $C$ depends on $O(1)$
inputs bits. The previous best result was $C$ in NC$^1$.
Even in the simpler setting of $|\phi| = \poly(T)$ the
previous best result was $C$ in AC$^0$.

More generally, for any time $T \ge n$ and parameter $r
\leq n$ we obtain $\log_2 |\phi| = \max(\log T, n/r) +
O(\log n) + O(\log\log T)$ and each output bit of $C$ is
a decision tree of depth $O(\log r)$.

As an application, we simplify the proof of Williams'
ACC$^0$ lower bound, and tighten his connection between
satisfiability algorithms and lower bounds.

Minor changes

We reduce non-deterministic time $T \ge 2^n$ to a 3SAT
instance $\phi$ of size $|\phi| = T \cdot \log^{O(1)} T$
such that there is an explicit circuit $C$ that on input
an index $i$ of $\log |\phi|$ bits outputs the $i$th
clause, and each output bit of $C$ depends on $O(1)$
inputs bits. The previous best result was $C$ in NC$^1$.
Even in the simpler setting of $|\phi| = \poly(T)$ the
previous best result was $C$ in AC$^0$.

More generally, for any time $T \ge n$ and parameter $r
\leq n$ we obtain $\log_2 |\phi| = \max(\log T, n/r) +
O(\log n) + O(\log\log T)$ and each output bit of $C$ is
a decision tree of depth $O(\log r)$.

As an application, we simplify the proof of Williams'
ACC$^0$ lower bound, and tighten his connection between
satisfiability algorithms and lower bounds.