Conjunctive Normal Form Which is True iff Exactly $k$ literals are true?

Question

Can we create a CNF formula $F$ which is true iff exactly $k$ of the $n$ variables are true?

Formally, if variables $x_i \in \{0,1\}$ then $\sum_{i=1}^{n} x_i = k \iff F$ is true

What about a CNF which is true iff $ \le k$ variables are true?

Update: I arrived at a DNF with $\binom{n}{k}$ clauses such that in each clause exactly $k$ variables are positive literals and the other $n-k$ variables are negative literals.

To convert this to a CNF I was distributing the disjunction over the conjunctions. I noticed that this procedure will result in a lot of clauses which are unecessary eg of the form $x_i \lor \neg x_i \dots$ Moreover I will have $n^{\binom{n}{k}}$ clauses in total, not necessarily distinct. This form will not be very convenient if I wish to compute, given a random assignment of variables, what is the probability that a clause is not satisfied etc.

(My main objective is to use the CNF $F$ for this problem in conjunction with another formula such that I can model a constraint for the original problem)

I tried out the examples for small cases with $n = 3$ etc to find some patterns but I can't seem to generalize these for larger cases.

Hence I reask the question:

Does there exist a CNF formula $F$ with distinct with $n$ variables such that $F$ is in some form that can be analyzed and $F$ is true iff exactly $k$ variables are true.

Answer 1

Denote true and false by 1 and 0 respectively. Let $\oplus$ denote the xor-operation.

Denote a conjunction $n$ by $\wedge_j(\sigma_{n,j}\oplus x_j)$ with initial Boolean variables $x_j$ and signs $\sigma_{n,j}$.

A formula $F_k=\bigvee_{\{n|(\sum_j\sigma_{n,j}=k)\}}(\wedge_j(\sigma_{n,j}\oplus x_j))$ would do the trick, and could be transformed to CNF by standard procedures.