CNF/ Efficient way for satisfied k variables I have varaibles from X1....Xn. I want to ensure that only k of the variables are satisifed (geting the value true).
I know that for one variable, I can write formula for at least one, and formula for at most one, and then be sure that only one variable is satisifed. But how I do it for k variables (In CNF form)?
EDIT: I need an efficient way to do it. I would be happy for solution for k=2. Thank you.
 A: The "efficiency" depends on the parameters you're considering. For example, it's possible to construct such CNF of size which is polynomial in $n$ but not in $k$; for any fixed $k$, the size (and construction time) would be polynomial in $n$. Once such construction contains two types of clauses:


*

*Those which prevent more than $k$ variable from being true: $(\neg X_{i_1} \vee \neg X_{i_2} \vee \ldots \vee \neg X_{i_{k+1}})$ for all unordered $(k+1)$-tuples of distinct indices $i$.

*Those which force at least $k$ variables to be true: $(X_{j_1} \vee X_{j_2} \vee \ldots \vee X_{j_{n-k+1}})$ for all unordered $(n-k+1)$-tuples of distinct indices $j$.


In total, there are $\binom{n}{k+1}$ clauses of the first kind and $\binom{n}{n-k+1}=\binom{n}{k-1}$ of the second kind. The total number of literals in the clauses is $\binom{n}{k+1}(k+1)+\binom{n}{k-1}(n-k+1) = n\binom{n}{k}$.
For example, for $k=2$ and $n=5$, you'd get the following $15$ clauses with 50 literals in total:
$(\neg X_1 \vee \neg X_2 \vee \neg X_3)$, $(\neg X_1 \vee \neg X_2 \vee \neg X_4)$, $(\neg X_1 \vee \neg X_2 \vee \neg X_5)$, $(\neg X_1 \vee \neg X_3 \vee \neg X_4)$, $(\neg X_1 \vee \neg X_3 \vee \neg X_5)$, $(\neg X_1 \vee \neg X_4 \vee \neg X_5)$, $(\neg X_2 \vee \neg X_3 \vee \neg X_4)$, $(\neg X_2 \vee \neg X_3 \vee \neg X_5)$, $(\neg X_2 \vee \neg X_4 \vee \neg X_5)$, $(\neg X_3 \vee \neg X_4 \vee \neg X_5)$.
$(X_1 \vee X_2 \vee X_3 \vee X_4)$, $(X_1 \vee X_2 \vee X_3 \vee X_5)$, $(X_1 \vee X_2 \vee X_4 \vee X_5)$, $(X_1 \vee X_3 \vee X_4 \vee X_5)$, $(X_2 \vee X_3 \vee X_4 \vee X_5)$.
A: Here's a brute force solution, in two stages. (1) Write a DNF formula with the desired property. (2) Convert the DNF formula to CNF.
Step (1) is easy. Consider a wff $Q = Y_1 \land Y_2 \land Y_3 \land \ldots \land Y_n$ where each $Y_i$ is either $X_i$ or $\neg X_i$, and exactly $k$ of the $X_i$ appear unnegated. Then $Q$ is true when a particular $k$ atomic variables are satisfied, yes? So now disjoin every possible wff of the kind $Q$ (by taking every possible way of choosing $k$ variables from $n$ to appear positively). Then you have a wff in DNF which is true just when some assortment of exactly $k$ atomic variables are satisfied.
Step (2): turn that DNF wff into CNF by your favourite method.
