Set Constraint Model and Automated Encoding into SAT: Application to the Social Golfer Problem

A CSP is defined by some variables (generally over finite domains) and constraints between these variables. Solving a CSP consists in finding assignments of the variables that satisfy the constraints. One of the main strength of CSP is declarativity: variables can be of various types (finite domains, floating point numbers, intervals, sets,...) and constraints as well (linear arithmetic constraints, set constraints, non linear constraints, Boolean constraints, symbolic constraints,...). Moreover, the so-called global constraints not only improve solving efficiency but also declarativity: they propose new constructs and relations such as alldifferent (to enforce that all the variables of a list have different values), cumulative (to schedule tasks sharing resources),... On the other hand, the propositional satisfiability problem (SAT) [12] is restricted (in terms of declarativity) to Boolean variables and propositional formulae. However, SAT solvers can now handle huge SAT instances (millions of variables).