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:
Important Notes:

Usage

These examples require OptiMathSAT version 1.4.0 or superior.

All the examples can be run like this:

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

Option -opt.strategy=[lin|bin|ada] can be used to select the optimization search strategy.


MiniZinc ⇒ FlatZinc Translation

To use OptiMathSAT special support for some global constraints:
  1. Download the smt2.tar.gz package
  2. Unpack its content inside MiniZinc global constraints directory
    • for MiniZinc version 1.X, ${MINIZINC_PATH}/lib/minizinc
    • for MiniZinc version 2.X, ${MINIZINC_PATH}/share/minizinc
  3. Convert the MiniZinc files:
    ~$ mzn2fzn -G smt2 model_file.mzn [data_file.dzn] \
    		-o output_file.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


Examples

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