Ordering & counting constraints

The global constraints that say something about an array as a whole: that its values are distinct, how often a value occurs, how two arrays compare, or how two arrays encode the same information.

These are where a solver’s dedicated propagators earn their keep. Declaring one commits you to the meaning below; a solver that would rather have the constraint decomposed simply does not declare it, and the application decomposes instead.

Notation

The definitions below are formulas rather than sentences, and use these throughout.

$\operatorname{col}_j(\mathit{xs})$	$= \left( \mathit{xs}_{j},\; \mathit{xs}_{j + \mathit{columns}},\; \mathit{xs}_{j + 2\,\mathit{columns}},\; \ldots \right)$	column j of a matrix passed flat, row-major, with the given number of entries per row
$u \preceq v$		lexicographic order on tuples: either they are equal, or at the first position where they differ the left one is smaller
$u \prec v$		its strict form

55 constraints

bool_count

bool_count(list of var bool: xs, var bool: value, var int: n)

The value occurs exactly the given number of times in the array.

$$n = \lvert \{\, i \mid \mathit{xs}_i \leftrightarrow \mathit{value} \,\} \rvert$$

bool_increasing

bool_increasing(list of var bool: xs)

also declarable as bool_increasing_reif and bool_increasing_imp

The array is in non-decreasing order, taking false below true.

$$\forall i < j : \mathit{xs}_i \rightarrow \mathit{xs}_j$$

bool_lex_chain_less

bool_lex_chain_less(list of var bool: xs, int: columns)

also declarable as bool_lex_chain_less_reif and bool_lex_chain_less_imp

The columns of a Boolean matrix are in strictly increasing lexicographic order.

$$\forall j : \operatorname{col}_j(\mathit{xs}) \prec \operatorname{col}_{j+1}(\mathit{xs})$$

bool_lex_chain_lesseq

bool_lex_chain_lesseq(list of var bool: xs, int: columns)

also declarable as bool_lex_chain_lesseq_reif and bool_lex_chain_lesseq_imp

The columns of a Boolean matrix are in non-decreasing lexicographic order.

$$\forall j : \operatorname{col}_j(\mathit{xs}) \preceq \operatorname{col}_{j+1}(\mathit{xs})$$

bool_lex_chain_lesseq_orbitope_packing

bool_lex_chain_lesseq_orbitope_packing(list of var bool: xs, int: columns)

also declarable as bool_lex_chain_lesseq_orbitope_packing_reif and bool_lex_chain_lesseq_orbitope_packing_imp

The columns of a Boolean matrix are in non-decreasing lexicographic order, and at most one entry in each row holds.

$$\left( \forall j : \operatorname{col}_j(\mathit{xs}) \preceq \operatorname{col}_{j+1}(\mathit{xs}) \right) \wedge \forall i : \lvert \{\, j \mid \mathit{xs}_{(i-1)\mathit{columns}+j} \,\} \rvert \leq 1$$

The set-packing form. With no row constraint at all it would be bool_lex_chain_lesseq.

bool_lex_chain_lesseq_orbitope_partition

bool_lex_chain_lesseq_orbitope_partition(list of var bool: xs, int: columns)

also declarable as bool_lex_chain_lesseq_orbitope_partition_reif and bool_lex_chain_lesseq_orbitope_partition_imp

The columns of a Boolean matrix are in non-decreasing lexicographic order, and exactly one entry in each row holds.

$$\left( \forall j : \operatorname{col}_j(\mathit{xs}) \preceq \operatorname{col}_{j+1}(\mathit{xs}) \right) \wedge \forall i : \lvert \{\, j \mid \mathit{xs}_{(i-1)\mathit{columns}+j} \,\} \rvert = 1$$

xs is the matrix flattened row-major, columns entries per row. Breaks the symmetry of a set-partitioning model with interchangeable columns; an orbitope propagator reasons about the rows and the column ordering together, which is why this is one constraint and not two.

