Constraints

Choosing which constraint to use

Minion offers several constraints which implement the same logical operation. These different constraints have different trade-offs and the best one to use varies between problems. This section will provide some basic guidance.

The philosophy of Minion’s input language is that the input language matches the features Minion implements internally. Unlike most other constraint solvers, Minion does not break up constraints into smaller pieces, introduce new variables or simplify or manipulate constraints. This provides complete control over how Minion represents your problem, but also introduces challenges.

One notable missing constraint is the “sum equals” constraint. Since the most efficient way to implement such a constraint would be by combining sumleq and sumgeq, Minion doesn’t offer a wrapper for it. However, if an efficient implementation of sumeq is discovered in the future, it may be added.

The watchsumgeq and watchsumleq are variants on the algorithm used to implement SAT constraints. They are faster than sumleq and sumgeq, but only work when summing a list of Booleans to a constant. Further, watchsumgeq performs best when the value being summed to is small, and watchsumleq works best when the value being summed to is close to the size of the input vector.

Minion does not attempt to simplify constraints, so constraints such as sumgeq([a,a,a], 3) are not simplified to sumgeq([a],1). This kind of simplification will often significantly improve performance. Rather than perform such transformations (which do have trade-offs), Minion leaves this tuning to the user, or alternatively (and much more sensibly!) to specialised tools such SavileRow or Conjure.

There are two main reasons there are multiple implementations of the same constraint:

• One version achieves more reasoning at the cost of speed.

• One version does not work on BOUND and SPARSEBOUND variables (often, the version for BOUND and SPARSEBOUND achieves lower reasoning).

It is impossible to predict if problems will be solved faster with more or less reasoning – in general using higher levels of reasoning is advisable since the possible gains from lower levels of reasoning tend to be smaller than the possible losses (which can be many orders of magnitude).

We will now go through all the constraints in Minion, grouped into categories.

All Different, Cardinality and Counting Constraints

alldiff

Forces the input vector of variables to take distinct values.

Suppose the input file had the following vector of variables defined:

DISCRETE myVec[9] {1..9}

Then alldiff(myVec) enforces all variables in myVec take different values.

This constraint enforces the same level of consistency as a clique of not equals constraints.

Related constraints

See gacalldiff for an implementation which achieves GAC.

gacalldiff

Forces the input vector of variables to take distinct values.

Suppose the input file had the following vector of variables defined:

DISCRETE myVec[9] {1..9}

Then gacalldiff(myVec) enforces all variables in myVec take different values. This constraint enforces generalised arc consistency.

Related constraints

See alldiff is faster but performs less reasoning.

alldiffmatrix

alldiffmatrix(myVec, value)

myVec is a square matrix flattened into a vector, and value is a single value – not a dimension. The size is taken from the length of the vector, which must be a perfect square.

The constraint concerns one value at a time: it ensures that value appears exactly once in every row and exactly once in every column. Equivalently, it ensures there is a bipartite matching between rows and columns where the edges in the matching correspond to a pair (row, column) whose variable may be assigned value.

One such constraint therefore does not make a latin square on its own. You build one by posting it once for each value, which is what the name refers to. For a 3x3 matrix over {1..3}, posting it for values 1, 2 and 3 gives exactly the 12 latin squares of order 3; posting it for value 1 alone leaves 384 solutions.

BOUND and SPARSEBOUND variables are rejected.

Notes

This constraint adds some extra reasoning in addition to the GAC Alldifferents on the rows and columns.

gcc

The Generalized Cardinality Constraint (GCC) constrains the number of each value that a set of variables can take.

gcc([primary variables], [values of interest], [capacity variables])

For each value of interest, there must be a capacity variable, which specifies the number of occurrences of the value in the primary variables.

This constraint only restricts the number of occurrences of the values in the value list. There is no restriction on the occurrences of other values. Therefore the semantics of gcc are identical to a set of occurrence constraints like this:

