Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
MetadataShow full item record
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.
Is part ofConstraints, 2013, vol. 18, núm. 2, p. 236-268
Showing items related by title, author, creator and subject.
Ansótegui Gil, Carlos José; Larrubia, Jose; Li, Chu-Min; Manyà Serres, Felip (Springer Verlag, 2007)We show that we can design and implement extremely efficient variable selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets of Boolean variables that model the same multivalued variable ...
Empirical models for predicting the production of wild mushrooms in Scots pine (Pinus sylvestris L.) forests in the Central Pyrenees Bonet Lledos, José Antonio; Pukkala, Timo; Colinas, C. (Carlos); Fischer, Christine; Palahí, Marc; Martínez de Aragón, Juan; Colinas, C. (Carlos) (Institut national de la recherche agronomique (França)EDP Sciences, 2008)Mushroom picking has become a widespread autumn recreational activity in the Central Pyrenees and other regions of Spain. Predictive models that relate mushroom production or fungal species richness with forest stand and ...
Argelich Romà, Josep; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles; Planes Cid, Jordi (Springer International Publishing Switzerland, 2016-06-01)We analyze and compare two solvers for Boolean optimization problems: WMaxSatz, a solver for Partial MaxSAT, and MinSatz, a solver for Partial MinSAT. Both MaxSAT and MinSAT are similar, but previous results indicate that ...