Set constraint model and automated encoding into SAT: application to the social golfer problem

Lardeux F.; Monfroy E.; Crawford B.; Soto R.

dc.contributor.author	Lardeux F.
dc.contributor.author	Monfroy E.
dc.contributor.author	Crawford B.
dc.contributor.author	Soto R.
dc.date.accessioned	2020-09-02T22:21:16Z
dc.date.available	2020-09-02T22:21:16Z
dc.date.issued	2015
dc.identifier	10.1007/s10479-015-1914-5
dc.identifier.citation	235, 1, 423-452
dc.identifier.issn	02545330
dc.identifier.uri	https://hdl.handle.net/20.500.12728/5051
dc.description	On the one hand, constraint satisfaction problems allow one to expressively model problems. On the other hand, propositional satisfiability problem (SAT) solvers can handle huge SAT instances. We thus present a technique to expressively 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 expressive, and less error-prone than direct modeling. The SAT instances that we automatically generate contain less clauses than improved direct instances such as in Triska and Musliu (Ann Oper Res 194(1):427–438, 2012), 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. © 2015, Springer Science+Business Media New York.
dc.language.iso	en
dc.publisher	Springer New York LLC
dc.subject	Constraint programming
dc.subject	CSP
dc.subject	SAT encoding
dc.subject	Set constraints
dc.subject	Social golfer problem
dc.title	Set constraint model and automated encoding into SAT: application to the social golfer problem
dc.type	Article