Item


Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories

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

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

© Constraints, 2013, vol. 18, núm. 2, p. 236-268

Springer Verlag

Author: Ansótegui, Carlos
Bofill Arasa, Miquel
Palahí i Sitges, Miquel
Suy Franch, Josep
Villaret i Ausellé, Mateu
Date: 2013 January 1
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
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
Format: application/pdf
ISSN: 1383-7133 (versió paper)
1572-9354 (versió electrònica)
Document access: http://hdl.handle.net/10256/12646
Language: eng
Publisher: Springer Verlag
Collection: MEC/PN 2009-2011/TIN2008-04547
AGAUR/2009-2013/2009 SGR-1434
Reproducció digital del document publicat a: http://dx.doi.org/10.1007/s10601-012-9131-1
Articles publicats (D-IMA)
Is part of: © Constraints, 2013, vol. 18, núm. 2, p. 236-268
Rights: Tots els drets reservats
Subject: Programació per restriccions (Informàtica)
Constraint programming (Computer science)
Algorismes computacionals
Computer algorithms
CSP (Llenguatge de programació)
CSP (Computer program language)
Title: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
Type: info:eu-repo/semantics/article
Repository: DUGiDocs

Subjects

Authors