An AC$^1$ circuit for 2-SAT
The proof that $\mathsf{NL} \subseteq \mathsf{AC}^1$ is constructive, giving an $\mathsf{AC}^1$ circuit for directed reachability. Since directed reachability is $\mathsf{NL}$-complete and 2SAT is in $\mathsf{NL}$, there is an $\mathsf{AC}^0$ reduction from 2SAT to directed reachability. Combining the $\mathsf{AC}^1$ circuit for directed reachability with the $\mathsf{AC}^0$ reduction from 2SAT to directed reachability, we obtain an $\mathsf{AC}^1$ circuit for 2SAT.

It might be better, however, to construct such a circuit directly using ideas from the proof of $\mathsf{NL} \subseteq \mathsf{AC}^1$. This could result is a smaller and simpler circuit.

The OP also asks whether HornSAT has $\mathsf{AC}^1$ circuits. Since HornSAT is $\mathsf{P}$-complete and we believe that $\mathsf{AC}^1 \neq \mathsf{P}$, the answer is probably no. The OP suggests using the switching lemma to prove this. However, the switching lemma only works for circuits of depth $O(\log n/\log\log n)$.