Reformulation of constraint models into SMT
Full Text
Share
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.
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/