10.10.4.4 Arithmetic-Logical Constraints

`smt(:ConstraintBody)   since release 4.2`

The arithmetic, membership, and propositional constraints described earlier are transformed at compile time to conjunctions of library constraints. Although linear in the size of the source code, the expansion of a propositional formula over reifiable constraints to library goals can have time and memory overheads, and propagates disjunctions very weakly. Temporary variables holding intermediate values may have to be introduced, and the grain size of the constraint solver invocations can be rather small. As an alternative to the default propagation of such constraint formulas, this constraint is a front-end to the `case/[3,4]` propagator, which treats such a formula globally. The pruning can be stronger and it can run faster than the default propagator, but this is not necessarily the case. Bounds consistency is not guaranteed.

ConstraintBody should be of one of the following forms, or a propositional combination of such forms. See Syntax of Indexicals for the exact definition:

• var `in` ConstantRange
• `element(var,CList,var)`
• `table([VList],CTable)`
• LinExpr RelOp LinExpr
• var { `X` stands for `X#=1` }
`count(+Val,+List,+RelOp,?Count)   since release 4.0.5,deprecated`

where Val is an integer, List is a list of domain variables, Count a domain variable, and RelOp is a relational symbol as in Arithmetic Constraints. True if N is the number of elements of List that are equal to Val and N RelOp Count. Implemented by decomposition into one `sum/3` constraint, one arithmetic comparison, and several reified equalities.

Corresponds to `count_*/3`, `exactly/3` in MiniZinc.

`count/4` maintains domain consistency, but in practice, the following constraint is a better alternative.

`global_cardinality(+Xs,+Vals)`
`global_cardinality(+Xs,+Vals,+Options)`

where Xs = [X1,…,Xd] is a list of domain variables, and Vals = [K1-V1,…,Kn-Vn] is a list of pairs where each key Ki is a unique integer and Vi is a domain variable. True if every element of Xs is equal to some key and for each pair Ki-Vi, exactly Vi elements of Xs are equal to Ki.

If either Xs or Vals is ground, and in many other special cases, `global_cardinality/[2,3]` maintains domain consistency, but generally, bounds consistency cannot be guaranteed. A domain consistency algorithm [Regin 96] is used, roughly linear in the total size of the domains.

Corresponds to `global_cardinality*/*` and `distribute/3` in MiniZinc.

Options is a list of zero or more of the following:

`consistency(Cons)`

Which filtering algorithm to use. One of the following:

`domain`

The constraint will use the algorithm mentioned above. Implies `on(dom)`. The default.

`bounds`

The constraint will use the algorithm mentioned above. Implies `on(minmax)`.

`value`

The constraint will use a simple algorithm, which prevents too few or too many of the Xs from taking values among the Vals. Implies `on(val)`.

`on(On)`

How eagerly to wake up the constraint. One of the following:

`dom`

to wake up when the domain of a variable is changed (the default);

`minmax`

to wake up when a bound of a variable is changed;

`val`

to wake up when a variable is fixed.

`cost(Cost,Matrix)`

Overrides any `consistency/1` option value. A cost is associated with the constraint and reflected into the domain variable Cost. Matrix should be a d*n matrix of integers, represented as a list of d lists, each of length n. Assume that each Xi equals K(pi). The cost of the constraint is then Matrix[1,p1]+…+Matrix[d,pd].

With this option, a domain consistency algorithm [Regin 99] is used, the complexity of which is roughly O(d(m + n log n)) where m is the total size of the domains.

`all_different(+Variables)`
`all_different(+Variables, +Options)`
`all_distinct(+Variables)`
`all_distinct(+Variables, +Options)`

where Variables is a list of domain variables. Each variable is constrained to take a value that is unique among the variables. Declaratively, this is equivalent to an inequality constraint for each pair of variables.

Corresponds to `alldifferent/1` in MiniZinc.

Options is a list of zero or more of the following:

`L #= R   since release 4.3`

where R should be an integer, and L an expressions of one of the following forms, where X1, …, Xj occur among Variables:

`X1 + ... + Xj`
`X1*X1 + ... + Xj*Xj`
`X1 * ... * Xj`

The given equation is a side constraint for the constraint to hold. A special bounds consistency algorithm is used, which considers the main constraint and the side constraints globally. This option is only valid if the domains of X1, …, Xj consist of integers strictly greater than zero.

`consistency(Cons)`

Which algorithm to use, one of the following:

`domain`

The default for `all_distinct/[1,2]` and `assignment/[2,3]`. A domain consistency algorithm [Regin 94] is used, roughly linear in the total size of the domains. Implies `on(dom)`.

`bounds`

A bounds consistency algorithm [Lopez-Ortiz 03] is used, which runs in O(n log n) time for n variables. Implies `on(minmax)`.

`value`

The default for `all_different/[1,2]`. An algorithm achieving exactly the same pruning as a set of pairwise inequality constraints is used, roughly linear in the number of variables. Implies `on(val)`.

`on(On)`

How eagerly to wake up the constraint. One of the following:

`dom`

(the default for `all_distinct/[1,2]` and `assignment/[2,3]`), to wake up when the domain of a variable is changed;

`min`

to wake up when the lower bound of a domain is changed;

`max`

to wake up when the upper bound of a domain is changed;

`minmax`

to wake up when some bound of a domain is changed;

`val`

(the default for `all_different/[1,2]`), to wake up when a variable is fixed.

`nvalue(?N, +Variables)`

where Variables is a list of domain variables with finite bounds, and N is a domain variable. True if N is the number of distinct values taken by Variables. Approximates bounds consistency in N and domain consistency in Variables. Can be thought of as a relaxed version of `all_distinct/2`.

Corresponds to `nvalue/2` in MiniZinc.

