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.