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, 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

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.