A satisfiability modulo theories approach to constraint programming

Full Text
In this thesis we focus on solving CSPs using SMT. Essentially, what we do is reformulating CSPs into SMT. The obtained results allow us to conclude that state-of-the-art SMT solvers are a robust tool to solve CSPs. We tackle not only decisional CSPs, but also Constraint Optimization Problems and Weighted Constraint Satisfaction Problems. For solving these problems we have used SMT in conjunction with appropriated algorithms: search algorithms and UNSAT core-based algorithms. We have provided support for meta-constraints that is, constraints on constraints. Meta-constraints can be very helpful in the modelling process. Once verified that SMT is a good generic approximation for CP, we tested how algorithms built on top of an SMT solver can have equal or better performance than ad-hoc programs designed specifically for a given problem. The problem that we have selected to make this test is the RCPSP, obtaining highly competitive results. ​
​L'accés als continguts d'aquesta tesi queda condicionat a l'acceptació de les condicions d'ús establertes per la següent llicència Creative Commons: http://creativecommons.org/licenses/by/3.0/es/