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

TL;DR

This paper introduces a new method for modeling set constraint problems and automatically encoding them into SAT, demonstrated on the Social Golfer Problem, resulting in more efficient and less error-prone solutions.

Contribution

The authors present a novel, declarative technique for modeling set constraints and automatically encoding them into SAT, improving over manual modeling methods.

Findings

Generated SAT instances have fewer clauses and variables.

Automatically encoded instances solve faster with SAT solvers.

Technique simplifies modeling and reduces errors.

Abstract

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.