# 4.2.6. Global constraints¶

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

## 4.2.6.2. Lexicographic constraints¶

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

Require adjacent rows and adjacent columns in the array `x` to be
lexicographically ordered. Adjacent rows and adjacent columns may be equal.

```
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.

```
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.

```
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.

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

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

```
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.

```
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.

```
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.

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

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

```
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.

```
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.

```
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.

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

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

```
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.

```
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.

```
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.

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

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

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

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

```
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`

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

Require adjacent rows and adjacent columns in the array `x` to be
lexicographically ordered. Adjacent rows and adjacent columns cannot be equal.

```
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` .

```
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` .

```
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` ].

```
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].

## 4.2.6.3. 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].

```
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].

```
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].

```
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]].

`x` [ `p` [ `i` ]] = `x` [ `p` [ `i` +1]] \(\rightarrow\) `p` [ `i` ] < `p` [ `i` +1].

```
predicate decreasing(array [int] of var bool: x)
```

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

```
predicate decreasing(array [int] of var float: x)
```

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

```
predicate decreasing(array [int] of var int: x)
```

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

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

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

```
predicate increasing(array [int] of var bool: x)
```

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

```
predicate increasing(array [int] of var float: x)
```

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

```
predicate increasing(array [int] of var int: x)
```

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

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

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

```
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.

```
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.

## 4.2.6.4. 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` ) ↔ ( `i` in `y` [ `j` ]).

```
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.

```
function array [int] of var int: inverse(array [int] of var int: f)
```

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

```
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.

```
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` ↔ `b` [ `i` ].

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

## 4.2.6.5. Counting constraints¶

```
predicate among(var int: n, array [int] of var int: x, set of int: v)
```

Requires exactly `n` variables in `x` to take one of the values in `v` .

```
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` .

```
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` .

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

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

```
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` .

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

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

```
predicate at_most1(array [int] of var set of int: s)
```

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

```
predicate count(array [int] of var int: x, var int: y, var int: c)
```

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

```
function var int: count(array [int] of var int: x, var int: y)
```

Returns the number of occurrences of `y` in `x` .

```
predicate count_eq(array [int] of var int: x, var int: y, var int: c)
```

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

```
function var int: count_eq(array [int] of var int: x, var int: y)
```

Returns the number of occurrences of `y` in `x` .

```
predicate count_geq(array [int] 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` .

```
predicate count_gt(array [int] 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` .

```
predicate count_leq(array [int] 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` .

```
predicate count_lt(array [int] 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` .

```
predicate count_neq(array [int] 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` .

```
predicate distribute(array [int] of var int: card,
array [int] of var int: value,
array [int] of var int: base)
```

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

```
function array [int] of var int: distribute(array [int] of var int: value,
array [int] of var int: base)
```

Returns an array of the number of occurences of `value` [ `i` ] in
`base` . The values in `value` need not be distinct.

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

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

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

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

```
predicate global_cardinality(array [int] of var int: x,
array [int] of int: cover,
array [int] of var int: counts)
```

Requires that the number of occurrences of `cover` [ `i` ] in `x` is `counts` [ `i` ].

```
function array [int] of var int: global_cardinality(array [int] of var int: x,
array [int] of int: cover)
```

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

```
predicate global_cardinality_closed(array [int] of var int: x,
array [int] of int: cover,
array [int] of var int: counts)
```

Requires that the number of occurences of `i` in `x` is `counts` [ `i` ].

The elements of `x` must take their values from `cover` .

```
function array [int] of var int: global_cardinality_closed(array [int] of var int: x,
array [int] of int: cover)
```

Returns an array with number of occurences of `i` in `x` .

The elements of `x` must take their values from `cover` .

```
predicate global_cardinality_low_up(array [int] of var int: x,
array [int] of int: cover,
array [int] of int: lbound,
array [int] 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` .

```
predicate global_cardinality_low_up_closed(array [int] of var int: x,
array [int] of int: cover,
array [int] of int: lbound,
array [int] 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` .

## 4.2.6.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

```
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

```
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

```
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

```
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.

```
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.

```
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.

```
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.

```
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.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`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.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`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.

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.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`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

- Weights

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.6.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

```
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

```
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

```
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

```
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

```
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

```
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

```
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.

## 4.2.6.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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`w` is the weight of each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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
`K` is 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`w` is the weight of each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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
`K` is 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`w` is the weight of each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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
`K` is 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`w` is the weight of each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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
`K` is 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.

`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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`w` is the weight of each edge
`r` is the root node (which may be variable)
`es` is a Boolean for each edge whether it is in the subgraph
`K` is 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.

`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 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.

`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`r` is the root node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`r` is the root node (which may be variable)
`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`w` is the weight of each edge
`r` is the root node (which may be variable)
`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
`K` is 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`r` is the root node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`r` is the root node (which may be variable)
`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`s` is the source node (which may be variable)
`t` is the dest node (which may be variable)
`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`r` is the root node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`r` is the root node (which may be variable)
`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`w` is the weight of 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
`K` is 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.

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` 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 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.

`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 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` .

`N` is the number of nodes in the given graph
`E` is the number of edges in the given graph
`from` is the leaving node 1.. `N` for each edge
`to` is the entering node 1.. `N` for each edge
`r` is the root node (which may be variable)
`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 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` .

`from` is the leaving node for each edge
`to` is the entering node for each edge
`r` is the root node (which may be variable)
`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 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` .

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

## 4.2.6.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` .

`N` is the number of nodes, the root node is node 1
`level` is the level of each node, the root is level 1, T is level `length` (x)+1
`E` is the number of edges
`from` is the leaving node (1.. `N` )for each edge
`label` is the set of value of the x variable for each edge
`cost` is the cost for each edge
`to` is the entering node for each edge, where 0 = T node
`totalcost` is 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` .

```
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 MDD defined by

`N` is the number of nodes, the root node is node 1
`level` is the level of each node, the root is level 1, T is level `length` (x)+1
`E` is the number of edges
`from` is the leaving node (1.. `N` )for each edge
`label` is the set of values of the `x` variable for each edge
`to` is 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.

```
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.

```
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` ).

```
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` ).

```
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.

```
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.

```
set of int: 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: { RELU, STEP, LINEAR, SOFTPLUS }

## 4.2.6.10. 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.

```
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.

```
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.

```
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.

```
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.

```
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.

```
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` .

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

Requires that sets `s1` and `s2` do not intersect.

```
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.

```
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.

```
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

```
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

```
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

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

Requires that `y` occurs in the array `x` .

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

Requires that `y` occurs in the array `x` .

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

Requires that `y` occurs in the array `x` .

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

Requires that `y` occurs in the array `x` .

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

Requires that `y` occurs in the set `x` .

```
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.

```
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.

```
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

```
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

```
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

```
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.

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.

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` .

```
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`

```
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.

```
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.

```
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.

```
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`

```
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`

```
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` ].

```
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.

```
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.

```
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`