All Questions
Tagged with applied-theory satisfiability
2 questions
1
vote
1
answer
136
views
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 ...
- 203
34
votes
3
answers
7k
views
Encoding 1-out-of-n constraint for SAT solvers
I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
D.W.♦
- 166k