Expressing $n$ out of $m$ Boolean variables have to be true

Question

I have a SAT problem with thousands of variables. Let $m$ be the number of variables. Each of the variables has $4$ indexes $v_{i,j,k,l}$. I struggle to find some concise mathematical notation to express that exactly $n$ variables have to be $\texttt{true}$, and all of them must have distinct $l$ index.

Can someone help?

Answer 1

I may be overlooking something, but this seems straightforward. Use value $0$ for false and $1$ for true.

Exactly $n$ variables are true: $$\sum_{i,j,k,l}{v_{i,j,k,l}} = n$$

No two have the same $l$-index: $$\forall l:\sum_{i,j,k}{v_{i,j,k,l}} \le 1$$

Answer 2

Exactly $n$ true: $$\bigvee_{S: |S|=n} \left[\left(\bigwedge_{(i,j,k,l)\in S} v_{i,j,k,l}\right)\bigwedge \left(\bigwedge_{(i,j,k,l)\notin S} \neg v_{i,j,k,l}\right)\right]$$

Distinct $l$ index: $$\bigwedge_l \bigwedge_{\substack{(i,j,k),(i',j',k'):\\(i,j,k)\not=(i',j',k')}} \neg(v_{i,j,k,l} \land v_{i',j',k',l})$$