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

Text Complet
SolvingWeightedCSPs.pdf closed access
Sol·licita còpia a l'autor de l'article
En omplir aquest formulari esteu demanant una còpia de l'article dipositat al repositori institucional (DUGiDocs) al seu autor o a l'autor principal de l'article. Serà el mateix autor qui decideixi lliurar una còpia del document a qui ho sol•liciti si ho creu convenient. En tot cas, la Biblioteca de la UdG no intervé en aquest procés ja que no està autoritzada a facilitar articles quan aquests són d'accés restringit.
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 ​
​Tots els drets reservats