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

Full Text
SolvingWeightedCSPs.pdf embargoed access
Request a copy
When filling the form you are requesting a copy of the article, that is deposited in the institutional repository (DUGiDocs), at the autor or main autor of the article. It will be the same author who decides to give a copy of the document to the person who requests it, if it considers it appropriate. In any case, the UdG Library doesn’t take part in this process because it is not authorized to provide restricted articles.
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