MiniZinc Documentation - Standard Library

These constraints represent high-level modelling abstractions, for which many solvers implement special, efficient inference algorithms.

Sections:

Declarations in this section:

Functions and Predicates
function var int: arg_max(array [int] of var int: x) =
let {constraint length(x) > 0,} in (arg_max_total(x))
(standard decomposition from arg_max.mzn:5)

Returns the index of the maximum value in the array x. When breaking ties the least index is returned.

function var int: arg_max(array [int] of var float: x) =
let {constraint length(x) > 0,} in (arg_max_total(x))
(standard decomposition from arg_max.mzn:12)

Returns the index of the maximum value in the array x. When breaking ties the least index is returned.

function var int: arg_min(array [int] of var int: x) =
let {constraint length(x) > 0,} in (arg_min_total(x))
(standard decomposition from arg_min.mzn:5)

Returns the index of the minimum value in the array x. When breaking ties the least index is returned.

function var int: arg_min(array [int] of var float: x) =
let {constraint length(x) > 0,} in (arg_min_total(x))
(standard decomposition from arg_min.mzn:12)

Returns the index of the minimum value in the array x. When breaking ties the least index is returned.

predicate circuit(array [int] of var int: x) =
let { set of int: S = index_set(x), int: l = min(S), int: n = card(S), array [S] of var 1..n: order, } in ( alldifferent(x) /\ alldifferent(order) /\ forall ( i in S ) ( x[i]!=i ) /\ order[l]==1 /\ forall ( i in S ) ( order[i]!=n -> order[x[i]]==order[i]+1 ) /\ forall ( i in S ) ( order[i]==n -> x[i]==l ))
(standard decomposition from circuit.mzn:7)

Constrains the elements of x to define a circuit where x[i] = j means that j is the successor of i.

predicate disjoint(var set of int: s1, var set of int: s2) =
s1 intersect s2=={}
(standard decomposition from disjoint.mzn:2)

Requires that sets s1 and s2 do not intersect.

predicate maximum(var int: m, array [int] of var int: x) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: ly = lb_array(x), int: uy = ub_array(x), array [l..u] of var ly..uy: y, } in ( y[l]==x[l] /\ m==y[u] /\ forall ( i in l+1..u ) ( y[i]==max(x[i], y[i-1]) ))
(standard decomposition from redefinitions-2.0.mzn:11)

Constrains m to be the maximum of the values in x.

Assumptions: |x| > 0.

predicate maximum(var float: m, array [int] of var float: x) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), float: ly = lb_array(x), float: uy = ub_array(x), array [l..u] of var ly..uy: y, } in ( y[l]==x[l] /\ m==y[u] /\ forall ( i in l+1..u ) ( y[i]==max(x[i], y[i-1]) ))
(standard decomposition from redefinitions-2.0.mzn:21)

Constrains m to be the maximum of the values in x.

Assumptions: |x| > 0.

predicate maximum_arg(array [int] of var int: x, var int: i) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: ly = lb_array(x), int: uy = ub_array(x), array [l..u] of var ly..uy: y, array [l..u] of var l..u: mi, } in ( y[l]==x[l] /\ mi[l]==l /\ i==mi[u] /\ forall ( j in l+1..u ) ( y[j]==max(x[j], y[j-1]) /\ mi[j]==if y[j-1]>=x[j] then mi[j-1] else j endif ))
(standard decomposition from arg_max_int.mzn:1)

Constrain i to be the index of the maximum value in the array x. When breaking ties the least index is returned. Assumption: |x| > 0

predicate maximum_arg(array [int] of var float: x, var int: i) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), float: ly = lb_array(x), float: uy = ub_array(x), array [l..u] of var ly..uy: y, array [l..u] of var l..u: mi, } in ( y[l]==x[l] /\ mi[l]==l /\ i==mi[u] /\ forall ( j in l+1..u ) ( y[j]==max(x[j], y[j-1]) /\ mi[j]==if y[j-1]>=x[j] then mi[j-1] else j endif ))
(standard decomposition from arg_max_float.mzn:1)

Constrain i to be the index of the maximum value in the array x. When breaking ties the least index is returned. Assumption: |x| > 0

predicate member(array [int] of var bool: x, var bool: y) =
exists ( i in index_set(x) ) ( x[i]==y )
(standard decomposition from member_bool.mzn:5)

Requires that y occurs in the array x.

predicate member(array [int] of var float: x, var float: y) =
exists ( i in index_set(x) ) ( x[i]==y )
(standard decomposition from member_float.mzn:5)

