Sets

Generic CP sets

Domain of variables

ConstraintProgrammingExtensions.DomainType
Domain{T <: Number}(values::Set{T})

The set corresponding to an enumeration of constant values.

The value of a scalar function is enforced to take a value from this set of values.

This constraint is sometimes called in, member or allowed_assignments. https://sofdem.github.io/gccat/gccat/Cdomain.html

Example

x in Domain(1:3)
# enforces `x == 1` OR `x == 2` OR `x == 3`.
source
ConstraintProgrammingExtensions.VectorDomainType
VectorDomain{T <: Number}(dimension::Int, values::Set{Vector{T}})

The set corresponding to an enumeration of constant values.

The value of a vector function is enforced to take a value from this set of vector values.

This constraint is sometimes called in, member or allowed_assignments. https://sofdem.github.io/gccat/gccat/Cdomain.html

Example

[x, y] in Domain(2, Set([[1, 2], [2, 3]]))
# enforces (`x == 1` AND `y == 2`) OR (`x == 2` AND `y == 3`).
source
ConstraintProgrammingExtensions.AntiDomainType
AntiDomain{T <: Number}(values::Set{T})

The set corresponding to an enumeration of constant values that are excluded.

The value of a scalar function is enforced to take a value that is not from this set of values.

This constraint is sometimes called (not_in)[https://sofdem.github.io/gccat/gccat/Cnotin.html], `notmember,rel,forbiddenassignments, ornogood`.

Example

x in AntiDomain(1:3)
# enforces `x != 1` AND `x != 2` AND `x != 3`.
source
ConstraintProgrammingExtensions.VectorAntiDomainType
VectorAntiDomain{T <: Number}(values::Set{T})

The set corresponding to an enumeration of constant values that are excluded.

The value of a vector function is enforced to take a value that is not from this set of vector values.

This constraint is sometimes called (not_in)[https://sofdem.github.io/gccat/gccat/Cnotin.html], `notmember,rel,forbiddenassignments, ornogood`.

Example

[x, y] in VectorAntiDomain(2, Set([[1, 2], [2, 3]]))
# enforces (`x != 1` AND `y != 2`) OR (`x != 2` AND `y != 3`).
source
ConstraintProgrammingExtensions.MembershipType
Membership(dimension)

The first element of a function of dimension dimension must equal at least one of the following dimension - 1 elements of the function.

This constraint is sometimes called in_set.

Example

[x, y, z] in Membership(3)
# enforces `x == y` OR `x == z`.
source

Array indexing

ConstraintProgrammingExtensions.ElementType
Element{T <: Real}(values::Vector{T})

$\{(x, i) \in \mathbb{R} \times \mathbb{N} | x = values[i]\}$

Less formally, the first element constrained in this set will take the value of values at the index given by the second element.

Also called indexing or nth.

Examples

[x, 3] in Element([4, 5, 6])
# Enforces that x = 6, because 6 is the 3rd element from the array.

[y, j] in Element([4, 5, 6])
# Enforces that y = array[j], depending on the value of j (an integer
# between 1 and 3).
source
ConstraintProgrammingExtensions.ElementVariableArrayType
ElementVariableArray(dimension::Int)

$\{(x, i, values) \in \mathbb{R} \times \mathbb{N} \times \mathbb{R}^{\mathtt{dimension}} | x = values[i]\}$

Less formally, the first element constrained in this set will take the value of values at the index given by the second element in the array given by the remaining elements constrained in the set.

Examples

[x, 3, a, b, c] in ElementVariableArray(3)
# Enforces that x = c, because 6 is the 3rd element from the array [a, b, c].

[y, j, a, b, c] in ElementVariableArray(3)
# Enforces that y = array[j], depending on the value of j (an integer
# between 1 and 3), from the array [a, b, c].
source

Others

ConstraintProgrammingExtensions.AllEqualType

AllEqual(dimension::Int)

The set corresponding to an all-equal constraint.

All expressions of a vector-valued function are enforced to take the same value in the solution.

Example

[x, y, z] in AllEqual(3)
# enforces `x == y` AND `x == z`.
source
ConstraintProgrammingExtensions.AllDifferentType
AllDifferent(dimension::Int)

The set corresponding to an all-different constraint.

All expressions of a vector-valued function are enforced to take distinct values in the solution: for all pairs of expressions, their values must differ.

This constraint is sometimes called distinct.

Example

[x, y, z] in AllDifferent(3)
# enforces `x != y` AND `x != z` AND `y != z`.
source
ConstraintProgrammingExtensions.AllDifferentExceptConstantsType
AllDifferentExceptConstants{T <: Number}(dimension::Int, k::Set{T})

All expressions of a vector-valued function are enforced to take distinct values in the solution, but values equal to any value in k are not considered: for all pairs of expressions, either their values must differ or at least one of the two variables has a value in k.

This constraint is sometimes called distinct.

Example

[x, y] in AllDifferentExceptConstant(2, 0)
# enforces `x != y` OR `x == 0` OR `y == 0`.

[x, y] in AllDifferentExceptConstant(2, Set([0, 1]))
# enforces `x != y` OR `x == 0` OR `y == 0` OR `x == 1` OR `y == 1`.
source
ConstraintProgrammingExtensions.SymmetricAllDifferentType
SymmetricAllDifferent(dimension::Int)

The set corresponding to an all-different constraint, with the additional requirement that the array must be symmetric.

All expressions of a vector-valued function are enforced to take distinct values in the solution: for all pairs of expressions, their values must differ. Symmetry means that, if $x[i]=j$, then $x[j]=i$.

This constraint is sometimes called symmetric_alldifferent.

Example

[x, y, z] in SymmetricAllDifferent(3)
# enforces `x != y` AND `x != z` AND `y != z` AND `(x == 2 => y == 1)` AND 
# `(x == 3 => z = 1)` AND `(y == 1 => x == 2)` AND `(y == 3 => z == 2)` AND 
# `(z == 1 => x == 3)` AND `(z == 2 => y == 3)`.
source
ConstraintProgrammingExtensions.MinimumDistanceType
MinimumDistance{T <: Real}(dimension::Int, k::T)

Ensures that all the dimension expressions in this set are at least k apart, in absolute value:

$\Big\{x \in \mathbb{S}^{\mathtt{dimension}} \Big| |x_i - x_j| \geq k, \forall i \neq j \in \{1, 2\dots \mathtt{dimension}\} \Big\}$

Also called all_min_dist or inter_distance.

source
ConstraintProgrammingExtensions.MaximumDistanceType
MaximumDistance{T <: Real}(dimension::Int, k::T)

Ensures that all the dimension expressions in this set are at most k apart, in absolute value:

$\Big\{x \in \mathbb{S}^{\mathtt{dimension}} \Big| |x_i - x_j| \leq k, \forall i \neq j \in \{1, 2\dots \mathtt{dimension}\} \Big\}$

source
ConstraintProgrammingExtensions.InverseType
Inverse(dimension::Int)

Ensures that the two arrays of variables of size dimension are the inverse one of the other.

$\Big\{(x, y) \in \mathbb{R}^{\mathtt{dimension}} \times \mathbb{R}^{dimension} \Big| x_i = j \iff y_j = i, \forall i, j \in \{1, 2 \dots \mathtt{dimension}\} \Big\}$

Indices start at 1, like Julia.

Also called channel, inverse_channeling, or assignment.

source
ConstraintProgrammingExtensions.SlidingSumType
SlidingSum{T}(low::T, high::T, length::Int, dimension::Int)

Ensures that the sum of all sequences of size length have a value between low and high.

$\{x \in \mathbb{R}^{\mathtt{dimension}} | \mathtt{low} \leq \sum_{j=i}^{i+\mathtt{length}-1} x_i \leq \mathtt{high}, \forall i \in \{ 0, 1 \dots \mathtt{dimension} - \mathtt{length} \} \}$

https://sofdem.github.io/gccat/gccat/Csliding_sum.html

source
ConstraintProgrammingExtensions.ValuePrecedenceType
ValuePrecedence(before::T, value::T, dimension::Int)

Ensures that the value before happens before value in the array of size dimension.

$\{x \in \mathbb{R}^{\mathtt{dimension}} | \exists i < j: x_i = \mathtt{before}, x_j = \mathtt{value} \}$

Also called precede or value_precede.

https://sofdem.github.io/gccat/gccat/Cintvalueprecede.html

source

Combinatorial constraints

ConstraintProgrammingExtensions.ContiguityType
Contiguity(dimension::Int)

Ensures that, in the binary variables x constrained to be in this set, all the 1s are contiguous. The vector must correspond to the regular expression 0*1*0*.

source

Bin packing

ConstraintProgrammingExtensions.BinPackingType
BinPacking(n_bins::Int, n_items::Int, weights::Vector{T})

Uncapacitated bin packing

Implements an uncapacitated version of the bin-packing problem.

The first n_bins variables give the load in each bin, the last n_items give the number of the bin to which the item is assigned to.

The load of a bin is defined as the sum of the sizes of the items put in that bin.

Also called pack.

Example

[a, b, c] in BinPacking{NO_CAPACITY_BINPACKING}(1, 2, [2, 3])
# As there is only one bin, the only solution is to put all the items in 
# that bin.
# Enforces that:
# - the bin load is the sum of the weights of the objects in that bin: 
#   a = 2 + 3
# - the bin number of the two items is 1: b = c = 1

Fixed-capacity bin packing

Implements a capacitated version of the bin-packing problem where capacities are constant.

The first n_bins variables give the load in each bin, the last n_items give the number of the bin to which the item is assigned to.

The load of a bin is defined as the sum of the sizes of the items put in that bin.

This constraint is equivalent to BinPacking with inequality constraints on the loads of the bins where the upper bound is a constant. However, there are more efficient propagators for the combined constraint (bin packing with maximum load); if such propagators are not available, bridges are available to make the conversion seamless.

Also called bin_packing_capa.

Example

[a, b, c] in BinPacking{FIXED_CAPACITY_BINPACKING}(1, 2, [2, 3], [4])
# As there is only one bin, the only solution is to put all the items in
# that bin if its capacity is large enough.
# Enforces that:
# - the bin load is the sum of the weights of the objects in that bin: 
#   a = 2 + 3
# - the bin load is at most its capacity: a <= 4 (given in the set)
# - the bin number of the two items is 1: b = c = 1

Variable-capacity bin packing

Implements an capacitated version of the bin-packing problem where capacities are optimisation variables.

The first n_bins variables give the load in each bin, the next n_bins are the capacity of each bin, the last n_items give the number of the bin to which the item is assigned to.

The load of a bin is defined as the sum of the sizes of the items put in that bin.

This constraint is equivalent to BinPacking with inequality constraints on the loads of the bins where the upper bound is any expression. However, there are more efficient propagators for the combined constraint (bin packing with maximum load) and for the fixed-capacity version.

Also called bin_packing_capa.

Example

[a, 2, b, c] in BinPacking{VARIABLE_CAPACITY_BINPACKING}(1, 2, [2, 3])
# As there is only one bin, the only solution is to put all the items in
# that bin if its capacity is large enough.
# Enforces that:
# - the bin load is the sum of the weights of the objects in that bin: 
#   a = 2 + 3
# - the bin load is at most its capacity: a <= 2 (given in a variable)
# - the bin number of the two items is 1: b = c = 1
source
ConstraintProgrammingExtensions.BinPackingCapacityTypeType
BinPackingCapacityType

Whether the capacities of a BinPacking constraint are fixed:

  • either there is no capacity: NO_CAPACITY_BINPACKING
  • or the capacity values are fixed when creating the set: FIXED_CAPACITY_BINPACKING
  • or the capacity values are themselves variable: VARIABLE_CAPACITY_BINPACKING
source

Knapsack

ConstraintProgrammingExtensions.KnapsackType
Knapsack{KCT, KVT, T <: Real}(weights::T, capacity::Vector{T})

Fixed capacity, unvalued

Ensures that the n variables respect a knapsack constraint with fixed weights and a fixed capacity:

$\{x \in \{0, 1\}^n | \sum_{i=1}^n \mathtt{weights[i]} x_i \leq \mathtt{capacity} \}$.

Variable capacity, unvalued

Ensures that the first n variables respect a knapsack constraint with fixed weights and a capacity given by the last variable:

$\{(x, y) \in \{0, 1\}^n \times \mathbb{R} | \sum_{i=1}^n \mathtt{weights[i]} x_i \leq y \}$.

Fixed capacity, valued

Ensures that the n first variables respect a knapsack constraint with fixed weights and a fixed capacity, the last variable being the total value of the knapsack:

$\{(x, y) \in \{0, 1\}^n \times \mathbb{R} | \sum_{i=1}^n \mathtt{weights[i]} x_i \leq \mathtt{capacity} \land y = \sum_{i=1}^n \mathtt{values[i]} x_i \}$.

Variable capacity, valued

Ensures that the first n variables respect a knapsack constraint with fixed weights and a capacity given by the last-but-one variable; the total value is the last variable:

$\{(x, y, z) \in \{0, 1\}^n \times \mathbb{R} \times \mathbb{R} | \sum_{i=1}^n \mathtt{weights[i]} x_i \leq y \land z = \sum_{i=1}^n \mathtt{values[i]} x_i \}$.

source

Counting constraints

ConstraintProgrammingExtensions.CountType
Count{S <: MOI.AbstractScalarSet}(dimension::Int, set::MOI.AbstractScalarSet)

$\{(y, x) \in \mathbb{N} \times \mathbb{T}^\mathtt{dimension} : y = |\{i | x_i \in S \}|\}$

dimension is the number of variables that are checked against the set.

Also called among.

Example

[w, x, y, z] in Count(3, MOI.EqualTo(2.0))
# w == sum([x, y, z] .== 2.0)
source
ConstraintProgrammingExtensions.CountCompareType
CountCompare(dimension::Int)

$\{(z, x, y) \in \mathbb{N} \times \mathbb{R}^\mathtt{dimension} \times \mathbb{R}^\mathtt{dimension} : Z = |\{i | x_i = y_i\}|\}$

The first dimension variables are the first array that is compared to the second one, indicated by the next dimension variables. The last variable is the number of values that are identical in both arrays.

Example

[v, w, x, y, z] in Count(2)
# w == sum([w, x] .== [y, z])
source
ConstraintProgrammingExtensions.CountDistinctType
CountDistinct(dimension::Int)

The first variable in the set is forced to be the number of distinct values in the rest of the expressions.

This is a relaxed version of AllDifferent; it encodes an AllDifferent constraint when the first variable is the number of variables in the set.

Also called nvalues.

Example

[x, y, z] in CountDistinct(3)
# x = 1 if y == z, x = 2 if y != z
source

Global cardinality

ConstraintProgrammingExtensions.GlobalCardinalityType
GlobalCardinality{CVT, CVCT, T}(dimension::Int, values::Vector{T})

This set represents the large majority of the variants of the global-cardinality constraint, with the parameters set in CountedValuesType (CVT parameter) and CountedValuesClosureType (CVCT parameter).

Fixed and open

$\{(x, y) \in \mathbb{T}^\mathtt{dimension} \times \mathbb{N}^d : y_i = |\{ j | x_j = \mathtt{values}_i, \forall j \}| \}$

The first dimension variables are an array, the last variables are the number of times that each item of values is present in the first array. Values that are not in values are ignored.

Also called gcc or count.

Example

[x, y, z, v, w] in GlobalCardinality{FIXED_COUNTED_VALUES, OPEN_COUNTED_VALUES}(3, [2.0, 4.0])
[x, y, z, v, w] in GlobalCardinality{OPEN_COUNTED_VALUES}(3, [2.0, 4.0])
[x, y, z, v, w] in GlobalCardinality(3, [2.0, 4.0])
# v == sum([x, y, z] .== 2.0)
# w == sum([x, y, z] .== 4.0)

Variable and open

$\{(x, y, z) \in \mathbb{T}^\mathtt{dimension} \times \mathbb{N}^\mathtt{n\_values} \times \mathbb{T}^\mathtt{n\_values} : y_i = |\{ j | x_j = z_i, \forall j \}| \}$

The first dimension variables are an array, the next n_values variables are the number of times that each item of the last n_values variables is present in the first array. Values of the first array that are not in the n_values are ignored.

Also called distribute.

Example

[x, y, z, t, u, v, w] in GlobalCardinality{VARIABLE_COUNTED_VALUES, OPEN_COUNTED_VALUES, T}(3, 2)
[x, y, z, t, u, v, w] in GlobalCardinality{OPEN_COUNTED_VALUES, T}(3, 2)
[x, y, z, t, u, v, w] in GlobalCardinality{T}(3, 2)
# t == sum([x, y, z] .== v)
# u == sum([x, y, z] .== w)

Fixed and closed

$\{(x, y) \in \mathbb{T}^\mathtt{dimension} \times \mathbb{N}^d : y_i = |\{ j | x_j = \mathtt{values}_i, \forall j \}| \}$

The first dimension variables are an array, the last variables are the number of times that each item of values is present in the first array. Each value of the first array must be within values.

Example

[x, y, z, v, w] in GlobalCardinality{FIXED_COUNTED_VALUES, CLOSED_COUNTED_VALUES, T}(3, [2.0, 4.0])
# v == sum([x, y, z] .== 2.0)
# w == sum([x, y, z] .== 4.0)
# x ∈ [2.0, 4.0], y ∈ [2.0, 4.0], z ∈ [2.0, 4.0]

Variable and closed

$\{(x, y, z) \in \mathbb{T}^\mathtt{dimension} \times \mathbb{N}^\mathtt{n\_values} \times \mathbb{T}^\mathtt{n\_values} : y_i = |\{ j | x_j = z_i, \forall j \}| \}$

The first dimension variables are an array, the next n_values variables are the number of times that each item of the last n_values variables is present in the first array. Each value of the first array must be within the next given n_values.

Also called distribute.

Example

[x, y, z, t, u, v, w] in GlobalCardinality{VARIABLE_COUNTED_VALUES, CLOSED_COUNTED_VALUES, T}(3, 2)
# t == sum([x, y, z] .== v)
# u == sum([x, y, z] .== w)
# x ∈ [v, w], y ∈ [v, w], z ∈ [v, w]
source
ConstraintProgrammingExtensions.CountedValuesTypeType
CountedValuesType

Kind of values to be counted for a GlobalCardinality constraint:

  • either the values to count are fixed when creating the set: FIXED_COUNTED_VALUES
  • or the values are themselves variables (typically constrained elsewhere): VARIABLE_COUNTED_VALUES
source
ConstraintProgrammingExtensions.CountedValuesClosureTypeType
CountedValuesClosureType

Whether values that are not counted in GlobalCardinality constraint are allowed in the array whose values are counted:

  • either uncounted values are allowed: OPEN_COUNTED_VALUES
  • or they are not allowed: CLOSED_COUNTED_VALUES
source

Graph constraints

ConstraintProgrammingExtensions.WalkType
Walk{VWT, EWT, WT, WST, WsT, WtT, T}(n_nodes::Int)

A walk in an undirected graph.

If the vector x describes the walk within a Walk constraint, each x[i] denotes the next vertex in the n-vertex graph, for i ∈ [1, n].

The considered graph is an undirected complete graph with n vertices. To model a walk in a noncomplete graph, you can add constraints on the variables: if the vertex i only has edges towards j and k, then x[i] should only have the possible values j and k.

The dimensions of this set are as follows:

  • first, the description of the walk, typically denoted by x
  • second, the source vertex, depending on WsT
  • third, the destination vertex, depending on WtT
  • fourth, the individual weights, depending on VWT and EWT – vertices (VWT) come before edges (EWT)
  • fifth, the total weights, depending on VWT and EWT – vertices (VWT) come before edges (EWT)
  • sixth, the total weight, depending on VWT and EWT (sum of the weight over the vertices [VWT] and the edges [EWT])

For cycles, all the variables describing the cycle are implied to have an integer value between 1 and n. For other walks, the walk-description variables

Some variants are called circuit or atour.

GCC: https://sofdem.github.io/gccat/gccat/Ccircuit.html

Unweighted walk

Walk{UNWEIGHTED_VERTEX, UNWEIGHTED_EDGE, WalkType, WalkSubType, WalkSourceType, WalkDestinationType, T} considers an unweighted walk, for all WalkType, WalkSubType, WalkSourceType, WalkDestinationType, and T <: Real.

x-in-Walk{UNWEIGHTED_VERTEX, UNWEIGHTED_EDGE, WT, WST, WsT, WtT, T}(n): a walk in the complete graph of n vertices. x[i] is the index of the next vertex after i in the walk.

Fixed-edge-weight cycle

Walk{UNWEIGHTED_VERTEX, FIXED_WEIGHT_EDGE, CYCLE_WALK, NO_SPECIFIC_WALK, NO_SOURCE_VERTEX, NO_DESTINATION_VERTEX, T} considers a cycle whose edge weights are fixed: having an edge in the cycle increases the total weight. Vertices are unweighted, because all of them must be included in a cycle.

[x, tw]-in-Walk{UNWEIGHTED_VERTEX, FIXED_WEIGHT_EDGE, CYCLE_WALK, NO_SPECIFIC_WALK, NO_SOURCE_VERTEX, NO_DESTINATION_VERTEX, T}(n, edge_weights) where the elements of edge_weights have type T:

  • x is a cycle in the complete graph of n vertices, x[i] is the index of the next vertex in the cycle

  • tw is the total weight of the cycle, with edge_weights being indexed by the vertices:

    $\mathtt{tw} = \sum_{i=1}^{n} \mathtt{edge_weights[i, x[i]]}$

Variable-vertex-weight path

Walk{VARIABLE_WEIGHT_VERTEX, UNWEIGHTED_EDGE, PATH_WALK, NO_SPECIFIC_WALK, FIXED_SOURCE_VERTEX, FIXED_DESTINATION_VERTEX, T} considers a path whose vertex weights are variable. Having a vertex in the cycle increases the total weight, but edges do not contribute in this case (although there is no reason why they could not).

[x, w, tw]-in-Walk{VARIABLE_WEIGHT_VERTEX, UNWEIGHTED_EDGE, PATH_WALK, NO_SPECIFIC_WALK, FIXED_SOURCE_VERTEX, FIXED_DESTINATION_VERTEX, T}(n):

  • x is a path in the complete graph of n vertices, x[i] is the index of the next vertex in the path

  • w is the weight of each vertex (a vector indexed by the vertex indices)

  • tw is the total vertex weight of the path:

    $\mathtt{tw} = \sum_{i=1}^{n} \mathtt{w[x[i]]}$

source

Reification constraints

ConstraintProgrammingExtensions.ReificationType
Reification{S <: MOI.AbstractSet}(set::S)

$\{(y, x) \in \{0, 1\} \times \mathbb{R}^n | y = 1 \iff x \in set, y = 0 otherwise\}$.

This set serves to find out whether a given constraint is satisfied.

The only possible values are 0 and 1 for the first variable of the set.

source
ConstraintProgrammingExtensions.EquivalenceType
Equivalence{S1 <: MOI.AbstractSet, S2 <: MOI.AbstractSet}(set1::S1, 
                                                          set2::S2)

The logical equivalence operator ≡ or ⇔.

$\{(x, y) \in \mathbb{R}^{a+b} | x \in S1 \iff y \in S2\}$.

The two constraints must be either satisfied or not satisfied at the same time. More explicitly, if the first one is satisfied, then the second one is implied to be satisfied too; if the second one is satisfied, then the first one is implied.

source
ConstraintProgrammingExtensions.EquivalenceNotType

EquivalenceNot{S1 <: MOI.AbstractSet, S2 <: MOI.AbstractSet}(set1::S1, set2::S2)

The logical equivalence operator ≡ or ⇔, with the second argument negated.

$\{(x, y) \in \mathbb{R}^{a+b} | x \in S1 \iff y \not\in S2\}$.

source
ConstraintProgrammingExtensions.IfThenElseType
IfThenElse{
    Condition <: MOI.AbstractSet, 
    TrueConstraint <: MOI.AbstractSet, 
    FalseConstraint <: MOI.AbstractSet
}(condition::Condition, true_constraint::TrueConstraint, 
  false_constraint::FalseConstraint)

The ternary operator.

If the condition is satisfied, then the first constraint (of type TrueConstraint) will be implied. Otherwise, the second constraint (of type FalseConstraint) will be implied.

$\{(x, y, z) \in \mathbb{R}^(a+b+c) | y \in TrueConstraint \iff x \in set, z \in FalseConstraint otherwise\}$.

source
ConstraintProgrammingExtensions.ImplicationType
Implication{
    Antecedent <: MOI.AbstractSet,
    Consequent <: MOI.AbstractSet
}(antecedent::Antecedent, consequent::Consequent)

The logical implication operator ⇒.

If the antecedent is satisfied, then the consequent will be implied to be satisfied. Otherwise, nothing is implied on the truth value of consequent.

$\{(x, y) \in \mathbb{R}^a \times \mathbb{R}^b | y \in Consequent if x \in Antecedent\}$.

Also called if_then, material implication, or material conditional.

source
ConstraintProgrammingExtensions.ConjunctionType
Conjunction{Ts}(constraints::Ts)

The logical conjunction operator ∧ (AND): all the constraints in the conjunction must be satisfied.

$\{(x, y\dots) \in \mathbb{R}^a \times \mathbb{R}^b\dots | x \in \mathbb{S_1} \land y \in \mathbb{S_2} \dots \}$.

source
ConstraintProgrammingExtensions.DisjunctionType
Disjunction{Ts}(constraints::Ts)

The logical disjunction operator ∨ (OR): at least one of the constraints in the disjunction must be satisfied.

$\{(x, y\dots) \in \mathbb{R}^a \times \mathbb{R}^b\dots | x \in \mathbb{S_1} \lor y \in \mathbb{S_2} \dots \}$.

source

Scheduling constraints

Cumulative resource

ConstraintProgrammingExtensions.CumulativeResourceType
CumulativeResource{CRDT}(n_tasks::Int)

This set models most variants of task scheduling with cumulative resource usage. Presence of deadlines can be indicated with the CumulativeResourceDeadlineType enumeration.

Without deadline

Each task is given by a minimum start time (the first n_tasks variables), a duration (the next n_tasks variables), and the resource consumption (the following n_tasks variables). The final variable is the maximum amount of the resource available.

Also called cumulative. This version does not consider end deadlines for tasks.

With variable deadline

Each task is given by a minimum start time (the first n_tasks variables), a duration (the next n_tasks variables), a deadline (the following n_tasks variables), and the resource consumption (the next n_tasks variables). The final variable is the maximum amount of the resource available.

Also called cumulative

source

Non-overlapping orthotopes

ConstraintProgrammingExtensions.NonOverlappingOrthotopesType
NonOverlappingOrthotopes{NOOCT}(n_orthotopes::Int, n_dimensions::Int)

This set corresponds to a guarantee that orthotopes do not overlap. Some orthotopes can optionally be disabled for the constraint (guided by variables), based on the value of NonOverlappingOrthotopesConditionalityType.

Unconditional constraint

Guarantees that the n_orthotopes orthotopes do not overlap. The orthotopes live in various dimensions: segments if n_dimensions = 1, rectangles if n_dimensions = 2, rectangular parallelepiped if n_dimensions = 3, hyperrectangles otherwise.

The variables are packed by orthotope:

  • the first n_dimensions are the origin of the orthotope
  • the next n_dimensions are the size of the orthotope in each dimension
  • the last n_dimensions are the destination of the orthotope. These variables are automatically constrained to be origin + size (unlike other modelling layers, such as Gecode)

The set can be defined as:

$(o_1, s_1, d_1, o_2, s_2, d_2 \dots o_\mathtt{o}, s_\mathtt{o}, d_\mathtt{o}) \in \mathbb{R}^{3 \times \mathtt{o} \times \mathtt{d} }$

Also called diffn, geost, nooverlap, diff2, or disjoint.

Example: two 2-D rectangles

[x1, y1, w1, h1, x1e, y1e, x2, y2, w2, h2, x2e, y2e] in NonOverlappingOrthotopes(2, 2)
# Enforces the following five constraints: 
#   OR(
#     x1 + w1 <= x2,
#     x2 + w2 <= x1,
#     y1 + h1 <= y2,
#     y2 + h2 <= y1
#   )
#   x1e = x1 + w1
#   y1e = y1 + h1
#   x2e = x2 + w2
#   y2e = y2 + h2

Conditional constraint

Guarantees that the n_orthotopes orthotopes do not overlap, with a binary variable indicating whether a given orthotope must not overlap with other orthotopes (if 1) or if it can be ignored (if 0). The orthotopes live in various dimensions: segments if n_dimensions = 1, rectangles if n_dimensions = 2, rectangular parallelepiped if n_dimensions = 3, hyperrectangles otherwise.

The variables are packed by orthotope:

  • the first n_dimensions are the origin of the orthotope
  • the next n_dimensions are the size of the orthotope in each dimension
  • the next n_dimensions are the destination of the orthotope. These variables are automatically constrained to be origin + size (unlike other modelling layers, such as Gecode)
  • the last variable indicates whether the orthotope is mandatory (true) or optional (false)

The set can be defined as:

$(o_1, s_1, d_1, m_1, o_2, s_2, d_2, m_2 \dots o_\mathtt{o}, s_\mathtt{o}, d_\mathtt{o}, m_\mathtt{o}) \in \prod_{i=1}^{\mathtt{o}} (\mathbb{R}^{3 \times \mathtt{d} \times \{0, 1\}) }$

Also called diffn, nooverlap, or disjointconditional.

source

Sorting constraints

Lexicographic order

ConstraintProgrammingExtensions.LexicographicallyLessThanType
LexicographicallyLessThan(row_dim::Int, column_dim::Int)

Ensures that each column of the matrix is lexicographically less than the next column.

Formally, for two columns:

$\{(x, y) \in \mathbb{R}^\mathtt{column\_dim} \times \mathbb{R}^\mathtt{column\_dim} | \exists j \in \{1, 2 \dots \mathtt{column\_dim}\}: x_j < y_j, \forall i < j, x_i = y_i \}$.

Also called lex_less.

The matrix is encoded by stacking the columns, matching the behaviour of Julia's vec function.

source
ConstraintProgrammingExtensions.LexicographicallyGreaterThanType
LexicographicallyGreaterThan(row_dim::Int, column_dim::Int)

Ensures that each column of the matrix is lexicographically greater than the next column.

Formally, for two columns:

$\{(x, y) \in \mathbb{R}^\mathtt{column\_dim} \times \mathbb{R}^\mathtt{column\_dim} | xists j \in \{1, 2 \dots \mathtt{column\_dim}\}: x_j > y_j, \forall i < j, x_i = y_i \}$.

Also called lex_greater.

The matrix is encoded by stacking the columns, matching the behaviour of Julia's vec function.

source
ConstraintProgrammingExtensions.DoublyLexicographicallyLessThanType
DoublyLexicographicallyLessThan(dimension::Int)

Ensures that each column of the matrix is lexicographically less than the next column, and that each row of the matrix is lexicographically less than the next row.

Also called lex2.

The matrix is encoded by stacking the columns, matching the behaviour of Julia's vec function.

source
ConstraintProgrammingExtensions.DoublyLexicographicallyGreaterThanType
DoublyLexicographicallyGreaterThan(dimension::Int)

Ensures that each column of the matrix is lexicographically greater than the next column, and that each row of the matrix is lexicographically greater than the next row.

The matrix is encoded by stacking the columns, matching the behaviour of Julia's vec function.

source

Typical order

ConstraintProgrammingExtensions.SortType
Sort(dimension::Int)

Ensures that the first dimension elements is a sorted copy of the next dimension elements.

Example

[a, b, c, d] in Sort(2)
# Enforces that:
# - the first part is sorted: a <= b
# - the first part corresponds to the second one:
#     - either a = c and b = d
#     - or a = d and b = c
source
ConstraintProgrammingExtensions.SortPermutationType
SortPermutation(dimension::Int)

Ensures that the first dimension elements is a sorted copy of the next dimension elements.

The last dimension elements give a permutation to get from the original array to its sorted version.

Example

[a, b, c, d, i, j] in SortPermutation(2)
# Enforces that:
# - the first part is sorted: a <= b
# - the first part corresponds to the second one:
#     - either a = c and b = d: in this case, i = 1 and j = 2
#     - or a = d and b = c: in this case, i = 2 and j = 1
source

Extrema

ConstraintProgrammingExtensions.ArgumentMaximumAmongType
ArgumentMaximumAmong(dimension::Int)

Ensures that the first element is the index of the maximum value among the next dimension elements.

Example

[a, b, c] in ArgumentMaximumAmong(2)
# Enforces that a == argmax(b, c)
# I.e., if b > c, a = 1, if b < c, a = 2
source
ConstraintProgrammingExtensions.ArgumentMinimumAmongType
ArgumentMinimumAmong(dimension::Int)

Ensures that the first element is the index of the minimum value among the next dimension elements.

Example

[a, b, c] in ArgumentMinimumAmong(2)
# Enforces that a == argmin(b, c)
# I.e., if b < c, a = 1, if b > c, a = 2
source

Strict constraints

ConstraintProgrammingExtensions.StrictlyType
Strictly{S <: Union{LessThan{T}, GreaterThan{T}, LexicographicallyGreaterThan}}

Converts an inequality set to a set with the same inequality made strict. For example, while LessThan(1) corresponds to the inequality x <= 1, Strictly(LessThan(1)) corresponds to the inequality x < 1.

Example

x in Strictly(LessThan(1))
source