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, int2tfloatThe 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_reifFurthermore, 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_log2OptiMathSAT 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_setSee MiniZinc ⇒ FlatZinc Translation instructions below to make use of this special handling.
solve minimize cost1, maximize cost2;Option -opt.priority=[box|lex|par] can be used to select the multi-objective optimization mode:
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
~$ mzn2fzn -G smt2 model_file.mzn [data_file.dzn] \ -o output_file.fzn
~$ ./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.fznThen, OptiMathSAT should be run with the following options:
~$ ./optimathsat -model_generation=True \ -opt.print_objectives=True \ -opt.par.mode=CALLBACK \ < FILENAME.smt2
A few examples are included in OptiMathSAT binary distribution.
A richer library of FlatZinc 1.6 examples can be
found HERE.