# 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?

• Have you seen the proof that $\mathsf{NL} \subseteq \mathsf{AC}^1$? The proof is constructive an explains how to construct an $\mathsf{AC}^1$ circuit for directed reachability (or some other $\mathsf{NL}$-complete problem). Combine this with the reduction from 2SAT to directed reachability, and you're done. – Yuval Filmus Jun 8 '15 at 0:46
• The first part of the circuit would be the $AC^0$ reduction from 2SAT to directed reachability (constant depth circuit). The second part of the circuit would be the $O(\log n)$ depth circuit to solve directed reachability. – Sameer Gupta Jun 8 '15 at 4:13
• That's right. Perhaps you can now answer your own question. – Yuval Filmus Jun 8 '15 at 12:28
• Some other questions to consider --- Could we construct an $AC^1$ circuit for HornSAT? Or, in the other direction, can we prove that this is impossible, perhaps using the switching lemma? Some food for thought. – Sameer Gupta Jun 8 '15 at 23:18
• HornSAT is P-complete, so it's probably not in $\mathsf{AC}^1$. The switching lemma doesn't help, though – it stops working around depth $\log n/\log\log n$. – Yuval Filmus Jun 9 '15 at 2:16

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)$.