Polynomial size Boolean circuit for counting number of bits Given a natural number $n \geq 1$, I am looking for a Boolean circuit over $2n$ variables, $\varphi(x_1, y_1, \dots, x_n, y_n)$, such that the output is true if and only if the assignment that makes it true verifies
$$\sum_{i = 1}^{i = n} (x_i + y_i) \not\equiv n \bmod 3$$
I should specify that this I am looking for a Boolean circuit, not necessarily a Boolean formula as it is usually written in Conjunctive Normal Form (CNF). This is because when written in CNF, a formula like the one before has a trivial representation where the number of clauses is approximately $\frac{4^n}{3}$, as it contains a clause for every assignment $(x_1, y_1, \dots, x_n, y_n)$ whose bits sum to a value which is congruent with $n \bmod 3$. Constructing such a formula would therefore take exponential time.
I have been told that a Boolean circuit can be found for this formula that accepts a representation of size polynomial in $n$. However, so far I have been unable to find it. I would use some help; thanks.
 A: Hint: Suppose you have a circuit with three outputs $s_0,s_1,s_2$ such that
$s_k$ is true iff $\sum_{i=1}^{n-1} (x_i + y_i) \equiv k \mod 3$. Use these
and $x_n, y_n$ to get $s'_0, s'_1, s'_2$ such that $s'_j$ is true iff
$\sum_{i=1}^n (x_i + y_i) \equiv j \mod 3$.
A: So, following Robert Israel's hint (and more or less the same hint received at the Computer Science Stack Exchange), I've got the following:
You consider Boolean circuits $s_i^k$ over variables $(x_1, y_1, \dots, x_k, y_k)$, with $i \in \{0, 1, 2\}$ and $k \in \{1, \dots, n - 1\}$, such that $s_i^k$ is true if and only if $\sum_{j = 1}^k (x_i + y_i)\equiv i \bmod 3$.
With these circuits in hand, it is easy to obtain the corresponding circuits for $k = n$ (that is, $s_0^n$, $s_1^n$ and $s_2^n$):
$$s_0^n = (s_0^{n-1} \land \neg x_n \land \neg y_n) \lor (s_1^{n-1} \land x_n \land y_n) \lor (s_2^{n-1} \land  (x_n \oplus  y_n))$$
$$\dots$$
Now, you can obtain $\varphi(x_1, y_1, \dots, x_n, y_n) = \neg s_{n \bmod 3}^n$. Since we only have to build three new formulas for each value in $\{1, \dots, n\}$, each of which can be computed in constant time, we are able to build $\varphi$ in linear time.
With regards to the base cases, it is straightforward to see that:
$$s_0^1 = \neg x_1 \land \neg y_1$$
$$s_1^1 = x_1 \oplus y_1$$
$$s_0^2 = x_1 \land y_1$$