bool_lex_less

bool_lex_less(list of var bool: xs, list of var bool: ys)

also declarable as bool_lex_less_reif and bool_lex_less_imp

The first array is strictly before the second in lexicographic order.

$$\exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \neg \mathit{xs}_k \wedge \mathit{ys}_k$$

bool_lex_lesseq

bool_lex_lesseq(list of var bool: xs, list of var bool: ys)

also declarable as bool_lex_lesseq_reif and bool_lex_lesseq_imp

The first array is before or equal to the second in lexicographic order.

$$\mathit{xs} = \mathit{ys} \;\vee\; \exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \neg \mathit{xs}_k \wedge \mathit{ys}_k$$

bool_sliding_among

bool_sliding_among(list of var bool: xs, var bool: value, int: window, int: lower_bound, int: upper_bound)

also declarable as bool_sliding_among_reif and bool_sliding_among_imp

Every window of consecutive elements takes the given value between the given number of times.

$$\forall k : \mathit{lower\_bound} \leq \lvert \{\, i \in [k, k + \mathit{window}) \mid \mathit{xs}_i \leftrightarrow \mathit{value} \,\} \rvert \leq \mathit{upper\_bound}$$

float_count

float_count(list of var float: xs, var float: value, var int: n)

The value occurs exactly the given number of times in the array.

$$n = \lvert \{\, i \mid \mathit{xs}_i = \mathit{value} \,\} \rvert$$

float_increasing

float_increasing(list of var float: xs)

also declarable as float_increasing_reif and float_increasing_imp

The array is in non-decreasing order.

$$\forall i < j : \mathit{xs}_i \leq \mathit{xs}_j$$

float_lex_less

float_lex_less(list of var float: xs, list of var float: ys)

also declarable as float_lex_less_reif and float_lex_less_imp

The first array is strictly before the second in lexicographic order.

$$\exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k < \mathit{ys}_k$$

float_lex_lesseq

float_lex_lesseq(list of var float: xs, list of var float: ys)

also declarable as float_lex_lesseq_reif and float_lex_lesseq_imp

The first array is before or equal to the second in lexicographic order.

$$\mathit{xs} = \mathit{ys} \;\vee\; \exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k < \mathit{ys}_k$$

float_strictly_increasing

float_strictly_increasing(list of var float: xs)

also declarable as float_strictly_increasing_reif and float_strictly_increasing_imp

The array is in strictly increasing order, so no value repeats.

$$\forall i < j : \mathit{xs}_i < \mathit{xs}_j$$

int_all_different

int_all_different(list of var int: xs)

also declarable as int_all_different_reif and int_all_different_imp

No value occurs twice in the array.

$$\forall i < j : \mathit{xs}_i \neq \mathit{xs}_j$$

int_all_different_except

int_all_different_except(list of var int: xs, set of int: except)

also declarable as int_all_different_except_reif and int_all_different_except_imp

No value occurs twice, except for values in the given set, which may repeat freely.

$$\forall i < j : \mathit{xs}_i \neq \mathit{xs}_j \;\vee\; \mathit{xs}_i \in \mathit{except}$$

The common case of a value marking an unused slot is this constraint with except = {0}.

int_all_different_symmetric

int_all_different_symmetric(list of var int: xs, int: offset)

also declarable as int_all_different_symmetric_reif and int_all_different_symmetric_imp

The array is a permutation that is its own inverse.

$$\forall i : \sigma(\sigma(i)) = i \quad \text{where } \sigma(i) = \mathit{xs}_{i - \mathit{offset} + 1}$$

int_all_equal

int_all_equal(list of var int: xs)

also declarable as int_all_equal_reif and int_all_equal_imp

Every element of the array takes the same value.

$$\forall i, j : \mathit{xs}_i = \mathit{xs}_j$$

int_among

int_among(list of var int: xs, set of int: values, var int: n)