occurrence([primary variables], val1, cap1)
occurrence([primary variables], val2, cap2)
...

Example

Suppose the input file had the following vectors of variables defined:

DISCRETE myVec[9] {1..9}
BOUND cap[9] {0..2}

The following constraint would restrict the occurrence of values 1..9 in myVec to be at most 2 each initially, and finally equal to the values of the cap vector.

gcc(myVec, [1,2,3,4,5,6,7,8,9], cap)

Notes

This constraint enforces a hybrid consistency. It reads the bounds of the capacity variables, then enforces GAC over the primary variables only. Then the bounds of the capacity variables are updated using flow algorithms similar to those proposed by Quimper et al, Improved Algorithms for the Global Cardinality Constraint (CP 2004).

This constraint provides stronger propagation to the capacity variables than the gccweak constraint.

gccweak

The Generalized Cardinality Constraint (GCC) (weak variant) implements the same constraint as gcc, with a weaker (but faster) level of propagation.

This constraint enforces a hybrid consistency. It reads the bounds of the capacity variables, then enforces GAC over the primary variables only. Then the bounds of the capacity variables are updated by counting values in the domains of the primary variables.

The consistency over the capacity variables is weaker than the gcc constraint, hence the name gccweak.

occurrence

The constraint occurrence(vec, elem, count) ensures that there are count occurrences of the value elem in the vector vec.

elem must be a constant.

occurrenceleq

The constraint occurrenceleq(vec, elem, count) ensures that there are AT MOST count occurrences of the value elem in the vector vec.

elem and count must be constants

occurrencegeq

The constraint occurrencegeq(vec, elem, count) ensures that there are AT LEAST count occurrences of the value elem in the vector vec.

elem and count must be constants

nvalueleq

The constraint nvalueleq(vec,x) ensures that there are <= x different values assigned to the list of variables vec.

nvaluegeq

The constraint nvaluegeq(vec,x) ensures that there are >= x different values assigned to the list of variables vec.

Accessing Elements of Arrays

element

The constraint element(vec, i, e) specifies that vec[i] = e (treating vec as a 0-indexed array). This implies that i is in the range [0..len(vec)-1].

Notes

Warning: This constraint is not confluent. Depending on the order the propagators are called in Minion, the number of search nodes may vary when using element. To avoid this problem, use watchelement instead. Technical details below.

The level of propagation enforced by this constraint is not named, however it works as follows. For constraint vec[i]=e:

• After i is assigned, ensures that min(vec[i]) = min(e) and max(vec[i]) = max(e).

• When e is assigned, removes idx from the domain of i whenever e is not an element of the domain of vec[idx].

• When m[idx] is assigned, removes idx from i when m[idx] is not in the domain of e.

This level of consistency is designed to avoid the propagator having to scan through vec, except when e is assigned. It does a quantity of cheap propagation and may work well in practice.

For example, the following input causes Minion to search 41 nodes.

MINION 3
**VARIABLES**
DISCRETE x[5] {1..5}
**CONSTRAINTS**
element([x[0],x[1],x[2]], x[3], x[4]) alldiff([x])
**EOF**

However if the two constraints are swapped over, Minion explores 29 nodes.

Related constraints

See watchelement for details of a logically identical constraint that enforces generalised arc consistency.

element_one

The constraint element_one is identical to element, except that the vector is indexed from 1 rather than from 0.

element_undefzero

The constraint element_undefzero(vec, i, e)

specifies that, in any solution, either:

• vec[i] = e and i is in the range [0 .. len(v)-1]

• i is outside the index range of vec, and e = 0

This is the non-watched variant; see watchelement_undefzero for a GAC-enforcing version.

watchelement_one

This constraint is identical to watchelement, except the vector is indexed from 1 rather than from 0.

watchelement

The constraint watchelement(vec, i, e) specifies that vec[i] = e. This implies that i is in the range [0..len(vec)-1]. Enforces generalised arc consistency.

