fzn2smt

What is fzn2smt?

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.

Versions

Install instructions

  1. Unpack the fzn2smt.zip file
  2. Download and unpack the ANTLR runtime (read its terms of use)
  3. Download an SMT solver: default Yices 2 (read its terms of use)
  4. Add the following to the CLASSPATH environment variable:
  5. Add to the PATH the folder where you uncompressed fzn2smt.zip

  6. For usage, see the help:

    java fzn2smt -h

    Note: For large flatzinc files it is appropriate to extend the Java heap memory.
    Use "java -XmxYYYYM fzn2smt ...", where YYYY must be greater than 1024.

    Example: java -Xmx2048M fzn2smt -ce "./yices2/bin/yices -f" -i file.fzn

License

License

Miquel Bofill, Miquel Palahí, Josep Suy, and Mateu Villaret 
Departament d'Informàtica i Matemàtica Aplicada
Universitat de Girona
E-17003 Girona, Spain

Contact: suy@ima.udg.edu