OptiMathSAT

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:

• OptiMathSAT allows for multi-objective optimization, e.g.

  solve minimize cost1, maximize cost2;
  

  Option -opt.priority=[box|lex|par] can be used to select the multi-objective optimization mode:
  • par: the Pareto-front is explored
    
  • lex: objectives are optimized in lexicographic order
    In the example, OptiMathSAT prints one optimum model resulting from the opimization of cost2 after cost1 is fixed at its optimum value
    
  • box: each objective is handled independently from the others
    In the example, OptiMathSAT prints one optimum model for cost1 and one for cost2
    
• OptiMathSAT uses infinite precision arithmetic
• OptiMathSAT assumes any unbounded int or float variable to have domain in ]-INF, +INF[
• OptiMathSAT ignores all annotations except for ::output_var and ::output_array(...)
• OptiMathSAT may be able to solve some sources of non-linearity in the encoding of the problem if all bool2int constraints appear at the beginning of the constraints section

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.