0
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.