2024-03-29T10:08:54Zhttps://www.tdx.cat/oai/requestoai:www.tdx.cat:10803/3921632022-12-08T19:30:55Zcom_10803_253col_10803_98301
TDX (Tesis Doctorals en Xarxa)
author
Palahí i Sitges, Miquel
authoremail
miquel.bofill@udg.edu
authoremailshow
false
director
Bofill Arasa, Miquel
director
Villaret Ausellé, Mateu
authorsendemail
true
2016-08-02T09:18:21Z
2016-08-02T09:18:21Z
2015-12-10
http://hdl.handle.net/10803/392163
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.
eng
Constraint programming
Programació amb restriccions
Programación con restricciones
Boolean satisfiability
Satisfactibilitat booleana
Satisfactibilidad booleana
Reformulation of constraint models into SMT
info:eu-repo/semantics/doctoralThesis info:eu-repo/semantics/publishedVersion
URL
https://www.tdx.cat/bitstream/10803/392163/8/tmps1de1.pdf
File
MD5
bf90a337b3446b10dba8973cc11caa15
1700523
application/pdf
tmps1de1.pdf
URL
https://www.tdx.cat/bitstream/10803/392163/6/tmps1de1.pdf.txt
File
MD5
d41d8cd98f00b204e9800998ecf8427e
0
text/plain
tmps1de1.pdf.txt