Encoding a "not-k-out-of-n" constraint for SAT solvers
Assuming you work in CNF, construct  "at least $k+1$-out-of-$n$" and add "or $p$" to each disjunction. Do the same for "at most $k-1$-out-of-$n$" and add "or $q$" to each disjunction.

Then add one extra term to your main conjunction, $\neg p \vee \neg q$.