A satisfiability modulo theories approach to constraint programming

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.