  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 and to encode them automatically
into SAT instances. We apply our technique to the Social Golfer Problem and we
also use it to break symmetries of the problem. Our technique is simpler, more
declarative, and less error-prone than direct and improved hand modeling. The
SAT instances that we automatically generate contain less clauses than improved
hand-written instances such as in [20], and with unit propagation they also
contain less variables. Moreover, they are well-suited for SAT solvers and they
are solved faster as shown when solving difficult instances of the Social
Golfer Problem.