See entry element for details of an identical constraint that enforces a lower level of consistency.

watchelement_undefzero

The constraint watchelement_undefzero(vec, i, e)

specifies that, in any solution, either:

• vec[i] = e and i is in the range [0 .. len(v)-1]

• i is outside the index range of vec, and e = 0

This differs from watchelement (and element) which are false if i is outside the index range of vec.

In general, use watchelement unless you have a special reason to use this constraint!

watchelement_one_undefzero

This constraint is identical to watchelement_undefzero, except the vector is indexed from 1 rather than from 0.

Arithmetic Constraints

difference

The constraint difference(x,y,z) ensures that z=|y-x|. This constraint achieves bounds consistency

eq

eq(x,y) ensures that x=y. This constraint implements bounds consistency.

Related constraints

minuseq

minuseq

minuseq(x,y) ensures that x=-y. The constraint implements bounds consistency.

Related constraints

eq

gaceq

gaceq(x,y) ensures that x=y, enforcing generalised arc consistency. This is a GAC variant of eq.

diseq

diseq(x,y) ensures that x is not equal y. Achieves arc consistency.

watchneq

watchneq(x,y) ensures that x is not equal y. This is the watched variant of diseq and may perform better when one variable is assigned early.

ineq

The constraint ineq(x, y, k) ensures that x <= y + k in any solution. k must be a constant. Minion has no strict inequality (<) constraints. However x < y can be achieved by ineq(x, y, -1)

watchless

The constraint watchless(x,y) ensures that x is less than y.

abs

The constraint abs(x,y) makes sure that x=|y|, i.e. x is the absolute value of y.

max

The constraint max(vec, x) ensures that x is equal to the maximum value of any variable in vec.

min

The constraint min(vec, x) ensures that x is equal to the minimum value of any variable in vec.

div

The constraint div(x,y,z)

ensures that floor(x/y)=z.

For example,

• 10/3 = 3

• (-10)/3 = -4

• 10/(-3) = -4

• (-10)/(-3) = 3

div and mod satisfy together the condition that:

y*(x/y) + x % y = x

The constraint is always false when y = 0

div_undefzero

The constraint div_undefzero(x,y,z)

is the same as div (it ensures that floor(x/y)=z) except the constraint is always true when y = 0, instead of false.

This constraint exists for cases where y being zero should not lead to the whole model being false. If you are unsure what constraint to use, then you probably want the div constraint!

modulo

The constraint modulo(x,y,z) ensures that x%y=z . For negative values, we ensure that:

y(x/y) + x%y = x

For example:

• 3 % 5 = 3

• -3 % 5 = 2

• 3 % -5 = -2

• -3 % -5 = -3

modulo_undefzero

The constraint modulo_undefzero(x,y,z) is the same as modulo except the constraint is always true when y = 0, instead of false.

This constraint exists for cases where y being zero should not lead to the whole model being false. If you are unsure what constraint to use, then you probably want the modulo constraint!

product

The constraint product(x,y,z) ensures that z=x*y in any solution.

This constraint can be used for (and, in fact, has a specialised implementation for) achieving boolean AND, i.e. x & y=z can be modelled as product(x,y,z)

The general constraint achieves bounds consistency for positive numbers.

pow

The constraint pow(x,y,z)

Ensures that x^y=z. This constraint is false when y<0 except for 1^y=1 and (-1)^y=z (where z is 1 if y is even and z is -1 if y is odd).

This constraint is more efficient when x, y and z have positive domains.

sumleq

The constraint sumleq(vec, x) ensures that sum(vec) <= x.

sumgeq

The constraint sumgeq(vec, x) ensures that sum(vec) >= x.

weightedsumleq

The constraint weightedsumleq(constantVec, varVec, total)

ensures that constantVec.varVec <= total, where constantVec.varVec is the scalar dot product of constantVec and varVec.

weightedsumgeq

