Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
dc.contributor.author
dc.date.accessioned
2016-09-06T10:12:46Z
dc.date.available
2016-09-06T10:12:46Z
dc.date.issued
2013-01-01
dc.identifier.issn
1383-7133
dc.identifier.uri
dc.description.abstract
We introduce WSimply, a new framework for modelling and solving Weighted Constraint Satisfaction Problems (WCSP) using Satisfiability Modulo Theories (SMT) technology. In contrast to other well-known approaches designed for extensional representation of goods or no-goods, and with few declarative facilities, our approach aims to follow an intensional and declarative syntax style. In addition, our language has built-in support for some meta-constraints, such as priority and homogeneity, which allows the user to easily specify rich requirements on the desired solutions, such as preferences and fairness. We propose two alternative strategies for solving these WCSP instances using SMT. The first is the reformulation into Weighted SMT (WSMT) and the application of satisfiability test based algorithms from recent contributions in the Weighted Maximum Satisfiability field. The second one is the reformulation into an operation research-like style which involves an optimisation variable or objective function and the application of optimisation SMT solvers. We present experimental results of two well-known problems: the Nurse Rostering Problem (NRP) and a variant of the Balanced Academic Curriculum Problem (BACP), and provide some insights into the impact of the addition of meta-constraints on the quality of the solutions and the solving time
dc.description.sponsorship
This work is an extended version of the paper [1] presented at the ModRef 2011 workshop. Research partially supported by the Generalitat de Catalunya under grant AGAUR 2009-SGR-1434, and the Ministerio de Economía y Competividad research projects TIN2008-04547, TIN2009-14704-C03-01, and TIN2010-20967-C04-01/03
dc.format.mimetype
application/pdf
dc.language.iso
eng
dc.publisher
Springer Verlag
dc.relation
info:eu-repo/grantAgreement/MICINN//TIN2008-04547/ES/SUBASTAS ROBUSTAS MEDIANTE LA INCORPORACION DE TECNICAS DE SATISFACTIBILIDAD MODULO TEORIAS/
AGAUR/2009-2013/2009 SGR-1434
dc.relation.isformatof
Reproducció digital del document publicat a: http://dx.doi.org/10.1007/s10601-012-9131-1
dc.relation.ispartof
© Constraints, 2013, vol. 18, núm. 2, p. 236-268
dc.relation.ispartofseries
Articles publicats (D-IMA)
dc.rights
Tots els drets reservats
dc.subject
dc.title
Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
dc.type
info:eu-repo/semantics/article
dc.rights.accessRights
info:eu-repo/semantics/embargoedAccess
dc.embargo.terms
Cap
dc.date.embargoEndDate
info:eu-repo/date/embargoEnd/2026-01-01
dc.type.version
info:eu-repo/semantics/publishedVersion
dc.identifier.doi
dc.identifier.idgrec
016758
dc.contributor.funder
dc.relation.ProjectAcronym
dc.identifier.eissn
1572-9354