On the one hand, Constraint Satisfaction Problems allow one to declaratively model problems. On the other hand, propositional satisfiability problem (SAT) solvers can handle huge SAT instances. We thus present a technique to declaratively model set constraint problems, to reduce them, and to encode them into ”good” SAT instances. We illustrate our technique on the well-known nqueens problem. Our technique is simpler, more expressive, and less error-prone than direct hand modeling. The SAT instances that we automatically generate are rather small w.r.t. hand-written instances.