# Encoding a “not-k-out-of-n” constraint for SAT solvers

I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver.

The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch and Giannaros, for example.

Given an "at-most-k-out-of-n" tool, I can get an "at-least-k-out-of-n" tool by inverting all the terms. With both tools, I can get a "k-out-of-n" tool by having both the "at-most-k" and "at-least-k" constraints.

But I don't see how I can encode a "not-k-out-of-n" constraint. If I use "at-most-(k-1)" and "at-least-(k+1)", then obviously I'm going to get no solutions.

Is there a simple transformation here that I'm missing?

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$$.