An AC$^1$ circuit for 2-SAT We know that $NC^1 \subseteq NL \subseteq AC^1$ and that 2-SAT is complete for $NL$.


  How does one construct an $AC^1$ circuit for 2-SAT?


Recall that $AC^1$ circuits have $O(\log n)$ depth where $n$ is the number of bits in the input.

I have read Herbert Vollmer's book on Circuit Complexity as well as the chapter in Arora-Barak's book.  Still, appears to be very challenging.

For example, we can fix the length of the input for each variable (say $3$ bits).    For each literal, let the first bit indicate whether it is positive or negative.  So each literal is represented by $1+3 = 4$ bits.

Thus the negative literal $\neg x_1 \equiv 0001$ and the positive literal $x_2 \equiv 1010$.

Let FALSE $\equiv 0000$ and let a unit clause (a clause with one literal) ($x_i$) be represented as $(x_i \lor FALSE)$.

Hence a 2SAT formula $\phi = (x_1 \lor \neg x_2) \land (x_5 \lor \neg x_6)$ would be represented as

$11110$-$1001$-$0010$-$1101$-$0110~ $ as input to the circuit
(dashes just added for reading clarity only).

The first $4$ bits $1111$ mean that each literal is represented by $4$ bits --- the fifth bit ($0$) is just a separator before the actual input $\phi$ begins.

And then we have to implement an algorithm in the (C $\log n$) levels above the input level, for some constant $C$, using $AND$, $OR$ and $NOT$ gates, allowing unbounded fan-in.

Is this going in the right direction?
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)$.