Ítem


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

Springer Verlag

Director: Ministerio de Educación y Ciencia (Espanya)
Generalitat de Catalunya. Agència de Gestió d’Ajuts Universitaris i de Recerca
Autor: Ansótegui, Carlos
Bofill Arasa, Miquel
Palahí i Sitges, Miquel
Suy Franch, Josep
Villaret i Ausellé, Mateu
Resum: 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
Accés al document: http://hdl.handle.net/2072/297998
Llenguatge: eng
Editor: Springer Verlag
Drets: Tots els drets reservats
Matèria: Programació per restriccions (Informàtica)
Constraint programming (Computer science)
Algorismes computacionals
Computer algorithms
CSP (Llenguatge de programació)
CSP (Computer program language)
Títol: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
Tipus: info:eu-repo/semantics/article
Repositori: Recercat

Matèries

Autors