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

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.

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.

• Observation: any propositional formula is equivalent to a formula in CNF, so the restriction to CNF is a red herring. – Rob Arthan Feb 26 '16 at 22:40
• Do you mean "if and only if"? Because as it stands (with just "only if") any sentence that is always false (such as $p\land \lnot p$) would satisfy this. Or maybe spotting this is part of the exercise? – Arthur Feb 26 '16 at 22:42
• @Arthur: perhaps we're supposed to take the conjunction of the title and the question $\ddot{\smile}$. – Rob Arthan Feb 26 '16 at 22:44
• I mean to say that if I assign the literals $x_i = {0,1}$, then the CNF is true iff $\sum x_i = k$ – Banach Tarski Feb 26 '16 at 22:44
• Hint: try a disjunctive normal form over all conjunctions with exactly k variables true and transform it to CNF. – Gyro Gearloose Feb 26 '16 at 22:53

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.
• @BanachTarski sigma is the sign. If $\sigma=1$ then xor-ing a variable with it effectively negates it. And I see I have forgotten to put $\oplus$ into the formula. – Gyro Gearloose Feb 27 '16 at 15:31