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.

The following constraints are fully supported:

array_bool_and, array_bool_element, array_bool_or, array_bool_xor, 
array_float_element, array_int_element, array_set_element, 
array_var_bool_element, array_var_float_element, array_var_int_element, 
array_var_set_element, bool_and, bool_clause, bool_eq, bool_eq_reif, 
bool_le, bool_le_reif, bool_lin_eq, bool_lin_le, bool_lt, bool_lt_reif, 
bool_not, bool_or, bool_xor, float_abs, float_eq, float_eq_reif, 
float_le, float_le_reif, float_lt, float_lt_reif, float_max, float_min, 
float_ne, float_ne_reif, float_plus, float_times, float_div, int_abs,
int_eq, int_eq_reif, int_le, int_le_reif, int_lt, int_lt_reif, int_max,
int_min, int_ne, int_ne_reif, int_plus, set_card, set_diff, set_eq,
set_eq_reif, set_in, set_in_reif, set_intersect, set_le, set_lt, set_ne,
set_ne_reif, set_subset, set_subset_reif, set_symdiff, set_union, bool2int, 
int2tfloat
The following constraints are supported only as long as no non-linearity is introduced:
ind_div, int_mod, int_times, int_lin_eq, int_lin_eq_reif, int_lin_le,
int_lin_le_reif, int_lin_ne, int_lin_ne_reif, float_lin_eq, 
float_lin_eq_reif, float_lin_le, float_lin_le_reif, float_lin_lt, 
float_lin_lt_reif, float_lin_ne, float_lin_ne_reif
Furthermore, the following constraints are currently not supported
float_acos, float_asin, float_atan, float_cos, float_cosh, float_sin, 
float_sinh, float_tan, float_tanh, float_exp, float_sqrt, float_ln,
float_log10, float_log2
OptiMathSAT has an optional special handling for some global constraints:
among, alldifferent_except_0, alldifferent_int, alldifferent_set, 
at_least_int, at_least_set, at_most_int, at_most_set, atmost1, count_eq, 
count_geq, count_gt, count_leq, count_lt, count_neq, exactly_int, 
exactly_set
See MiniZinc ⇒ FlatZinc Translation instructions below to make use of this special handling.

Important Notes:

Usage

NEW: fzn2omt, an open source project that makes it easy to use OptiMathSAT, Barcelogic, Z3 and CVC4 with FlatZinc!

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
    
For the best performance, you can use the emzn2fzn compiler instead of mzn2fzn.

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.