The constraint weightedsumgeq(constantVec, varVec, total) ensures that constantVec.varVec >= total, where constantVec.varVec is the scalar dot product of constantVec and varVec.

litsumgeq

The constraint litsumgeq(vec1, vec2, c) ensures that there exists at least c distinct indices i such that vec1[i] = vec2[i].

Notes

A SAT clause {x,y,z} can be created using:

litsumgeq([x,y,z],[1,1,1],1)

Note also that this constraint is more efficient for smaller values of c. For large values consider using watchsumleq.

Table constraints

table

An extensional constraint that enforces GAC. The constraint is specified via a list of tuples.

The variables used in the constraint have to be BOOL or DISCRETE variables. Other types are not supported.

To specify a constraint over 3 variables that allows assignments (0,0,0), (1,0,0), (0,1,0) or (0,0,1) do the following.

1. Add a tuplelist to the **TUPLELIST** section, e.g.

**TUPLELIST**
myext 4 3
0 0 0
1 0 0
0 1 0
0 0 1

N.B. the number 4 is the number of tuples in the constraint, the number 3 is the -arity.

2. Add a table constraint to the CONSTRAINTS section, e.g.:

**CONSTRAINTS**
table(myvec, myext)

and now the variables of myvec will satisfy the constraint myext.

The constraints extension can also be specified in the constraint definition, e.g.:

table(myvec, {<0,0,0>,<1,0,0>,<0,1,0>,<0,0,1>})

negativetable

An extensional constraint that enforces GAC. The constraint is specified via a list of disallowed tuples.

See table for how to specify a table constraint in minion input. The only difference for negativetable is that the specified tuples are disallowed.

gacschema

An extensional constraint that enforces GAC. The constraint is specified via a list of tuples.

The format, and usage of gacschema, is identical to the ‘table’ constraint. It is difficult to predict which out of ‘table’ and ‘gacschema’ will be faster for any particular problem.

haggisgac-stable

An extensional constraint that enforces GAC. haggisgac-stable is a variant of haggisgac which uses less memory in some cases, and can also be faster (or slower). The input is identical to haggisgac.

Related constraints

haggisgac

haggisgac

An extensional constraint that enforces GAC. This constraint make uses of ‘short tuples’, which allow some values to be marked as don’t care. When this allows the set of tuples to be reduced in size, this leads to performance gains.

The variables used in the constraint have to be BOOL or DISCRETE variables. Other types are not supported.

Example

Consider the constraint ‘min([x1,x2,x3],x4)’’ on Booleans variables x1,x2,x3,x4.

Represented as a TUPLELIST for a table or gacschema constraint, this would look like:

**TUPLELIST** mycon 8 4
0 0 0 0
0 0 1 0
0 1 0 0
0 1 1 0
1 0 0 0
1 0 1 0
1 1 0 0
1 1 1 1

Short tuples give us a way of shrinking this list. Short tuples consist of pairs (x,y), where x is a variable position, and y is a value for that variable. For example, [(0,0),(3,0)] Represents “if the variable at index 0 is 0, and the variable at index 3 is 0, then the constraint is true”.

This allows us to represent our constraint as follows:

**SHORTTUPLELIST**
mycon 4
[(0,0),(3,0)]
[(1,0),(3,0)]
[(2,0),(3,0)]
[(0,1),(1,1),(2,1),(3,1)]

Note that some tuples are double-represented here. The first 3 short tuples all allow the assignment 0 0 0 0. This is fine. The important thing for efficiency is to try to give a small list of short tuples.

We use this tuple by writing haggisgac([x1,x2,x3,x4], mycon) and now the variables [x1,x2,x3,x4] will satisfy the constraint mycon.

mddc

MDDC (mddc) is an implementation of MDDC(sp) by Cheng and Yap. It enforces GAC on a constraint using a multi-valued decision diagram (MDD).

The MDD required for the propagator is constructed from a set of satisfying tuples. The constraint has the same syntax as ‘table’ and can function as a drop-in replacement.

