Reformulation of constraint models into SMT

Abstract

In this thesis we focus on reformulate constraint satisfaction problems (CSP)

into SAT Modulo Theories (SMT). SMT is an extension of SAT where the literals

appearing in the formulas are not restricted to contain only propositional

variables, instead they can have predicates from other theories, e.g., linear

integer arithmetic.

We present two systems developed to reformulate CSPs into SMT (fzn2smt and

WSimply). The first one, reads instances written in FlatZinc and solved using

an external SMT solver, and it has been extended to also solve optimization

problems (COP) which are not supported by SMT solvers. The second one reads

CSP, COP and weighted CSPs (WCSP) written in its own high level declarative

language, which in addition to reformulate into SMT also reformulates into

pseudo-Boolean and linear programming formats.

We also present an incremental optimization algorithm based on using Binary

Decision Diagrams (BDD) to solve WCSPs.

La tesi es centra en la reformulació de problemes de satisfacció de

restriccions (CSP) a SAT Mòdul Teories (SMT). SMT és una extensió de SAT on

els literals que apareixen a la fórmula no estan limitats a contenir només

variables Booleanes, sinó que poden tenir-hi predicats d’altres teories,

e.g., aritmètica lineal entera.

Presenta dos sistemes desenvolupats per reformular CSPs a SMT (fzn2smt i

WSimply). El primer llegeix instàncies CSPs escrites en FlatZinc que són

resoltes mitjançant un resoledor SMT extern, i s’ha estès per resoldre

problemes d'optimització (COP) que per defecte no són suportats pels

resoledors SMT. El segon llegeix instàncies CSPs, COP i CSP amb pesos (WCSP)

escrites en el seu propi llenguatge declaratiu d'alt nivell, que a més a més

de reformular-les a SMT es poden reformular a format pseudo-Booleà i

programació lineal.

Presenta un algorisme d'optimització incremental basat en diagrames de

decisió binaris per a resoldre WCSPs.