A satisfiability modulo theories approach to constraint programming
dc.contributor.author
dc.date.accessioned
2015-01-21T12:09:59Z
dc.date.available
2015-01-21T12:09:59Z
dc.date.issued
2012-12-20
dc.identifier.other
Gi. 150-21013
dc.identifier.uri
dc.description.abstract
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.
Aquesta tesi es centra en la resolució de CSPs utilitzant SMT. En essència, es reformulen els CSPs a fórmules SMT. Els resultats obtinguts permeten concloure que els millors solucionadors actuals d'SMT són una eina sòlida per a resoldre CSPs. No només s'aborden els CSP decisionals, sinó també problemes d'optimització de restriccions i problemes de satisfactibilitat de restriccions amb pesos. Per a resoldre aquests problemes s'ha utilitzat SMT juntament amb els algorismes apropiats: algorismes de cerca i algorismes basats en nuclis d'insatisfactibilitat. També es dóna suport a meta-restriccions, és a dir, restriccions sobre restriccions. Un cop vist que SMT és una molt bona aproximació genèrica per a CP, s'ha comprovat com algorismes basats en SMT poden tenir un rendiment igual o millor que els programes dissenyats específicament per a un determinat problema. El problema seleccionat per a dur a terme aquesta comprovació ha estat el RCPSP, obtenint uns resultats altament competitius.
dc.format.mimetype
application/pdf
dc.language.iso
eng
dc.publisher
Universitat de Girona
dc.rights
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/
dc.source
TDX (Tesis Doctorals en Xarxa)
dc.subject
dc.subject.other
dc.title
A satisfiability modulo theories approach to constraint programming
dc.type
info:eu-repo/semantics/doctoralThesis
dc.rights.accessRights
info:eu-repo/semantics/openAccess
dc.contributor.director
dc.subject.udc
dc.type.version
info:eu-repo/semantics/publishedVersion