For examples on how to call it, see the help for ‘table’. Substitute ‘mddc’ for ‘table’. This constraint enforces generalised arc consistency.

negativemddc

Negative MDDC (negativemddc) is an implementation of MDDC(sp) by Cheng and Yap. It enforces GAC on a constraint using a multi-valued decision diagram (MDD).

The MDD required for the propagator is constructed from a set of unsatisfying (negative) tuples. The constraint has the same syntax as ‘negativetable’ and can function as a drop-in replacement. This constraint enforces generalised arc consistency.

lighttable

An extensional constraint that enforces GAC. The constraint is specified via a list of tuples. lighttable is a variant of the table constraint that is stateless and potentially faster for small constraints.

For full documentation, see the help for the table constraint.

shortctuplestr2

This constraint extends the ShortSTR2 algorithm to support short c-tuples (that is, short tuples which can contain more than one domain value per variable).

Example

Input format is similar to that used by other short tuple constraints, such as haggisgac or shortstr2. Refer to the haggisgac and shorttuplelist pages for more information.

The important change is that more than one literal may be given for each variable. Variables which are not mentioned are assumed to be allowed to take any value. For example,

**SHORTTUPLELIST**
mycon 4
[(0,0),(0,1),(3,0)]
[(1,0),(1,2),(3,0)]
[(2,0),(3,0),(3,1)]
[(0,1),(1,1),(2,1),(3,1)]

**CONSTRAINTS**
shortctuplestr2([x1,x2,x3,x4], mycon)

This constraint enforces generalised arc consistency.

shortstr2

ShortSTR2 is the algorithm described in the IJCAI 2013 paper by Jefferson and Nightingale. It is an extension of STR2+ by Christophe Lecoutre, adapted f

Input format is exactly the same as haggisgac. Refer to the haggisgac and shorttuplelist pages for more information.

This constraint enforces generalised arc consistency.

str2plus

str2plus is an implementation of the STR2+ algorithm by Christophe Lecoutre.

str2plus is invoked in the same way as other table constraints, such as table and mddc.

This constraint enforces generalised arc consistency.

Lexicographic Ordering

Lexicographic ordering constraints take two vectors of the same length and compare them lexicographically: the first position at which they differ decides the comparison. They are most often used to break symmetry between two rows or columns of a matrix.

All of these constraints accept the same arguments, and all are correct even if the same variable appears more than once, or appears in both vectors. They differ only in how much propagation they do.

If you are unsure which to use, start with lexleq[quick]. It is the cheapest, and the extra pruning of the others rarely pays for itself; problems posting over 100,000 lexleq[quick] constraints are solved routinely.

lexleq

lexleq(A, B) ensures the vector A is lexicographically less than or equal to the vector B.

With DISCRETE p[3] {0..2} and DISCRETE q[3] {0..2}, lexleq([p[0],p[1],p[2]], [q[0],q[1],q[2]]) allows p = <0,2,1> with q = <1,0,0>, and allows the two vectors to be equal, but forbids p = <1,0,0> with q = <0,2,1>.

This constraint enforces generalised arc consistency when no variable is repeated.

Related constraints

See lexless for the strict version, and lexleq[quick] for a cheaper one.

lexless

lexless(A, B) ensures the vector A is lexicographically strictly less than the vector B. It is identical to lexleq except that the two vectors may not be equal.

This constraint enforces generalised arc consistency when no variable is repeated.

Related constraints

See lexleq for the non-strict version.

lexleq[quick]

lexleq[quick](A, B) is logically identical to lexleq, but does less propagation in exchange for running considerably faster. It does not achieve generalised arc consistency.

This is usually the best choice, especially when a model posts a large number of lexicographic constraints.

Related constraints

See lexleq for the version which achieves GAC.

lexless[quick]

lexless[quick](A, B) is logically identical to lexless, but does less propagation in exchange for running considerably faster. It does not achieve generalised arc consistency.