The count is how many array elements take a value from the given set.

$$n = \lvert \{\, i \mid \mathit{xs}_i \in \mathit{values} \,\} \rvert$$

Counting a single value is int_count; this counts membership of a set.

int_count

int_count(list of var int: xs, var int: value, var int: n)

The value occurs exactly the given number of times in the array.

$$n = \lvert \{\, i \mid \mathit{xs}_i = \mathit{value} \,\} \rvert$$

The count is a value, not a comparison: at most k occurrences is this constraint alongside int_lin_le([1], [n], k).

int_distribute

int_distribute(list of var int: xs, list of var int: cover, list of var int: count)

Each count says how often its matching value occurs in the array, with the values themselves variable.

$$\forall j : \mathit{count}_j = \lvert \{\, i \mid \mathit{xs}_i = \mathit{cover}_j \,\} \rvert$$

Unlike int_global_cardinality, the values being counted are decision variables rather than constants.

int_global_cardinality

int_global_cardinality(list of var int: xs, list of int: cover, list of var int: count)

Each covered value occurs as many times in the array as its matching count says.

$$\forall j : \mathit{count}_j = \lvert \{\, i \mid \mathit{xs}_i = \mathit{cover}_j \,\} \rvert$$

Values outside cover are unconstrained. cover and count must have equal length.

int_global_cardinality_closed

int_global_cardinality_closed(list of var int: xs, list of int: cover, list of var int: count)

also declarable as int_global_cardinality_closed_reif and int_global_cardinality_closed_imp

As int_global_cardinality, and additionally every array element must take a covered value.

$$\forall i : \mathit{xs}_i \in \mathit{cover} \;\wedge\; \forall j : \mathit{count}_j = \lvert \{\, i \mid \mathit{xs}_i = \mathit{cover}_j \,\} \rvert$$

int_global_cardinality_low_up

int_global_cardinality_low_up(list of var int: xs, list of int: cover, list of int: lower_bound, list of int: upper_bound)

also declarable as int_global_cardinality_low_up_reif and int_global_cardinality_low_up_imp

Each covered value occurs a number of times between its lower and upper bound.

$$\forall j : \mathit{lower\_bound}_j \leq \lvert \{\, i \mid \mathit{xs}_i = \mathit{cover}_j \,\} \rvert \leq \mathit{upper\_bound}_j$$

Kept alongside int_global_cardinality, which would need count variables introduced to say the same thing.

int_global_cardinality_low_up_closed

int_global_cardinality_low_up_closed(list of var int: xs, list of int: cover, list of int: lower_bound, list of int: upper_bound)

also declarable as int_global_cardinality_low_up_closed_reif and int_global_cardinality_low_up_closed_imp

As int_global_cardinality_low_up, and additionally every array element must take a covered value.

$$\forall i : \mathit{xs}_i \in \mathit{cover} \;\wedge\; \forall j : \mathit{lower\_bound}_j \leq \lvert \{\, i \mid \mathit{xs}_i = \mathit{cover}_j \,\} \rvert \leq \mathit{upper\_bound}_j$$

int_increasing

int_increasing(list of var int: xs)

also declarable as int_increasing_reif and int_increasing_imp

The array is in non-decreasing order.

$$\forall i < j : \mathit{xs}_i \leq \mathit{xs}_j$$

Non-increasing order is this constraint over the reversed array.

int_inverse

int_inverse(list of var int: f, int: f_offset, list of var int: invf, int: invf_offset)

also declarable as int_inverse_reif and int_inverse_imp

The two arrays are mutually inverse permutations.

$$\forall i, j : f_{i - \mathit{f\_offset} + 1} = j \leftrightarrow \mathit{invf}_{j - \mathit{invf\_offset} + 1} = i$$

Each array is read in the caller’s numbering: f from f_offset, invf from invf_offset. The standard channelling between a permutation and its inverse.

