Set Constraint Model and Automated Encoding into SAT: Application to the Social Golfer Problem
This work addresses the problem of simplifying and improving the efficiency of modeling set constraints for SAT solvers, primarily for researchers and practitioners in constraint programming and SAT solving, though it is incremental as it builds on existing encoding methods.
The authors tackled the challenge of modeling set constraint problems by developing a technique to automatically encode them into SAT instances, applied to the Social Golfer Problem, resulting in SAT instances with fewer clauses and variables and faster solving times for difficult instances.
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.