Related constraints

See lexless for the version which achieves GAC.

lexleq[rv]

lexleq[rv](A, B) is logically identical to lexleq. It achieves generalised arc consistency even when a variable is repeated within or between the two vectors, which plain lexleq does not.

Plain lexleq is still correct with repeated variables – it simply prunes less – so this variant is worth the extra work only when that extra pruning matters. There is no lexless[rv].

Related constraints

See lexleq for the usual version.

Constraints which operate on other Constraints

The input language of Minion is mostly “flat”. There are a number of constraints which do accept other constraints as arguments, which are given in this section.

watched-and

The constraint watched-and({C1,...,Cn}) ensures that the constraints C1,…,Cn are all true.

Conjunctions of constraints may seem pointless, bearing in mind that a CSP is simply a conjunction of constraints already! watched-and is provided to use with other nested constraint, for example in a reification: reify(watched-and({...}),r)

Related constraints

watched-or

watched-or

The constraint watched-or({C1,...,Cn}) ensures that at least one of the constraints C1,…,Cn is true.

Related constraints

watched-and

Reification allows users to set a boolean to be true or false depending on if a constraint is true. All constraints are reifiable and reifyimplyable, except where explicitly stated.

reify

reify(constraint, r) where r is a 0/1 var

ensures that r is set to 1 if and only if constraint is satisfied. That is, if r is 0 the constraint must NOT be satisfied; and if r is 1 it must be satisfied as normal. Conversely, if the constraint is satisfied then r must be 1, and if not then r must be 0.

reifyimply

reifyimply(constraint, r)

checks that if r is set to 1 then constraint must be satisfied. If r is 0, constraint can be true or false.

Minion performs checks to see if constraint will always be false, in which case it sets r to 0.

reifyimply-quick

reifyimply-quick(constraint, r), like reifyimply, checks that if r is set to 1 then constraint must be satisfied. If r is 0, constraint can be true or false. In reifyimply-quick, r is never set to 0 by propagation, instead Minion waits until r is set to 1, and only then imposes that constraint is true.

Changing how much a constraint propagates

The three constraints in this section each wrap one other constraint and do not change what it means: the set of solutions is exactly the same as posting the child constraint on its own. What they change is how much work Minion does to enforce it, and therefore how many search nodes it explores.

All three are specialist tools – normally you should post the child constraint directly and let it use its own propagator, which will be stronger than any of these.

check[assign]

check[assign](constraint) waits until every variable of constraint is assigned, and then checks whether the assignment satisfies it. It never removes a value from any domain.

This is the weakest possible treatment of a constraint: it can only reject a complete assignment, so search must guess its way to the bottom of the tree before anything is detected.

Related constraints

See check[gsa] and forwardchecking for stronger treatments.

check[gsa]

check[gsa](constraint) looks for one assignment satisfying constraint within the current domains, and fails if there is none. When it finds one, it watches it, and looks for another only once that one is destroyed. Like check[assign] it never removes a value from any domain, but unlike check[assign] it can fail before the variables are all assigned.

How early it fails depends on the child constraint, because the search for a satisfying assignment is the child’s own. For example, with domains {5..9}, check[gsa](sumleq([z0,z1],3)) fails immediately at the root, while check[assign] of the same constraint explores the whole tree first.

Related constraints

See check[assign] for the weaker version, and forwardchecking for one which prunes.

forwardchecking

forwardchecking(constraint) performs forward checking on constraint: it waits until at most one variable of the constraint is unassigned, and then removes from that variable every value which cannot be extended to a satisfying assignment.

This is the classical forward-checking algorithm. Unlike the two check constraints it removes values, but it is not simply stronger than them: it does nothing at all until one variable is left, so check[gsa] can fail at the root where forwardchecking has to search. Neither is weaker than the other in general, and both are weaker than the dedicated propagator of essentially every constraint Minion implements.

Related constraints