int_inverse_in_range

int_inverse_in_range(list of var int: f, int: f_offset, list of var int: invf, int: invf_offset)

also declarable as int_inverse_in_range_reif and int_inverse_in_range_imp

Each array inverts the other wherever the index is in range, leaving the rest free.

$$\forall i, j : f_{i - \mathit{f\_offset} + 1} = j \rightarrow \mathit{invf}_{j - \mathit{invf\_offset} + 1} = i$$

The one-sided form, for when the arrays have different index ranges.

int_lex_chain_less

int_lex_chain_less(list of var int: xs, int: columns)

also declarable as int_lex_chain_less_reif and int_lex_chain_less_imp

The columns of a matrix are in strictly increasing lexicographic order.

$$\forall j : \operatorname{col}_j(\mathit{xs}) \prec \operatorname{col}_{j+1}(\mathit{xs})$$

int_lex_chain_lesseq

int_lex_chain_lesseq(list of var int: xs, int: columns)

also declarable as int_lex_chain_lesseq_reif and int_lex_chain_lesseq_imp

The columns of a matrix are in non-decreasing lexicographic order.

$$\forall j : \operatorname{col}_j(\mathit{xs}) \preceq \operatorname{col}_{j+1}(\mathit{xs})$$

xs is the matrix flattened row-major, columns entries per row. Constraining rows as well as columns is this constraint applied to the matrix and to its transpose.

int_lex_less

int_lex_less(list of var int: xs, list of var int: ys)

also declarable as int_lex_less_reif and int_lex_less_imp

The first array is strictly before the second in lexicographic order.

$$\exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k < \mathit{ys}_k$$

int_lex_lesseq

int_lex_lesseq(list of var int: xs, list of var int: ys)

also declarable as int_lex_lesseq_reif and int_lex_lesseq_imp

The first array is before or equal to the second in lexicographic order.

$$\mathit{xs} = \mathit{ys} \;\vee\; \exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k < \mathit{ys}_k$$

The arrays need not have equal length; a proper prefix is lexicographically smaller.

int_nvalue

int_nvalue(list of var int: xs, var int: n)

The count is how many distinct values the array takes.

$$n = \lvert \{\, \mathit{xs}_i \mid i \,\} \rvert$$

n = 1 is int_all_equal; n = length(xs) is int_all_different.

int_seq_precede_chain

int_seq_precede_chain(list of var int: xs)

also declarable as int_seq_precede_chain_reif and int_seq_precede_chain_imp

A value may only be used once every smaller non-negative value has already been used.

$$\forall j : \mathit{xs}_j > 0 \rightarrow \exists i < j : \mathit{xs}_i = \mathit{xs}_j - 1$$

The canonical symmetry break for problems where values name interchangeable groups.

int_sliding_among

int_sliding_among(list of var int: xs, set of int: values, int: window, int: lower_bound, int: upper_bound)

also declarable as int_sliding_among_reif and int_sliding_among_imp

Every window of consecutive elements contains between the given bounds of the chosen values.

$$\forall k : \mathit{lower\_bound} \leq \lvert \{\, i \in [k, k + \mathit{window}) \mid \mathit{xs}_i \in \mathit{values} \,\} \rvert \leq \mathit{upper\_bound}$$

int_sliding_sum

int_sliding_sum(list of var int: xs, int: window, int: lower_bound, int: upper_bound)

also declarable as int_sliding_sum_reif and int_sliding_sum_imp

Every window of consecutive elements sums to a value between the given bounds.

$$\forall k : \mathit{lower\_bound} \leq \sum_{i \in [k,\, k + \mathit{window})} \mathit{xs}_i \leq \mathit{upper\_bound}$$

int_strictly_increasing

int_strictly_increasing(list of var int: xs)

also declarable as int_strictly_increasing_reif and int_strictly_increasing_imp

The array is in strictly increasing order, so no value repeats.