Requires that y occurs in the array x.

predicate member(array [int] of var int: x, var int: y) =
exists ( i in index_set(x) ) ( x[i]==y )
(standard decomposition from member_int.mzn:5)

Requires that y occurs in the array x.

predicate member(array [int] of var set of int: x, var set of int: y) =
exists ( i in index_set(x) ) ( x[i]==y )
(standard decomposition from member_set.mzn:5)

Requires that y occurs in the array x.

predicate member(var set of int: x, var int: y) =
y in x
(standard decomposition from set_member.mzn:5)

Requires that y occurs in the set x.

predicate minimum(var float: m, array [int] of var float: x) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), float: ly = lb_array(x), float: uy = ub_array(x), array [l..u] of var ly..uy: y, } in ( y[l]==x[l] /\ m==y[u] /\ forall ( i in l+1..u ) ( y[i]==min(x[i], y[i-1]) ))
(standard decomposition from redefinitions-2.0.mzn:41)

Constrains m to be the minimum of the values in x.

Assumptions: |x| > 0.

predicate minimum(var int: m, array [int] of var int: x) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: ly = lb_array(x), int: uy = ub_array(x), array [l..u] of var ly..uy: y, } in ( y[l]==x[l] /\ m==y[u] /\ forall ( i in l+1..u ) ( y[i]==min(x[i], y[i-1]) ))
(standard decomposition from redefinitions-2.0.mzn:31)

Constrains m to be the minimum of the values in x.

Assumptions: |x| > 0.

predicate minimum_arg(array [int] of var int: x, var int: i) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: ly = lb_array(x), int: uy = ub_array(x), array [l..u] of var ly..uy: y, array [l..u] of var l..u: mi, } in ( y[l]==x[l] /\ mi[l]==l /\ i==mi[u] /\ forall ( j in l+1..u ) ( y[j]==min(x[j], y[j-1]) /\ mi[j]==if y[j-1]<=x[j] then mi[j-1] else j endif ))
(standard decomposition from arg_min_int.mzn:1)

Constrain i to be the index of the minimum value in the array x. When breaking ties the least index is returned. Assumption: |x| > 0

predicate minimum_arg(array [int] of var float: x, var int: i) =
let { int: l = min(index_set(x)), int: u = max(index_set(x)), float: ly = lb_array(x), float: uy = ub_array(x), array [l..u] of var ly..uy: y, array [l..u] of var l..u: mi, } in ( y[l]==x[l] /\ mi[l]==l /\ i==mi[u] /\ forall ( j in l+1..u ) ( y[j]==min(x[j], y[j-1]) /\ mi[j]==if y[j-1]<=x[j] then mi[j-1] else j endif ))
(standard decomposition from arg_min_float.mzn:1)

Constrain i to be the index of the minimum value in the array x. When breaking ties the least index is returned. Assumption: |x| > 0

predicate network_flow(array [int,1..2] of int: arc, array [int] of int: balance, array [int] of var int: flow) =
let { int: source_node = 1, int: sink_node = 2, set of int: ARCS = index_set_1of2(arc), set of int: NODES = index_set(balance), } in ( assert(ARCS==index_set(flow) /\ lb_array(arc)>=min(NODES) /\ ub_array(arc)<=max(NODES), "network_flow: wrong sizes of input array parameters", forall ( i in NODES ) ( sum ( j in ARCS where i==arc[j, source_node] ) ( flow[j] )-sum ( j in ARCS where i==arc[j, sink_node] ) ( flow[j] )== balance[i] )))
(standard decomposition from network_flow.mzn:9)

Defines a network flow constraint.

Parameters
  • arc: a directed arc of the flow network. Arc i connects node arc[i,1] to node arc[i,2].
  • balance: the difference between input and output flow for each node.
  • flow: the flow going through each arc.
predicate network_flow_cost(array [int,1..2] of int: arc, array [int] of int: balance, array [int] of int: weight, array [int] of var int: flow, var int: cost) =
let { int: source_node = 1, int: sink_node = 2, set of int: ARCS = index_set_1of2(arc), set of int: NODES = index_set(balance), } in ( assert(ARCS==index_set(flow) /\ ARCS==index_set(weight) /\ lb_array(arc)>=min(NODES) /\ ub_array(arc)<=max(NODES), "network_flow: wrong sizes of input array parameters", cost==sum ( i in ARCS ) ( flow[i]*weight[i] ) /\ forall ( i in NODES ) ( sum ( j in ARCS where i==arc[j, source_node] ) ( flow[j] )-sum ( j in ARCS where i==arc[j, sink_node] ) ( flow[j] )== balance[i] )))
(standard decomposition from network_flow.mzn:39)

