Can a propositional threshold connective be expressed by standard connectives?

We are given a finite set of propositional atoms $\{x_1, \dots, x_n\}$ and an integer $k$.
Can we capture through a propositional formula $\varphi$ (built from the standard connectives $\neg, \wedge, \vee$ only) the set of all models having at most $k$ atoms valued at $1$, such that the size of $\varphi$ is polynomial w.r.t. $n$? If yes, how?

The only way I see is to define $\varphi$ as an exponential-sized DNF formula containing $\binom{n}{k}$ conjunctions of literals. For instance, for n=5 and k=2, the corresponding formula would be $(\neg x_1 \wedge \neg x_2 \wedge \neg x_3) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_4) \vee (\neg x_1 \wedge \neg x_2 \wedge \neg x_5) \vee (\neg x_2 \wedge \neg x_3 \wedge \neg x_4) \vee (\neg x_2 \wedge \neg x_3 \wedge \neg x_5) \vee \dots$

I got the following comment for the same question on https://cstheory.stackexchange.com/ but I do not have the level to understand it. I googled all keywords but I still cannot find the answer.


$d_H(\omega, \omega')$ equals the number of 1 bits in the pointwise XOR of $\omega$ and $\omega'$. So, compute the XORs, count the number of 1 bits, and compare the result to k. It is well known that one can count bits with log-depth circuits (hence polynomial-size formulas), and one easy way to do that is to sum the individual bits using repeated 3-to-2 carry-save addition. See en.wikipedia.org/wiki/Carry-save_adder if you don’t know what that is. The choice of the basis of connectives is immaterial in all this, as long as it is complete

The idea is to use the following steps:

• Construct an NC1 circuit computing the binary representation of $x_1+\cdots+x_n$, see for example these lecture notes (Theorem 7). This circuit implements carry-save addition.

• Convert the NC1 circuit to a polynomial size formula, see for example these lecture notes (Proposition 1).

• For each $k$, it is now easy to construct a polynomial size formula that tests whether $x_1+\cdots+x_n=k$.

• Use up to $n$ of the formulas from the previous step to come up with your desired formula.

You can in fact implement the last two steps more efficiently, using $\log n$ rather $n$ copies of the preceding formula, by using a comparison gadget; details left to you.

StackExchange Computer Science Q#38007, answer score: 4