$$\forall i < j : \mathit{xs}_i < \mathit{xs}_j$$

int_value_precede

int_value_precede(int: s, int: t, list of var int: xs)

also declarable as int_value_precede_reif and int_value_precede_imp

If the second value occurs at all, the first occurs somewhere before it.

$$\forall j : \mathit{xs}_j = t \rightarrow \exists i < j : \mathit{xs}_i = s$$

Breaks the symmetry between interchangeable values, for example colours in a graph colouring. A chain of precedences is this constraint applied to each consecutive pair.

int_var_perm_sym

int_var_perm_sym(list of var int: xs, list of int: permutations)

also declarable as int_var_perm_sym_reif and int_var_perm_sym_imp

The array is lexicographically no greater than any of its listed permutations.

$$\forall p : \mathit{xs} \preceq \left( \mathit{xs}_{\mathit{permutations}_{p,1}}, \mathit{xs}_{\mathit{permutations}_{p,2}}, \ldots \right)$$

permutations is flattened row-major, one permutation per row; no row length travels with it because the rows are as long as xs. A general symmetry break for a known symmetry group.

int_var_sqr_sym

int_var_sqr_sym(list of var int: xs, int: columns)

also declarable as int_var_sqr_sym_reif and int_var_sqr_sym_imp

A square matrix is lexicographically no greater than its transpose, or any row and column permutation of itself.

$$\left( \mathit{xs}_{(i-1)c+j} \right)_{i,j} \preceq \left( \mathit{xs}_{(j-1)c+i} \right)_{i,j} \quad \text{where } c = \mathit{columns}$$

set_of_int_all_different

set_of_int_all_different(list of var set of int: xs)

also declarable as set_of_int_all_different_reif and set_of_int_all_different_imp

No two elements of the array are the same set.

$$\forall i < j : \mathit{xs}_i \neq \mathit{xs}_j$$

set_of_int_all_disjoint

set_of_int_all_disjoint(list of var set of int: xs)

also declarable as set_of_int_all_disjoint_reif and set_of_int_all_disjoint_imp

No two sets in the array share a member.

$$\forall i < j : \mathit{xs}_i \cap \mathit{xs}_j = \emptyset$$

set_of_int_all_equal

set_of_int_all_equal(list of var set of int: xs)

also declarable as set_of_int_all_equal_reif and set_of_int_all_equal_imp

Every element of the array is the same set.

$$\forall i, j : \mathit{xs}_i = \mathit{xs}_j$$

set_of_int_count

set_of_int_count(list of var set of int: xs, var set of int: value, var int: n)

The value occurs exactly the given number of times in the array.

$$n = \lvert \{\, i \mid \mathit{xs}_i = \mathit{value} \,\} \rvert$$

set_of_int_global_cardinality

set_of_int_global_cardinality(list of var set of int: xs, list of int: cover, list of var int: count)

Each covered value is a member of as many sets in the array as its matching count says.

$$\forall j : \mathit{count}_j = \lvert \{\, i \mid \mathit{cover}_j \in \mathit{xs}_i \,\} \rvert$$

Counts membership where int_global_cardinality counts equality, so the two are different constraints. Values outside cover are unconstrained.

set_of_int_global_cardinality_closed

set_of_int_global_cardinality_closed(list of var set of int: xs, list of int: cover, list of var int: count)

also declarable as set_of_int_global_cardinality_closed_reif and set_of_int_global_cardinality_closed_imp

As set_of_int_global_cardinality, and additionally no set may hold a value outside the cover.

$$\left( \forall i : \mathit{xs}_i \subseteq \mathit{cover} \right) \wedge \forall j : \mathit{count}_j = \lvert \{\, i \mid \mathit{cover}_j \in \mathit{xs}_i \,\} \rvert$$

set_of_int_global_cardinality_low_up

set_of_int_global_cardinality_low_up(list of var set of int: xs, list of int: cover, list of int: lower_bound, list of int: upper_bound)