The following is a constraint over two lists of length n of variables. Each variable is constrained to take a value in [1,n] that is unique for its list. Furthermore, the lists are dual in a sense described below.

`assignment(+Xs, +Ys)`
`assignment(+Xs, +Ys, +Options)`

where Xs = [X1,…,Xn] and Ys = [Y1,…,Yn] are lists of domain variables. True if all Xi, Yi in [1,n] and Xi=j iff Yj=i.

Corresponds to `inverse/2` in MiniZinc.

Options is a list of zero or more of the following, where Boolean must be `true` or `false` (`false` is the default):

`on(On)`

Same meaning as for `all_different/2`.

`consistency(Cons)`

Same meaning as for `all_different/2`.

`circuit(Boolean)`

If `true`, `circuit(Xs,Ys)` must hold for the constraint to be true.

`cost(Cost,Matrix)`

A cost is associated with the constraint and reflected into the domain variable Cost. Matrix should be an n*n matrix of integers, represented as a list of lists. The cost of the constraint is Matrix[1,X1]+…+Matrix[n,Xn].

With this option, a domain consistency algorithm [Sellmann 02] is used, the complexity of which is roughly O(n(m + n log n)) where m is the total size of the domains.

The following constraint captures the relation between a list of values, a list of the values in ascending order, and their positions in the original list:

`sorting(+Xs,+Ps,+Ys)`

where Xs = [X1,…,Xn], Ps = [P1,…,Pn], and Ys = [Y1,…,Yn] are lists of domain variables. The constraint holds if the following are true:

• Ys is in ascending order.
• Ps is a permutation of [1,n].
• for all i in [1,n] : Xi = Y(Pi)

In practice, the underlying algorithm [Mehlhorn 00] is likely to achieve bounds consistency, and is guaranteed to do so if Ps is ground or completely free.

Corresponds to `sort/2` in MiniZinc.

The following constraint is a generalization of `sorting/3`, namely:

• It sorts not domain variables, but tuples of them.
• The tuples are split into a key prefix and a value suffix. They are sorted wrt. the key part only.
• The sort is stable: if two tuples have identical keys, their relative order is preserved in the output.
`keysorting(+Xs,+Ys)   since release 4.3.1`
`keysorting(+Xs,+Ys,+Options)`

where Xs and Ys are lists of tuples of domain variables. Both lists should be of the same length n, and all tuples should have the same length m. The constraint holds if the following are true:

• Ps is a permutation of [1,n].
• for all i in [1,n], j in [1,m] : Ys[i,j] = Xs[Ps[i],j].
• [[Ys[i,1],...,Ys[i,k],Ps[i]] | i in [1,n]] is in lex ascending order, where k equals Keys as defined below in the options.

The filtering algorithm is based on [Mehlhorn 00] and endeavors to achieve bounds consistency, but does not guarantee it.

Corresponds to Prolog’s `keysort/2`. In particular, the sort is stable by definition.

Options is a list of zero or more of the following:

`keys(Keys)`

where Keys should be a positive integer, denoting the length of the key prefix. The default is 1.

`permutation(Ps)`

where Ps should be a list of length n of domain variables. Its meaning is described above.

The following constraints express the fact that several vectors of domain variables are in ascending lexicographic order:

`lex_chain(+Vectors)`
`lex_chain(+Vectors,+Options)`

where Vectors is a list of vectors (lists) of domain variables with finite bounds. The constraint holds if Vectors are in ascending lexicographic order.

Corresponds to `*lex2/1`, `lex_greater*/2`, `lex_less*/2` in MiniZinc.

Options is a list of zero or more of the following:

`op(Op)`

If Op is the atom `#=<` (the default), the constraints holds if Vectors are in non-descending lexicographic order. If Op is the atom `#<`, the constraints holds if Vectors are in strictly ascending lexicographic order.

`increasing`

This option imposes the additional constraint that each vector in Vectors be sorted in strictly ascending order.

`among(Least,Most,Values)`

If given, Least and Most should be integers such that 0 <= Least <= Most and Values should be a list of distinct integers. This option imposes the additional constraint on each vector in Vectors that at least Least and at most Most elements belong to Values.

`global(Boolean)   since release 4.2.1`

if `true`, a more expensive algorithm [Carlsson & Beldiceanu 02], which guaranteed domain consistency unless the `increasing/0` or `among/3` options are given, will be used.

In the following constraints, a literal is either a term `X` or a term `#\ X`, where `X` is a 0/1 variable. They maintain domain consistency:

`bool_and(+Lits, +Lit)   since release 4.3`

where Lits is a list of literals `[L0,...,Lj]` and Lit is a literal. True if Lit equals the Boolean conjunction of Lits, and usually more efficient than the equivalent `L0#/\...#/\Lj #<=> Lit`.

`bool_or(+Lits, +Lit)   since release 4.3`

where Lits is a list of literals `[L0,...,Lj]` and Lit is a literal. True if Lit equals the Boolean disjunction of Lits, and usually more efficient than the equivalent `L0#\/...#\/Lj #<=> Lit`.

`bool_xor(+Lits, +Lit)   since release 4.3`

where Lits is a list of literals `[L0,...,Lj]` and Lit is a literal. True if Lit equals the Boolean exclusive or of Lits, and usually more efficient than the equivalent `L0#\...#\Lj #<=> Lit`.

`bool_channel(+Lits, ?Y, +Relop, +Offset)   since release 4.3`

where Lits is a list of literals `[L0,...,Lj]`, Y is a domain variable, RelOp is an arithmetic comparison as in Syntax of Arithmetic Expressions, and Offset is an integer. Expresses the constraint Li #<=> (Y RelOp i+Offset) for `i in 0..j`. Usually more efficient than a bunch of reified comparisons between a given variable and a sequence of integers.

Send feedback on this subject.