See check[assign] and check[gsa] for weaker treatments which never prune.

Matrix Constraints

watchsumgeq

The constraint watchsumgeq(vec, c) ensures that sum(vec) >= c, for a list of 0/1 variables vec.

For this constraint, small values of c are more efficient. This is equivalent to litsumgeq(vec, [1,...,1], c), but faster.

Related constraints

watchsumleq litsumgeq

watchsumleq

The constraint watchsumleq(vec, c) ensures that sum(vec) <= c, for a list of 0/1 variables vec.

Equivalent to litsumgeq([vec1,…,vecn], [0,…,0], n-c) but faster for large values of c.

Related constraints

watchsumgeq litsumgeq

hamming

The constraint hamming(X,Y,c) ensures that the hamming distance between X and Y is at least c. That is, that the size of the set {i | X[i] != y[i]} is greater than or equal to c.

not-hamming

The constraint not-hamming(X,Y,c) ensures that the hamming distance between X and Y is less than c. That is, that the size of the set {i | X[i] != y[i]} is strictly less than c.

watchvecneq

The constraint watchvecneq(A, B)

ensures that A and B are not the same vector, i.e., there exists some index i such that A[i] != B[i].

Related constraints

See watchvecexists_less for the same shape of constraint with < in place of !=.

watchvecexists_less

The constraint watchvecexists_less(A, B) ensures that there is some index i at which A[i] < B[i].

The two vectors must be the same length. Note that this is an existential condition on the pairs, not a lexicographic comparison: it asks only that A is smaller than B somewhere, and says nothing about the other positions. For example, with A = <1,0> and B = <0,1> the constraint is satisfied, because A[1] < B[1], even though A is lexicographically greater than B.

Related constraints

See watchvecneq for the != version, and lexless if you want a lexicographic comparison.

frameupdate

frameupdate(source, target, idx_source, idx_target, blocksize) relates two equal-length vectors which are each divided into consecutive blocks of blocksize variables. It says that if you delete the blocks of source listed in idx_source, and delete the blocks of target listed in idx_target, the two sequences of blocks that remain are equal, block by block and in order.

Block indices count from 1, and the values within each index vector must be distinct. An index is accepted up to the length of the vector rather than the number of blocks, so with source[4] and blocksize 2, indices 3 and 4 are allowed even though there are only two blocks; an index past the last block names nothing and deletes nothing. source and target must be the same length, and that length must be divisible by blocksize; both are checked when the constraint is built.

The intended use is to model one step of a planning problem, where source and target are consecutive states, and the two index vectors say which blocks the step removes and which it adds. Everything else must be carried over unchanged – the “frame” of the update.

Constant constraints

true

The constraint true takes no arguments and is always satisfied.

false

The constraint false takes no arguments and is never satisfied. It can be used to explicitly mark a model as unsatisfiable.

Unary constraints

The following unary constraints have two practical applications:

• They can be used with DISCRETE and BOUND variables, to remove values from their initial domains.

• They are used in watched-or, and related constraints, to build up more complex conditions.

w-inrange

The constraint w-inrange(x, [a,b]) ensures that a <= x <= b.

w-notinrange

The constraint w-notinrange(x, [a,b]) ensures that x < a or b < x.

w-inset

The constraint w-inset(x, [a1,…,an]) ensures that x belongs to the set {a1,..,an}.

w-notinset

The constraint w-notinset(x, [a1,…,an]) ensures that x does not belong to the set {a1,..,an}.

w-literal

The constraint w-literal(x, a) ensures that x=a.

w-notliteral

The constraint w-notliteral(x, a) ensures that x =/= a.

w-inintervalset

The constraint w-inintervalset(x, [a1,a2, b1,b2, … ]) ensures that the value of x belongs to one of the intervals {a1,…,a2}, {b1,…,b2} etc. The list of intervals must be given in numerical order.

There is no w-notinintervalset, as this constraint can be expressed using w-inintervalset.