OptiMathSAT

An Optimization Modulo Theories (OMT) tool

FlatZinc 1.6 Language Support

OptiMathSAT (>= 1.5.1) 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 several global constraints.
See MiniZinc ⇒ FlatZinc Translation instructions below.

Important Notes:

Usage

These examples require OptiMathSAT version 1.5.1 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.

Option -opt.fzn.all_solutions=[True|False] and -opt.fzn.max_solutions=INT can be used to print all solutions of the input formula.

Option -opt.fzn.partial_solutions=[True|False] can be used to print any sub-optimal solution found along the optimization search.


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

Then, OptiMathSAT should be run with the following options:
~$ ./optimathsat -model_generation=True \
                 -opt.print_objectives=True \
                 -opt.par.mode=CALLBACK \
                 < FILENAME.smt2


Examples

A few examples are included in OptiMathSAT binary distribution.

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