# Is there a simple way to construct a Boolean formula that is true if and only if at most $k$ of the input variables are true? [duplicate]

I could of course construct a truth table for the function $$f(x) = \left(\sum_i x_i\right) \leq k$$ Where $x$ is an assignment and I'm slightly abusing notation to count Booleans. And then I could make a formula from that.
But if there are $n$ variables then this truth table will have $2^n$ rows, rather unwieldy. Even if I only consider those rows for which $f(x) = \text{true}$ I'll still have ${n}\choose{k}$ clauses which remains exponential if $k = n/2$.
Alternatively I can write a program for verifying that only $k$ variables are true and then go through the construction in the Cook-Levin theorem to produce a 3-SAT formula, this time only of polynomial size.
But I feel like this problem ought to be even simpler than that. Does anybody have an idea?