A satisfiability modulo theories approach to constraint programming

Autores: Josep Suy Franch
Directores de la Tesis: Mateu Villaret Auselle (dir. tes.) , Miquel Bofill Arasa (dir. tes.)
Lectura: En la Universitat de Girona ( España ) en 2012
Idioma: inglés
Tribunal Calificador de la Tesis: Felip Manyà Serres (presid.) , Dídac Busquets Font (secret.) , Albert Oliveras Llunell (voc.)
Enlaces
- Tesis en acceso abierto en: TDX
Resumen
- 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.