fzn2smt is a compiler from the FlatZinc language to the standard SMT-LIB language version 1.2. 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 these 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 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 binary search on the domain of the variable to optimize.
The output of fzn2smt can be fed into any SMT solver supporting the standard SMT-LIB language. By default the system works in conjunction with Yices 2 with the authorization of their authors, and was intended to be used only in the MiniZinc Challenge 2010, where the tool made good results.