Defines a network flow constraint with cost.

Parameters
  • arc: a directed arc of the flow network. Arc i connects node arc[i,1] to node arc[i,2].
  • balance: the difference between input and output flow for each node.
  • weight: the unit cost of the flow through the arc.
  • flow: the flow going through each arc.
  • cost: the overall cost of the flow.
predicate partition_set(array [int] of var set of int: S, set of int: universe) =
all_disjoint(S) /\ universe==array_union ( i in index_set(S) ) ( S[i] )
(standard decomposition from partition_set.mzn:6)

Constrains the sets in array S to partition the universe.

function var set of int: range(array [int] of var int: x, var set of int: s) =
let { var set of lb_array(x)..ub_array(x): t, constraint range(x, s, t), } in (t)
(standard decomposition from range_fn.mzn:8)

Returns the image of function x (represented as an array) on set of values s. ub(s) must be a subset of index_set(x) otherwise an assertion failure will occur.

predicate range(array [int] of var int: x, var set of int: s, var set of int: t) =
assert(ub(s) subset index_set(x), "range: upper bound of \'s\' must be a subset of the index set of \'x\'", forall ( i in ub(s) ) ( i in s -> x[i] in t ) /\ forall ( i in ub(t) ) ( i in t -> exists ( j in ub(s) ) ( j in s /\ x[j]==i ) ))
(standard decomposition from range.mzn:6)

Requires that the image of function x (represented as an array) on set of values s is t. ub(s) must be a subset of index_set(x) otherwise an assertion failure will occur.

function var set of int: roots(array [int] of var int: x, var set of int: t) =
let { var set of index_set(x): s, constraint roots(x, s, t), } in (s)
(standard decomposition from roots_fn.mzn:6)

Returns s such that x[i] in t for all i in s

predicate roots(array [int] of var int: x, var set of int: s, var set of int: t) =
assert(ub(s) subset index_set(x), "roots: upper bound of \'s\' must be a subset of the index set of \'x\'", forall ( i in ub(s) ) ( i in s -> x[i] in t ) /\ forall ( i in ub(t) ) ( i in t -> forall ( j in index_set(x) ) ( x[j]==i -> j in s ) ))
(standard decomposition from roots.mzn:4)

Requires that x[i] in t for all i in s

predicate sliding_sum(int: low, int: up, int: seq, array [int] of var int: vs) =
let { int: lx = min(index_set(vs)), int: ux = max(index_set(vs)), } in ( forall ( i in lx..ux-seq+1 ) ( let {var int: sum_of_l = sum ( j in i..i+seq-1 ) ( vs[j] ), } in (low<=sum_of_l /\ sum_of_l<=up) ))
(standard decomposition from sliding_sum.mzn:5)

Requires that in each subsequence vs[i], ..., vs[i + seq - 1] the sum of the values belongs to the interval [low, up].

predicate subcircuit(array [int] of var int: x) =
let { set of int: S = index_set(x), int: l = min(S), int: u = max(S), int: n = card(S), array [S] of var 1..n: order, array [S] of var bool: ins = array1d(S, [ x[i]!=i | i in S ]), var l..u+1: firstin = min ( i in S ) ( u+1+bool2int(ins[i])*(i-u-1) ), var S: lastin, var bool: empty = firstin > u, } in ( alldifferent(x) /\ alldifferent(order) /\ (empty -> forall ( i in S ) ( not ins[i] )) /\ (not empty -> order[firstin]==1 /\ lastin > firstin /\ x[lastin]==firstin /\ ins[lastin] /\ ins[firstin] /\ forall ( i in S ) ( ins[i] /\ x[i]!=firstin -> order[x[i]]==order[i]+1 ) /\ forall ( i in S ) ( ins[i] \/ order[lastin] < order[i] )))
(standard decomposition from subcircuit.mzn:8)

Constrains the elements of x to define a subcircuit where x[i] = j means that j is the successor of i and x[i] = i means that i is not in the circuit.

predicate sum_pred(var int: i, array [int] of set of int: sets, array [int] of int: cs, var int: s) =
s==sum ( j in index_set(cs) ) ( bool2int(j in sets[i])*cs[j] )
(standard decomposition from sum_pred.mzn:9)

Requires that the sum of cs[i1]..cs[iN] equals s, where i1..iN are the elements of the i th set in sets.

Nb: not called 'sum' as in the constraints catalog because 'sum' is a MiniZinc built-in function.