how to convert linear equation to cnf

Question

I'm working on reduction from binary puzzle problem into sat. one of the game's rule is that in each row/column numbers of 1s equals to numbers of 0. I found a solution but it's exponential.
Therefore, I need to turn the equation: $X_1+ X_2+..... +X_{2n} =n$ , $X_i$ is $0$ or $1$, to cnf.

Answer 1

Another way to say, $X_1+ X_2+\dots +X_{2n} =n$ where $X_i$ is $0$ or $1$ is to say, $\exists_{=n}(X_1+ X_2+\dots+X_{2n})$, meaning that exactly n of the literals are true.

The CNF for this can be split into two subproblems, "n or fewer of the literals are true" and "n or more of the literals are true". When these two groups of constraints are put together, the intersection is "exactly n of the literals are true".

1) To state the constraint: "n or more of the literals are true", generate all combinations of the literals taken $n+1$ at time.

For example, given the elements:

(x₁, x₂, x₃, x₄, x₅, x₆)

The CNF for "no fewer than 3 three are true" is generated by taking the literals four at a time:

(x₁, x₂, x₃, x₄)
(x₁, x₂, x₃, x₅)
(x₁, x₂, x₃, x₆)
(x₁, x₂, x₄, x₅)
(x₁, x₂, x₄, x₆)
(x₁, x₂, x₅, x₆)
(x₁, x₃, x₄, x₅)
(x₁, x₃, x₄, x₆)
(x₁, x₃, x₅, x₆)
(x₁, x₄, x₅, x₆)
(x₂, x₃, x₄, x₅)
(x₂, x₃, x₄, x₆)
(x₂, x₃, x₅, x₆)
(x₂, x₄, x₅, x₆)
(x₃, x₄, x₅, x₆)

2) To state the constraint: "n or fewer of the literals are true", generate all combinations of the negated literals taken $n+1$ at time.

For example, given the elements:

(x₁, x₂, x₃, x₄, x₅, x₆)

The CNF for "no more than 3 three are true" is generated by taking the negated literals four at a time:

(~x₁, ~x₂, ~x₃, ~x₄)
(~x₁, ~x₂, ~x₃, ~x₅)
(~x₁, ~x₂, ~x₃, ~x₆)
(~x₁, ~x₂, ~x₄, ~x₅)
(~x₁, ~x₂, ~x₄, ~x₆)
(~x₁, ~x₂, ~x₅, ~x₆)
(~x₁, ~x₃, ~x₄, ~x₅)
(~x₁, ~x₃, ~x₄, ~x₆)
(~x₁, ~x₃, ~x₅, ~x₆)
(~x₁, ~x₄, ~x₅, ~x₆)
(~x₂, ~x₃, ~x₄, ~x₅)
(~x₂, ~x₃, ~x₄, ~x₆)
(~x₂, ~x₃, ~x₅, ~x₆)
(~x₂, ~x₄, ~x₅, ~x₆)
(~x₃, ~x₄, ~x₅, ~x₆)

Last, concatenate the two CNFs to generate all solutions to the linear formula where the only half of the literals are true :-)