MiniZinc

MiniZinc has a similar goal to this project: a common modelling interface for many underlying solvers. It is based on a similar concept to that of bridges, but with much less flexibility: each high-level constraint is mapped in a fixed way onto lower-level constraints.

• Basic CP constraints:
  • Domain:
    • Fixed: CP.Domain
    • Variable: CP.Membership
    • Multivalued: CP.VectorDomain
      • table: one binary variable per possible combination
  • All different:
    • Base: CP.AllDifferent
      • all_different: mapped onto a MILP-like model.
      • all_different_reif: similar, with an equivalence.
      • These constraints are available in two includes: all_different.mzn and alldifferent.mzn.
    • All different except constants: CP.AllDifferentExceptConstants
      • alldifferent_except_0 (one excluded value: 0) and alldifferent_except (set of excluded values): either mapped onto neq and disjunctions or onto GCC.
      • alldifferent_except_0_reif (one excluded value: 0) and alldifferent_except_reif (set of excluded values): the reified versions are only mapped onto neq and disjunctions.
    • With symmetry: SymmetricAllDifferent
      • symmetric_all_different: all_different and inverse
      • symmetric_all_different: similar, with an equivalence
  • All equal: CP.AllEqual
    • all_equal: mapped onto a series of equalities if the dimension is at least two.
    • all_equal_reif: similar, with an equivalence.
  • Counting: CP.Count; variants of Minizinc's count are not equivalent to the parameters of CP.Count, Minizinc only matches CP.Count{MOI.EqualTo}
    • count_eq: direct comparison of each element.
    • count_eq_reif: similar, with an equivalence.
    • count_neq, count_lt, count_le, count_gt, count_ge: count_eq with a !=, <, <=, >, >= constraint.
    • count_neq_reif, count_lt_reif, count_le_reif, count_gt_reif, count_ge_reif: similar, with an equivalence.
    • exactly: simple variation of count, not directly mapped in this package.
    • global_cardinality: simple variation of count.
    • global_cardinality_fn: function, simple variation of count.
    • global_cardinality_closed: simple variation of count with domains.
    • global_cardinality_closed_fn: function, simple variation of count.
    • nvalue: simple variation of reified comparisons.
    • nvalue_reif: similar, with an equivalence.
    • nvalue_fn: function.
  • Inversion: CP.Inverse
    • inverse: index computations.
    • inverse_reif: similar, wih an equivalence.
    • Also available as a function.
    • inverse_in_range: ?.
  • Sliding sum: CP.SlidingSum
    • sliding_sum: quite complex mapping.
    • sliding_sum_reif: similar, with an equivalence.
  • Precedence: CP.ValuePrecedence
    • value_precede: [several reifications)(https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fznvalueprecede_int.mzn).
    • [No reified variant)(https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fznvalueprecedeintreif.mzn).
• Combinatorial sets:
  • Bin packing:
    • Raw: CP.BinPacking (with supplementary load variables)
      • bin_packing: mapped onto a MILP-like model, but without binary variables (replaced by their definition in the capacity constraint: bin[item] == value).
      • bin_packing_reif: similar, with an equivalence.
    • Capacitated: CP.FixedCapacityBinPacking and CP.VariableCapacityBinPacking (with supplementary load variables)
      • bin_packing_capa: same MILP-like model with a linear capacity constraint.
      • bin_packing_capa_reif: similar, with an equivalence.
    • Load: CP.BinPacking
      • bin_packing_load: similar MILP-like model.
      • bin_packing_load_reif: similar MILP-like model.
    • Function: CP.BinPacking and CP.BinPackingLoadFunction
      • bin_packing_load_fn directly returns the load variables.
  • Knapsack: CP.Knapsack with values
    • knapsack: mapped onto a MILP model.
    • knapsack_reif: similar, with an equivalence.
• Sorting:
  • Maximum/minimum: CP.MaximumAmong and CP.MinimumAmong
    • maximum: built-in, except for linear solvers
    • minimum: built-in, except for linear solvers
    • No reification available.
  • Argument maximum/minimum: CP.ArgumentMaximumAmong and CP.MinimumAmong
    • arg_max: complex mapping from The ARGMAX Constraint, CP2020.
    • arg_min: complex mapping from The ARGMAX Constraint, CP2020.
    • No reification available.
  • Permutation to sort: CP.SortPermutation
    • arg_sort: alldifferent and array indexing.
    • No reification available.
  • Sort: CP.Sort
    • sort: alldifferent, increasing and array indexing, highly similar to arg_sort.
    • sort_reif: equivalence, indicating whether a given array is a sorted copy of another.
    • sort_fn: returns the sorted array, based on sort.
  • Increasing and decreasing: CP.Increasing, CP.Decreasing, and CP.Strictly
    • increasing: sequence of inequalities.
    • decreasing: sequence of inequalities.
    • strictly_increasing: sequence of strict inequalities.
    • strictly_decreasing: sequence of strict inequalities.
    • No reification available.
  • Lexicographic sorting: CP.LexicographicallyLessThan, CP.LexicographicallyGreaterThan, CP.DoublyLexicographicallyLessThan, and CP.DoublyLexicographicallyGreaterThan
    • lex_greater, lex_less, lex_greatereq, lex_lesseq: implemented using the definition of lexicographic sorting.
    • lex_chain_greater, lex_chain_less, lex_chain_greatereq, lex_chain_lesseq: lexicographic sort of a matrix of vectors, mapped to lexicographic relation between two arrays.
    • lex2: in a matrix, have both rows and columns lexicographically sorted, mapped to two chains.
    • strict_lex2: in a matrix, have both rows and columns strictly lexicographically sorted, mapped to two chains.
    • Reifications are available.
• Scheduling:
  • Rectangle overlapping: CP.NonOverlappingOrthotopes
    • diffn: mapped to a disjunction of linear inequalities.
    • diffn_k: generalisation to k dimensions.
    • No reification available, but a similar mapping is available.