# 4.2.1. Global constraints¶

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

## 4.2.1.1. Counting constraints¶

These constraints count and restrict how many times certain values occur in an array of variables. MiniZinc will automatically generate the basic counting constraints below from expressions such as count(i in x)(i=c) <= d, so you can write models in this much more readable style instead of using these predicates. However, if your model contains multiple counting constraints over the same array, constraints like distribute or global_cardinality below may be useful.

predicate among(var int: n, array [$X] of var int: x, set of int: v)  Requires exactly n variables in x to take one of the values in v . More… function var int: among(array [int] of var int: x, set of int: v)  Returns the number of variables in x that take one of the values in v . More… predicate at_least(int: n, array [$X] of var set of int: x,
set of int: v)


Requires at least n variables in x to take the value v .

More…

predicate at_most(int: n,
array [$X] of var set of int: x, set of int: v)  Requires at most n variables in x to take the value v . More… predicate at_most1(array [$X] of var set of int: s)


Requires that each pair of sets in s overlap in at most one element.

More…

function var int: count(array [$X] of var int: x, var int: y)  Returns the number of occurrences of y in x . More… predicate count(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be the number of occurrences of y in x .

More…

predicate count_eq(array [$X] of var int: x, var int: y, var int: c)  Constrains c to be the number of occurrences of y in x . More… predicate count_eq(array [$X] of var int: x, int: y, int: c)


Constrains c to be the number of occurrences of y in x .

More…

function var int: count_eq(array [$X] of var int: x, var int: y)  Returns the number of occurrences of y in x . More… predicate count_geq(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be greater than or equal to the number of occurrences of y in x .

More…

predicate count_geq(array [$X] of var int: x, int: y, int: c)  Constrains c to be greater than or equal to the number of occurrences of y in x . More… predicate count_gt(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be strictly greater than the number of occurrences of y in x .

More…

predicate count_gt(array [$X] of var int: x, int: y, int: c)  Constrains c to be strictly greater than the number of occurrences of y in x . More… predicate count_leq(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be less than or equal to the number of occurrences of y in x .

More…

predicate count_leq(array [$X] of var int: x, int: y, int: c)  Constrains c to be less than or equal to the number of occurrences of y in x . More… predicate count_lt(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be strictly less than the number of occurrences of y in x .

More…

predicate count_lt(array [$X] of var int: x, int: y, int: c)  Constrains c to be strictly less than the number of occurrences of y in x . More… predicate count_neq(array [$X] of var int: x, var int: y, var int: c)


Constrains c to be not equal to the number of occurrences of y in x .

More…

predicate count_neq(array [$X] of var int: x, int: y, int: c)  Constrains c to be not equal to the number of occurrences of y in x . More… predicate distribute(array [$X] of var int: card,
array [$X] of var int: value, array [$Y] of var int: base)


Requires that card [ i ] is the number of occurrences of value [ i ] in base . The values in value need not be distinct.

More…

function array [$X] of var int: distribute(array [$X] of var int: value,
array [$Y] of var int: base)  Returns an array of the number of occurrences of value [ i ] in base . The values in value need not be distinct. More… predicate exactly(int: n, array [$X] of var set of int: x,
set of int: v)


Requires exactly n variables in x to take the value v .

More…

predicate global_cardinality(array [$X] of var int: x, array [$Y] of int: cover,
array [$Y] of var int: counts)  Requires that the number of occurrences of cover [ i ] in x is counts [ i ]. More… function array [$Y] of var int: global_cardinality(array [$X] of var int: x, array [$Y] of int: cover)


Returns the number of occurrences of cover [ i ] in x .

More…

predicate global_cardinality_closed(array [$X] of var int: x, array [$Y] of int: cover,
array [$Y] of var int: counts)  Requires that the number of occurrences of cover [ i ] in x is counts [ i ]. The elements of x must take their values from cover . More… function array [$Y] of var int: global_cardinality_closed(array [$X] of var int: x, array [$Y] of int: cover)


Returns an array with number of occurrences of cover [ i ] in x .

The elements of x must take their values from cover .

More…

predicate global_cardinality_low_up(array [$X] of var int: x, array [$Y] of int: cover,
array [$Y] of int: lbound, array [$Y] of int: ubound)


Requires that for all i , the value cover [ i ] appears at least lbound [ i ] and at most ubound [ i ] times in the array x .

More…

predicate global_cardinality_low_up_closed(array [$X] of var int: x, array [$Y] of int: cover,
array [$Y] of int: lbound, array [$Y] of int: ubound)


Requires that for all i , the value cover [ i ] appears at least lbound [ i ] and at most ubound [ i ] times in the array x .

The elements of x must take their values from cover .

More…

## 4.2.1.3. Lexicographic constraints¶

predicate lex2(array [int,int] of var int: x)


More…

predicate lex_greater(array [int] of var bool: x,
array [int] of var bool: y)


Requires that the array x is strictly lexicographically greater than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greater(array [int] of var int: x,
array [int] of var int: y)


Requires that the array x is strictly lexicographically greater than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greater(array [int] of var float: x,
array [int] of var float: y)


Requires that the array x is strictly lexicographically greater than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greater(array [int] of var set of int: x,
array [int] of var set of int: y)


Requires that the array x is strictly lexicographically greater than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greatereq(array [int] of var bool: x,
array [int] of var bool: y)


Requires that the array x is lexicographically greater than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greatereq(array [int] of var int: x,
array [int] of var int: y)


Requires that the array x is lexicographically greater than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greatereq(array [int] of var float: x,
array [int] of var float: y)


Requires that the array x is lexicographically greater than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_greatereq(array [int] of var set of int: x,
array [int] of var set of int: y)


Requires that the array x is lexicographically greater than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_less(array [int] of var bool: x,
array [int] of var bool: y)


Requires that the array x is strictly lexicographically less than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_less(array [int] of var int: x,
array [int] of var int: y)


Requires that the array x is strictly lexicographically less than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_less(array [int] of var float: x,
array [int] of var float: y)


Requires that the array x is strictly lexicographically less than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_less(array [int] of var set of int: x,
array [int] of var set of int: y)


Requires that the array x is strictly lexicographically less than array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_lesseq(array [int] of var bool: x,
array [int] of var bool: y)


Requires that the array x is lexicographically less than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_lesseq(array [int] of var float: x,
array [int] of var float: y)


Requires that the array x is lexicographically less than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_lesseq(array [int] of var int: x,
array [int] of var int: y)


Requires that the array x is lexicographically less than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate lex_lesseq(array [int] of var set of int: x,
array [int] of var set of int: y)


Requires that the array x is lexicographically less than or equal to array y . Compares them from first to last element, regardless of indices.

More…

predicate seq_precede_chain(array [int] of var int: x)


Requires that i precedes i +1 in the array x for all positive i .

More…

predicate seq_precede_chain(array [int] of var set of int: x)


Requires that i appears in a set in array x before i +1 for all positive i

More…

predicate strict_lex2(array [int,int] of var int: x)


More…

predicate value_precede(int: s, int: t, array [int] of var int: x)


Requires that s precede t in the array x .

Precedence means that if any element of x is equal to t , then another element of x with a lower index is equal to s .

More…

predicate value_precede(int: s, int: t, array [int] of var opt int: x)


Requires that s precede t in the array x .

Precedence means that if any element of x is equal to t , then another element of x with a lower index is equal to s .

More…

predicate value_precede(int: s,
int: t,
array [int] of var set of int: x)


Requires that s precede t in the array x .

Precedence means that if an element of x contains t but not s , then another element of x with lower index contains s but not t .

More…

predicate value_precede_chain(array [int] of int: c,
array [int] of var int: x)


Requires that c [ i ] precedes c [ i +1] in the array x .

Precedence means that if any element of x is equal to c [ i +1], then another element of x with a lower index is equal to c [ i ].

More…

predicate value_precede_chain(array [int] of int: c,
array [int] of var set of int: x)


Requires that c [ i ] precedes c [ i +1] in the array x .

Precedence means that if an element of x contains c [ i +1] but not c [ i ], then another element of x with lower index contains c [ i ] but not c [ i +1].

More…

## 4.2.1.4. Sorting constraints¶

function array [int] of var int: arg_sort(array [int] of var int: x)


Returns the permutation p which causes x to be in sorted order hence x [ p [ i ]] <= x [ p [ i +1]].

The permutation is the stable sort hence x [ p [ i ]] = x [ p [ i +1]] $$\rightarrow$$ p [ i ] < p [ i +1].

More…

function array [int] of var int: arg_sort(array [int] of var float: x)


Returns the permutation p which causes x to be in sorted order hence x [ p [ i ]] <= x [ p [ i +1]].

The permutation is the stable sort hence x [ p [ i ]] = x [ p [ i +1]] $$\rightarrow$$ p [ i ] < p [ i +1].

More…

predicate arg_sort(array [int] of var int: x,
array [int] of var int: p)


Constrains p to be the permutation which causes x to be in sorted order hence x [ p [ i ]] <= x [ p [ i +1]].

The permutation is the stable sort hence x [ p [ i ]] = x [ p [ i +1]] $$\rightarrow$$ p [ i ] < p [ i +1].

More…

predicate arg_sort(array [int] of var float: x,
array [int] of var int: p)


Constrains p to be the permutation which causes x to be in sorted order hence x [ p [ i ]] <= x [ p [ i +1]].

The permutation is the stable sort hence x [ p [ i ]] = x [ p [ i +1]] $$\rightarrow$$ p [ i ] < p [ i +1].

More…

predicate decreasing(array [$X] of var bool: x)  Requires that the array x is in decreasing order (duplicates are allowed). More… predicate decreasing(array [$X] of var float: x)


Requires that the array x is in decreasing order (duplicates are allowed).

More…

predicate decreasing(array [$X] of var int: x)  Requires that the array x is in decreasing order (duplicates are allowed). More… predicate decreasing(array [$X] of var set of int: x)


Requires that the array x is in decreasing order (duplicates are allowed).

More…

predicate increasing(array [$X] of var bool: x)  Requires that the array x is in increasing order (duplicates are allowed). More… predicate increasing(array [$X] of var float: x)


Requires that the array x is in increasing order (duplicates are allowed).

More…

predicate increasing(array [$X] of var int: x)  Requires that the array x is in increasing order (duplicates are allowed). More… predicate increasing(array [$X] of var set of int: x)


Requires that the array x is in increasing order (duplicates are allowed).

More…

predicate sort(array [int] of var int: x, array [int] of var int: y)


Requires that the multiset of values in x are the same as the multiset of values in y but y is in sorted order.

More…

function array [int] of var int: sort(array [int] of var int: x)


Return a multiset of values that is the same as the multiset of values in x but in sorted order.

More…

predicate strictly_increasing(array [$X] of var bool: x)  Requires that the array x is in a stricly increasing order (duplicates are not allowed). More… predicate strictly_increasing(array [$X] of var int: x)


Requires that the array x is in a stricly increasing order (duplicates are not allowed).

More…

predicate strictly_increasing(array [\$X] of var opt int: x)


Requires that the array x is in a stricly increasing order (duplicates are not allowed).

More…

## 4.2.1.5. Channeling constraints¶

predicate int_set_channel(array [int] of var int: x,
array [int] of var set of int: y)


Requires that array of int variables x and array of set variables y are related such that ( x [ i ] = j ) $$\leftrightarrow$$ ( i in y [ j ]).

More…

predicate inverse(array [int] of var int: f,
array [int] of var int: invf)


Constrains two arrays of int variables, f and invf , to represent inverse functions. All the values in each array must be within the index set of the other array.

More…

function array [$$E] of var$$F: inverse(array [$$F] of var$$E: f)


Given a function f represented as an array, return the inverse function.

More…

function array [$$E] of$$F: inverse(array [$$F] of$$E: f)


Given a function f represented as an array, return the inverse function.

predicate inverse_in_range(array [int] of var int: f,
array [int] of var int: invf)


If the i th variable of the collection X is assigned to j and if j is in the index set of Y then the j th variable of the collection Y is assigned to i .

Conversely, if the j th variable of the collection Y is assigned to i and if i is in the index set of X then the i th variable of the collection X is assigned to j .

More…

predicate inverse_set(array [int] of var set of int: f,
array [int] of var set of int: invf)


Constrains two arrays of set of int variables, f and invf , so that a j in f[ i ] iff i in invf[ j ]. All the values in each array’s sets must be within the index set of the other array.

More…

predicate link_set_to_booleans(var set of int: s,
array [int] of var bool: b)


Constrain the array of Booleans b to be a representation of the set s : i in s $$\leftrightarrow$$ b [ i ].

The index set of b must be a superset of the possible values of s .

More…

## 4.2.1.6. Packing constraints¶

predicate bin_packing(int: c,
array [int] of var int: bin,
array [int] of int: w)


Requires that each item i with weight w [ i ], be put into bin [ i ] such that the sum of the weights of the items in each bin does not exceed the capacity c .

Assumptions:

• forall i , w [ i ] >=0
• c >=0

More…

predicate bin_packing_capa(array [int] of int: c,
array [int] of var int: bin,
array [int] of int: w)


Requires that each item i with weight w [ i ], be put into bin [ i ] such that the sum of the weights of the items in each bin b does not exceed the capacity c [ b ].

Assumptions:

• forall i , w [ i ] >=0
• forall b , c [ b ] >=0

More…

predicate bin_packing_load(array [int] of var int: load,
array [int] of var int: bin,
array [int] of int: w)


Requires that each item i with weight w [ i ], be put into bin [ i ] such that the sum of the weights of the items in each bin b is equal to load [ b ].

Assumptions:

• forall i , w [ i ] >=0

More…

function array [int] of var int: bin_packing_load(array [int] of var int: bin,
array [int] of int: w)


Returns the load of each bin resulting from packing each item i with weight w [ i ] into bin [ i ], where the load is defined as the sum of the weights of the items in each bin.

Assumptions:

• forall i , w [ i ] >=0

More…

predicate diffn(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy)


Constrains rectangles i , given by their origins ( x [ i ], y [ i ]) and sizes ( dx [ i ], dy [ i ]), to be non-overlapping. Zero-width rectangles can still not overlap with any other rectangle.

More…

predicate diffn_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size)


Constrains k -dimensional boxes to be non-overlapping. For each box i and dimension j , box_posn [ i , j ] is the base position of the box in dimension j , and box_size [ i , j ] is the size in that dimension. Boxes whose size is 0 in any dimension still cannot overlap with any other box.

More…

predicate diffn_nonstrict(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy)


Constrains rectangles i , given by their origins ( x [ i ], y [ i ]) and sizes ( dx [ i ], dy [ i ]), to be non-overlapping. Zero-width rectangles can be packed anywhere.

More…

predicate diffn_nonstrict_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size)


Constrains k -dimensional boxes to be non-overlapping. For each box i and dimension j , box_posn [ i , j ] is the base position of the box in dimension j , and box_size [ i , j ] is the size in that dimension. Boxes whose size is 0 in at least one dimension can be packed anywhere.

More…

predicate geost(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind)


A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap.

More…

Parameters:

• k: the number of dimensions
• rect_size: the size of each box in k dimensions
• rect_offset: the offset of each box from the base position in k dimensions
• shape: the set of rectangles defining the i -th shape.
• x: the base position of each object. x [ i , j ] is the position of object i in. dimension j .
• kind: the shape used by each object.
predicate geost_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u)


A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global k dimensional bounding box.

More…

Parameters:

• k: the number of dimensions
• rect_size: the size of each box in k dimensions
• rect_offset: the offset of each box from the base position in k dimensions
• shape: the set of rectangles defining the i -th shape.
• x: the base position of each object. x [ i , j ] is the position of object i in dimension j .
• kind: the shape used by each object.
• l: is an array of lower bounds, l [ i ] is the minimum bounding box for all objects in dimension i .
• u: is an array of upper bounds, u [ i ] is the maximum bounding box for all objects in dimension i .
predicate geost_nonoverlap_k(array [int] of var int: x1,
array [int] of int: w1,
array [int] of var int: x2,
array [int] of int: w2)


A global non-overlap constraint for 2 dimensional objects. It enforces that no two objects overlap and zero-length objects do not appear in the middle of other objects.

More…

Parameters:

• x1: first coordinate of each object
• w2: width in first dimension for each object
• x2: second coordinate of each object
• w2: width in second dimension for each object
predicate geost_smallest_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u)


A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global k dimensional bounding box. In addition, it enforces that the bounding box is the smallest one containing all objects, i.e., each of the 2k boundaries is touched by at least by one object.

More…

Parameters:

• k: the number of dimensions
• rect_size: the size of each box in k dimensions
• rect_offset: the offset of each box from the base position in k dimensions
• shape: the set of rectangles defining the i -th shape.
• x: the base position of each object. x [ i , j ] is the position of object i in dimension j .
• kind: the shape used by each object.
• l: is an array of lower bounds, l [ i ] is the minimum bounding box for all objects in dimension i .
• u: is an array of upper bounds, u [ i ] is the maximum bounding box for all objects in dimension i .
predicate knapsack(array [int] of int: w,
array [int] of int: p,
array [int] of var int: x,
var int: W,
var int: P)


Requires that items are packed in a knapsack with certain weight and profit restrictions.

Assumptions:

• Weights w and profits p must be non-negative
• w , p and x must have the same index sets

More…

Parameters:

• w: weight of each type of item
• p: profit of each type of item
• x: number of items of each type that are packed
• W: sum of sizes of all items in the knapsack
• P: sum of profits of all items in the knapsack

## 4.2.1.7. Scheduling constraints¶

predicate alternative(var opt int: s0,
var int: d0,
array [int] of var opt int: s,
array [int] of var int: d)


Alternative constraint for optional tasks. Task ( s0 , d0 ) spans the optional tasks ( s [ i ], d [ i ]) in the array arguments and at most one can occur

More…

predicate cumulative(array [int] of var int: s,
array [int] of var int: d,
array [int] of var int: r,
var int: b)


Requires that a set of tasks given by start times s , durations d , and resource requirements r , never require more than a global resource bound b at any one time.

Assumptions:

• forall i , d [ i ] >= 0 and r [ i ] >= 0

More…

predicate cumulative(array [int] of var opt int: s,
array [int] of var int: d,
array [int] of var int: r,
var int: b)


Requires that a set of tasks given by start times s , durations d , and resource requirements r , never require more than a global resource bound b at any one time. Start times are optional variables, so that absent tasks do not need to be scheduled.

Assumptions:

• forall i , d [ i ] >= 0 and r [ i ] >= 0

More…

predicate disjunctive(array [int] of var int: s,
array [int] of var int: d)


Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 can be scheduled at any time, even in the middle of other tasks.

Assumptions:

• forall i , d [ i ] >= 0

More…

predicate disjunctive(array [int] of var opt int: s,
array [int] of var int: d)


Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 can be scheduled at any time, even in the middle of other tasks. Start times are optional variables, so that absent tasks do not need to be scheduled.

Assumptions:

• forall i , d [ i ] >= 0

More…

predicate disjunctive_strict(array [int] of var int: s,
array [int] of var int: d)


Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time, but only when no other task is running.

Assumptions:

• forall i , d [ i ] >= 0

More…

predicate disjunctive_strict(array [int] of var opt int: s,
array [int] of var int: d)


Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time, but only when no other task is running. Start times are optional variables, so that absent tasks do not need to be scheduled.

Assumptions:

• forall i , d [ i ] >= 0

More…

predicate span(var opt int: s0,
var int: d0,
array [int] of var opt int: s,
array [int] of var int: d)


Span constraint for optional tasks. Task ( s0 , d0 ) spans the optional tasks ( s [ i ], d [ i ]) in the array arguments.

More…

## 4.2.1.8. Graph constraints¶

predicate bounded_dpath(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)


Constrains the subgraph ns and es of a given directed graph to be a path from s to t of weight K .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• w: the weight of each edge
• s: the source node (which may be variable)
• t: the dest node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
• K: the cost of the path
predicate bounded_dpath(array [int] of $$N: from, array [int] of$$N: to,
array [int] of int: w,
var $$N: s, var$$N: t,
array [$$N] of var bool: ns, array [int] of var bool: es, var int: K)  Constrains the subgraph ns and es of a given directed graph to be a path from s to t of weight K . More… Parameters: • from: the leaving node for each edge • to: the entering node for each edge • w: the weight of each edge • s: the source node (which may be variable) • t: the dest node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph • K: the cost of the path predicate bounded_path(int: N, int: E, array [int] of int: from, array [int] of int: to, array [int] of int: w, var int: s, var int: t, array [int] of var bool: ns, array [int] of var bool: es, var int: K)  Constrains the subgraph ns and es of a given undirected graph to be a path from s to t of weight K . More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • w: the weight of each edge • s: the source node (which may be variable) • t: the dest node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph • K: the cost of the path predicate bounded_path(array [int] of$$N: from,
array [int] of $$N: to, array [int] of int: w, var$$N: s,
var $$N: t, array [$$N] of var bool: ns,
array [int] of var bool: es,
var int: K)


Constrains the subgraph ns and es of a given undirected graph to be a path from s to t of weight K .

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• w: the weight of each edge
• s: the source node (which may be variable)
• t: the dest node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
• K: the cost of the path
predicate connected(array [int] of $$N: from, array [int] of$$N: to,
array [$$N] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given undirected graph to be connected. More… Parameters: • from: is the leaving node for each edge • to: is the entering node for each edge • ns: is a Boolean for each node whether it is in the subgraph • es: is a Boolean for each edge whether it is in the subgraph predicate d_weighted_spanning_tree(int: N, int: E, array [int] of int: from, array [int] of int: to, array [int] of int: w, var int: r, array [int] of var bool: es, var int: K)  Constrains the set of edges es of a given directed graph to be a weighted spanning tree rooted at r of weight W . More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • w: the weight of each edge • r: the root node (which may be variable) • es: a Boolean for each edge whether it is in the subgraph • K: the weight of the tree predicate dag(array [int] of$$N: from,
array [int] of $$N: to, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be a DAG.

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate dconnected(array [int] of $$N: from, array [int] of$$N: to,
array [$$N] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given directed graph to be connected. More… Parameters: • from: the leaving node for each edge • to: the entering node for each edge • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate dpath(int: N, int: E, array [int] of int: from, array [int] of int: to, var int: s, var int: t, array [int] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given directed graph to be a path from s to t . More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • s: the source node (which may be variable) • t: the dest node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate dpath(array [int] of$$N: from,
array [int] of $$N: to, var$$N: s,
var $$N: t, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be a path from s to t .

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• s: the source node (which may be variable)
• t: the dest node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate dreachable(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be reachable from r .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate dreachable(array [int] of $$N: from, array [int] of$$N: to,
var $$N: r, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be reachable from r .

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate dsteiner(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)


Constrains the subgraph ns and es of a given directed graph to be a weighted spanning tree rooted at r of weight W .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• w: the weight of each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
• K: the weight of the tree
predicate dtree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be a tree rooted at r .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate dtree(array [int] of $$N: from, array [int] of$$N: to,
var $$N: r, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given directed graph to be at tree rooted at r .

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate path(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given undirected graph to be a path from s to t .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• s: the source node (which may be variable)
• t: the dest node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate path(array [int] of $$N: from, array [int] of$$N: to,
var $$N: s, var$$N: t,
array [$$N] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given undirected graph to be a path from s to t . More… Parameters: • from: the leaving node for each edge • to: the entering node for each edge • s: the source node (which may be variable) • t: the dest node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate reachable(int: N, int: E, array [int] of int: from, array [int] of int: to, var int: r, array [int] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given undirected graph to be reachable from r . More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • r: the root node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate reachable(array [int] of$$N: from,
array [int] of $$N: to, var$$N: r,
array [$$N] of var bool: ns, array [int] of var bool: es)  Constrains the subgraph ns and es of a given undirected graph to be reachable from r . More… Parameters: • from: the leaving node for each edge • to: the entering node for each edge • r: the root node (which may be variable) • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate steiner(int: N, int: E, array [int] of int: from, array [int] of int: to, array [int] of int: w, array [int] of var bool: ns, array [int] of var bool: es, var int: K)  Constrains the set of edges es of a given undirected graph to be a weighted spanning tree of weight W . More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • w: the weight of each edge • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph • K: the weight of the tree predicate subgraph(int: N, int: E, array [int] of int: from, array [int] of int: to, array [int] of var bool: ns, array [int] of var bool: es)  Constrains that ns and es is a subgraph of a given directed graph. More… Parameters: • N: the number of nodes in the given graph • E: the number of edges in the given graph • from: the leaving node 1.. N for each edge • to: the entering node 1.. N for each edge • ns: a Boolean for each node whether it is in the subgraph • es: a Boolean for each edge whether it is in the subgraph predicate subgraph(array [int] of$$N: from,
array [int] of $$N: to, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains that ns and es is a subgraph of a given directed graph.

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given undirected graph to be a tree rooted at r .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate tree(array [int] of $$N: from, array [int] of$$N: to,
var $$N: r, array [$$N] of var bool: ns,
array [int] of var bool: es)


Constrains the subgraph ns and es of a given undirected graph to be at tree rooted at r .

More…

Parameters:

• from: the leaving node for each edge
• to: the entering node for each edge
• r: the root node (which may be variable)
• ns: a Boolean for each node whether it is in the subgraph
• es: a Boolean for each edge whether it is in the subgraph
predicate weighted_spanning_tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
array [int] of var bool: es,
var int: K)


Constrains the set of edges es of a given undirected graph to be a weighted spanning tree of weight W .

More…

Parameters:

• N: the number of nodes in the given graph
• E: the number of edges in the given graph
• from: the leaving node 1.. N for each edge
• to: the entering node 1.. N for each edge
• w: the weight of each edge
• es: a Boolean for each edge whether it is in the subgraph
• K: the weight of the tree

## 4.2.1.9. Extensional constraints (table, regular etc.)¶

predicate cost_mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: cost,
array [int] of int: to,
var int: totalcost)


Requires that x defines a path in the cost MDD with total edge weight totalcost .

More…

Parameters:

• N: the number of nodes, the root node is node 1
• level: the level of each node, the root is level 1, T is level length (x)+1
• E: the number of edges
• from: the leaving node (1.. N )for each edge
• label: the set of value of the x variable for each edge
• cost: the cost for each edge
• to: the entering node for each edge, where 0 = T node
• totalcost: the total cost of the path defined by x
predicate cost_regular(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of int: d,
int: q0,
set of int: F,
array [int,int] of int: c,
var int: C)


The sequence of values in array x (which must all be in the range 1.. S ) is accepted by the DFA of Q states with input 1.. S and transition function d (which maps (1.. Q , 1.. S ) -> 0.. Q )) and initial state q0 (which must be in 1.. Q ) and accepting states F (which all must be in 1.. Q ). We reserve state 0 to be an always failing state. Each edge has an associated cost c , and C is the sum of costs taken on the accepting path for x .

More…

predicate mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)


Requires that x defines a path from root to true node T through the (deterministic) MDD defined by

The MDD must be deterministic, i.e., there cannot be two edges with the same label leaving the same node.

More…

Parameters:

• N: the number of nodes, the root node is node 1
• level: the level of each node, the root is level 1, T is level length (x)+1
• E: the number of edges
• from: the leaving node (1.. N )for each edge
• label: the set of values of the x variable for each edge
• to: the entering node for each edge, where 0 = T node
predicate mdd_nondet(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)


Requires that x defines a path from root to true node T through the (nondeterministic) MDD defined by

The MDD can be nondeterministic, i.e., there can be two edges with the same label leaving the same node.

More…

Parameters:

• N: the number of nodes, the root node is node 1
• level: the level of each node, the root is level 1, T is level length (x)+1
• E: the number of edges
• from: the leaving node (1.. N )for each edge
• label: the set of values of the x variable for each edge
• to: the entering node for each edge, where 0 = T node
predicate regular(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of int: d,
int: q0,
set of int: F)


The sequence of values in array x (which must all be in the range 1.. S ) is accepted by the DFA of Q states with input 1.. S and transition function d (which maps (1.. Q , 1.. S ) -> 0.. Q )) and initial state q0 (which must be in 1.. Q ) and accepting states F (which all must be in 1.. Q ). We reserve state 0 to be an always failing state.

More…

predicate regular(array [int] of var int: x,
int: Q,
set of int: S,
array [int,int] of int: d,
int: q0,
set of int: F)


The sequence of values in array x (which must all be in the set S ) is accepted by the DFA of Q states with input S and transition function d (which maps (1.. Q , S ) -> 0.. Q )) and initial state q0 (which must be in 1.. Q ) and accepting states F (which all must be in 1.. Q ). We reserve state 0 to be an always failing state.

More…

predicate regular(array [int] of var int: x, string: r)


The sequence of values in array x is accepted by the regular expression r . This constraint generates it’s DFA equivalent.

Regular expressions can use the following syntax:

• Selection:
• Concatenation: “12 34”, 12 followed by 34. (Characters are assumed to be the part of the same number unless split by syntax or whitespace.)
• Union: “7|11”, a 7 or 11.
• Groups: “7(6|8)”, a 7 followed by a 6 or an 8.
• Wildcard: “.”, any value within the domain.
• Classes: “[3-6 7]”, a 3,4,5,6, or 7.
• Negated classes: “[^3 5]”, any value within the domain except for a 3 or a 5.
• Quantifiers:
• Asterisk: “12*”, 0 or more times a 12.
• Question mark: “5?”, 0 or 1 times a 5. (optional)
• Plus sign: “42+”, 1 or more time a 42.
• Exact: “1{3}”, exactly 3 times a 1.
• At least: “9{5,}”, 5 or more times a 9.
• Between: “7{3,5}”, at least 3 times, but at most 5 times a 7.

Members of enumerated types can be used in place of any integer (e.g., “A B”, A followed by B). Enumerated identifiers still use whitespace for concatenation.

predicate regular_nfa(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of set of int: d,
int: q0,
set of int: F)


The sequence of values in array x (which must all be in the range 1.. S ) is accepted by the NFA of Q states with input 1.. S and transition function d (which maps (1.. Q , 1.. S ) -> set of 1.. Q )) and initial state q0 (which must be in 1.. Q ) and accepting states F (which all must be in 1.. Q ).

More…

predicate regular_nfa(array [int] of var int: x,
int: Q,
set of int: S,
array [int,int] of set of int: d,
int: q0,
set of int: F)


The sequence of values in array x (which must all be in the range S ) is accepted by the NFA of Q states with input S and transition function d (which maps (1.. Q , S ) -> set of 1.. Q )) and initial state q0 (which must be in 1.. Q ) and accepting states F (which all must be in 1.. Q ).

More…

predicate table(array [int] of var bool: x, array [int,int] of bool: t)


Represents the constraint x in t where we consider each row in t to be a tuple and t as a set of tuples.

More…

predicate table(array [int] of var int: x, array [int,int] of int: t)


Represents the constraint x in t where we consider each row in t to be a tuple and t as a set of tuples.

More…

predicate table(array [int] of var opt int: x,
array [int,int] of opt int: t)


Represents the constraint x in t if the variable x_i and the value t_i occur where we consider each row in t to be a tuple and t as a set of tuples.

More…

## 4.2.1.10. Machine learning constraints¶

predicate neural_net(array [int] of var float: inputs,
array [int] of int: input_ids,
array [int] of var float: outputs,
array [int] of int: output_ids,
array [int] of float: bias,
array [int] of float: edge_weight,
array [int] of int: edge_parent,
array [int] of int: first_edge,
NEURON_TYPE: neuron_type)


constrain the output layer of a neural net to take the value defined by the input layer. the arguments are inputs : an array of float variables input_ids : array[int] of node outputs : an array of float variables output_ids : array[int] of node bias : array[node] of float edge_weight : array[edge] of float (dummy one at end!) edge_parent : array[edge] of neuron (start neuron for edge) first_edge : array[node] of 1..m+1 neuron_type : { NT_RELU, NT_STEP, NT_LINEAR, NT_SOFTPLUS }

More…

## 4.2.1.11. Deprecated constraints¶

predicate at_least(int: n, array [int] of var int: x, int: v)


Requires at least n variables in x to take the value v .

This constraint is deprecated. Use count(i in x)(i=v) >= n instead.

More…

predicate at_most(int: n, array [int] of var int: x, int: v)


Requires at most n variables in x to take the value v .

This constraint is deprecated. Use count(i in x)(i=v) <= n instead.

More…

predicate exactly(int: n, array [int] of var int: x, int: v)


Requires exactly n variables in x to take the value v .

This constraint is deprecated. Use count(i in x)(i=v) = n instead.

More…

## 4.2.1.12. Other declarations¶

function var $$E: arg_max(array [$$E] of var int: x)


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

More…

function var $$E: arg_max(array [$$E] of var bool: x)


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

More…

function var $$E: arg_max(array [$$E] of var float: x)


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

More…

function var $$E: arg_min(array [$$E] of var int: x)


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

More…

function var $$E: arg_min(array [$$E] of var bool: x)


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

More…

function var $$E: arg_min(array [$$E] of var float: x)


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

More…

predicate circuit(array [int] of var int: x)


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

More…

predicate disjoint(var set of int: s1, var set of int: s2)


Requires that sets s1 and s2 do not intersect.

More…

predicate maximum(var int: m, array [int] of var int: x)


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

Assumptions: | x | > 0.

More…

predicate maximum(var float: m, array [int] of var float: x)


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

Assumptions: | x | > 0.

More…

predicate maximum_arg(array [int] of var int: x, var int: i)


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

More…

predicate maximum_arg(array [int] of var bool: x, var int: i)


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

More…

predicate maximum_arg(array [int] of var float: x, var int: i)


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

More…

predicate member(array [int] of var bool: x, var bool: y)


Requires that y occurs in the array x .

More…

predicate member(array [int] of var float: x, var float: y)


Requires that y occurs in the array x .

More…

predicate member(array [int] of var int: x, var int: y)


Requires that y occurs in the array x .

More…

predicate member(array [int] of var set of int: x, var set of int: y)


Requires that y occurs in the array x .

More…

predicate member(var set of int: x, var int: y)


Requires that y occurs in the set x .

More…

predicate minimum(var float: m, array [int] of var float: x)


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

Assumptions: | x | > 0.

More…

predicate minimum(var int: m, array [int] of var int: x)


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

Assumptions: | x | > 0.

More…

predicate minimum_arg(array [int] of var int: x, var int: i)


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

More…

predicate minimum_arg(array [int] of var bool: x, var int: i)


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

More…

predicate minimum_arg(array [int] of var float: x, var int: i)


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

More…

predicate network_flow(array [int,1..2] of int: arc,
array [int] of int: balance,
array [int] of var int: flow)


Defines a network flow constraint.

More…

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)


Defines a network flow constraint with cost.

More…

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)


Constrains the sets in array S to partition the universe .

More…

function var float: piecewise_linear(var float: x,
array [int] of float: xi,
array [int] of float: vi)


Return a piecewise-linear interpolation of the given point sequence as a function of x

More…

predicate piecewise_linear(var float: x,
var float: y,
array [int] of float: xi,
array [int] of float: vi)


Constrains y ( x ) to be a piecewise-linear interpolation of the provided point sequence.

More…

predicate range(array [int] of var int: x,
var set of int: s,
var set of int: t)


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.

More…

function var set of int: range(array [int] of var int: x,
var set of int: s)


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.

More…

predicate roots(array [int] of var int: x,
var set of int: s,
var set of int: t)


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

More…

function var set of int: roots(array [int] of var int: x,
var set of int: t)


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

More…

predicate sliding_sum(int: low,
int: up,
int: seq,
array [int] of var int: vs)


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

More…

predicate subcircuit(array [int] of var int: x)


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.

More…

predicate sum_pred(var int: i,
array [int] of set of int: sets,
array [int] of int: cs,
var int: s)


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.

More…

predicate sum_set(array [int] of int: vs,
array [int] of int: ws,
var set of int: x,
var int: s)


Requires that the sum of the weights ws [ i1 ].. ws [ iN ] equals s , where vs [ i1 ].. vs [ iN ] are the elements appearing in set x

More…