Item


Reformulation of constraint models into SMT

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.

Universitat de Girona

Other contributions: Universitat de Girona. Departament d’Informàtica, Matemàtica Aplicada i Estadística (2013-)
Author: Palahí i Sitges, Miquel
Date: 2015 December 10
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.
Format: application/pdf
Other identifiers: http://hdl.handle.net/10803/392163
Document access: http://hdl.handle.net/10256/12639
Language: eng
Publisher: Universitat de Girona
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-nc-sa/3.0/es/
Subject: Constraint programming
Programació amb restriccions
Programación con restricciones
Boolean satisfiability
Satisfactibilitat booleana
Satisfactibilidad booleana
004 - Informàtica
51 - Matemàtiques
Title: Reformulation of constraint models into SMT
Type: info:eu-repo/semantics/doctoralThesis
Repository: DUGiDocs

Subjects

Authors