My Constraint Programming Blog

One of the new contestants in MiniZinc Challenge 2010 was fzn2smt and it did quite well:

• Silver medal in the Free search category
• Tied gold medal (with Gecode) in the Parallel search category

(For more details about the challenge, see the CP2010 presentation.)

From the fzn2smt page:

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 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 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.

The output of fzn2smt could be fed into any SMT solver supporting the standard SMT-LIB language. By default 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.

See the fzn2smt page for installation instructions.

Some comments

fzn2smt can sometimes solve problems fast where other more "traditional" CP solvers takes longer time. However, since fzn2smt can only generate a single solution it is less useful for problems when all solutions are required, or for checking if a problem has a unique solution (e.g. for debugging a model). Since I use fzn2smt mostly for harder/larger problem I allow Java 4Gb of use: java -Xmx4096M fzn2smt -ce "yices -f" -i file.fzn

It's great that we now have yet another powerful tool for solving MiniZinc/FlatZinc problems.