OptiMathSAT

An Optimization Modulo Theories (OMT) tool

FlatZinc 1.6 Language Support

OptiMathSAT (>= 1.4.0) has an experimental support to a subset of the FlatZinc 1.6 input language.

In particular, the following constraints are currently not supported:


Some constraints are supported as long as no non-linearity is introduced:
In addition, OptiMathSAT provides special support for the following global constraints:
Relevant differences with FlatZinc 1.6:

Usage

These examples require OptiMathSAT version 1.4.0 or superior.

All the examples can be run like this:

~$ ./optimathsat -input=fzn < FILENAME.fzn

FlatZinc ⇒ SMT2 Translation

It is possible to use OptiMathSAT to convert supported fzn problems into the smt2 format enriched with OptiMathSAT optimization extensions.
~$ ./optimathsat -input=fzn \
		 -debug.api_call_trace=1 \
		 -debug.api_call_trace_dump_config=False \
		 -debug.solver_enabled=False \
		 -debug.api_call_trace_filename=FILENAME.smt2 < FILENAME.fzn


MiniZinc ⇒ FlatZinc Translation

To use OptiMathSAT special support for some global constraints:
  1. Download the smt2.tar.gz package
  2. Unpack its content in ${MINIZINC_PATH}/lib/minizinc
  3. Convert the MiniZinc files:
    ~$ mzn2fzn -G smt2 model_file.mzn [data_file.dzn] \
    		-o output_file.fzn
    				

Examples

A rich library of FlatZinc 1.6 examples can be found HERE.