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 http://cstheory.stackexchange.com/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
