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.

You can write a straight-line program (an equivalent way to define a circuit) that computes the Boolean variables $z_{i,j}=[x_1+y_1+\cdots+x_i+y_i \equiv j \pmod{3}]$ (where $i=1,\ldots,n$ and $j=0,1,2$) as follows:

• $z_{1,0} = \lnot x_1 \land \lnot y_1$.

• $z_{1,1} = (x_1 \land \lnot y_1) \lor (\lnot x_1 \land y_1)$.

• $z_{1,2} = x_1 \land y_1$.

• $z_{i+1,j} = (z_{i,j} \land \lnot x_{i+1} \land \lnot y_{i+1}) \lor (z_{i,j-1} \land ((x_{i+1} \land \lnot y_{i+1}) \lor (\lnot x_{i+1} \land y_{i+1})) \lor (z_{i,j-2} \land x_{i+1} \land y_{i+1})$

The output of the circuit is $o = \lnot z_{n,n \bmod 3}$.

The circuit has size $O(n)$.

StackExchange Computer Science Q#111643, answer score: 2