also declarable as set_of_int_global_cardinality_low_up_reif and set_of_int_global_cardinality_low_up_imp

Each covered value is a member of a number of sets between its lower and upper bound.

$$\forall j : \mathit{lower\_bound}_j \leq \lvert \{\, i \mid \mathit{cover}_j \in \mathit{xs}_i \,\} \rvert \leq \mathit{upper\_bound}_j$$

set_of_int_global_cardinality_low_up_closed

set_of_int_global_cardinality_low_up_closed(list of var set of int: xs, list of int: cover, list of int: lower_bound, list of int: upper_bound)

also declarable as set_of_int_global_cardinality_low_up_closed_reif and set_of_int_global_cardinality_low_up_closed_imp

As set_of_int_global_cardinality_low_up, and additionally no set may hold a value outside the cover.

$$\left( \forall i : \mathit{xs}_i \subseteq \mathit{cover} \right) \wedge \forall j : \mathit{lower\_bound}_j \leq \lvert \{\, i \mid \mathit{cover}_j \in \mathit{xs}_i \,\} \rvert \leq \mathit{upper\_bound}_j$$

set_of_int_increasing

set_of_int_increasing(list of var set of int: xs)

also declarable as set_of_int_increasing_reif and set_of_int_increasing_imp

The array is in non-decreasing order under the standard total order on sets.

$$\forall i < j : \mathit{xs}_i \preceq \mathit{xs}_j$$

set_of_int_inverse

set_of_int_inverse(list of var set of int: f, int: f_offset, list of var set of int: invf, int: invf_offset)

also declarable as set_of_int_inverse_reif and set_of_int_inverse_imp

The two arrays of sets describe the same relation, read in opposite directions.

$$\forall i, j : j \in f_{i - \mathit{f\_offset} + 1} \leftrightarrow i \in \mathit{invf}_{j - \mathit{invf\_offset} + 1}$$

set_of_int_lex_less

set_of_int_lex_less(list of var set of int: xs, list of var set of int: ys)

also declarable as set_of_int_lex_less_reif and set_of_int_lex_less_imp

The first array is strictly before the second in lexicographic order.

$$\exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k \prec \mathit{ys}_k$$

set_of_int_lex_lesseq

set_of_int_lex_lesseq(list of var set of int: xs, list of var set of int: ys)

also declarable as set_of_int_lex_lesseq_reif and set_of_int_lex_lesseq_imp

The first array is before or equal to the second in lexicographic order.

$$\mathit{xs} = \mathit{ys} \;\vee\; \exists k : \left( \forall i < k : \mathit{xs}_i = \mathit{ys}_i \right) \wedge \mathit{xs}_k \prec \mathit{ys}_k$$

set_of_int_seq_precede_chain

set_of_int_seq_precede_chain(list of var set of int: xs)

also declarable as set_of_int_seq_precede_chain_reif and set_of_int_seq_precede_chain_imp

A value may only appear in a set once every smaller non-negative value has appeared in an earlier one.

$$\forall j, v > 0 : v \in \mathit{xs}_j \rightarrow \exists i < j : v - 1 \in \mathit{xs}_i$$

set_of_int_strictly_increasing

set_of_int_strictly_increasing(list of var set of int: xs)

also declarable as set_of_int_strictly_increasing_reif and set_of_int_strictly_increasing_imp

The array is strictly increasing under the standard total order on sets.

$$\forall i < j : \mathit{xs}_i \prec \mathit{xs}_j$$

set_of_int_value_precede

set_of_int_value_precede(int: s, int: t, list of var set of int: xs)

also declarable as set_of_int_value_precede_reif and set_of_int_value_precede_imp

If the second value occurs in any set, the first occurs in an earlier one.

$$\forall j : t \in \mathit{xs}_j \rightarrow \exists i < j : s \in \mathit{xs}_i$$