/////////////////////////////////////////////// // fzn2smt // /////////////////////////////////////////////// Miquel Bofill, Josep Suy, and Mateu Villaret {mbofill,suy,villaret}@ima.udg.edu Departament d'Informàtica i Matemàtica Aplicada Universitat de Girona E-17003 Girona, Spain fzn2smt is a compiler from the FlatZinc language version 1.1 to the standard SMT-LIB language version 1.2 (http://goedel.cs.uiowa.edu/smtlib/). SMT stands for Satisfiability Modulo Theories: the problem of deciding the satisfiability of a formula with respect to background theories --such as linear arithmetic, arrays, etc-- for which specialized decision procedures do exist. fzn2smt was designed with the idea in mind of help testing the adequacy of SMT technology outside the field of verification, where it has its roots. It aims at solving CSP instances with state-of-the art SMT solvers, by taking profit of recent advances in this tools and other already well-established and powerful implementation features of SAT technology such as non-chronological backtracking, learning and restarts, which seem to be rarely exploited in the context of Constraint Programming. fzn2smt supports all standard data types and constraints of FlatZinc. The logic required for solving each instance is determined automatically during the translation, and the translation is done in a straightforward way at the current stage of development. Search annotations are ignored, as they do not make sense in the context of SMT. Only the alldifferent and cumulative MiniZinc global constraints are supported (encoding them into SMT). The fzn2smt compiler is written in Java, and uses the ANTLR runtime (http://www.antlr.org/) for parsing. Working in cooperation with an SMT solver, fzn2smt is able to solve decision problems as well as optimization problems. However, since most SMT solvers do no support optimization, we have currently implemented it by means of iterative calls performing a binary search on the domain of the variable to optimize. This distribution of fzn2smt works in conjunction with Yices 2 (http://yices.csl.sri.com/), with the authorization of their authors, and is intended to be used only in the MiniZinc Challenge 2010. Nevertheless, the output of fzn2smt could be fed into any SMT solver supporting the standard SMT-LIB language. In order to participate in the MiniZinc Challenge, we have implemented a translator for converting the Yices output to the required format. A standalone free version of fzn2smt can be downloaded from http://ima.udg.edu/Recerca/GrupESLIP.html