Built-in Constraints

8.4 Built-in Constraints

The following section summarises the built-in constraint predicates of the ic library.

Vars :: Domain
Constrains Vars to take only integer or real values from the domain specified by Domain. Vars may be a variable, a list, or a submatrix (e.g. M[1..4, 3..6]); for a list or a submatrix, the domain is applied recursively so that one can apply a domain to, for instance, a list of lists of variables. Domain can be specified as a simple range Lo .. Hi, or as a list of subranges and/or individual elements (integer variables only). The type of the bounds determines the type of the variable (real or integer). Also allowed are the (untyped) symbolic bound values inf, +inf and -inf.
Vars $:: Domain
Like ::/2, but for declaring real variables (i.e. it never imposes integrality, regardless of the types of the bounds).
Vars #:: Domain
Like ::/2, but for declaring integer variables.
reals(Vars)
Declares that the variables are IC variables (like declaring Vars :: -inf..inf).
integers(Vars)
Constrains the given variables to take integer values only.

Figure 8.1: Domain constraints

The most common way to declare an IC variable is to use the ::/2 predicate (or $::/2 or #::/2) to give it an initial domain:

?- X :: -10 .. 10.
X = X{-10 .. 10}
Yes

?- X :: -10.0 .. 10.0.
X = X{-10.0 .. 10.0}
Yes

?- X #:: -10 .. 10.
X = X{-10 .. 10}
Yes

?- X $:: -10 .. 10.
X = X{-10.0 .. 10.0}
Yes

?- X :: 0 .. 1.0Inf.
X = X{0 .. 1.0Inf}
Yes

?- X :: 0.0 .. 1.0Inf.
X = X{0.0 .. 1.0Inf}
Yes

?- X :: [1, 4 .. 6, 9, 10].
X = X{[1, 4 .. 6, 9, 10]}
Yes

Note that for ::/2 the type of the bounds defines the type of the variable (integer or real) but that infinities are considered type-neutral. To just declare the type of a variable without restricting the domain at all, one can use the integers/1 and reals/1 .

The final way to declare that a variable is an IC variable is to just use it in an IC constraint: this performs an implicit declaration.

ExprX #= ExprY
ExprX is equal to ExprY. ExprX and ExprY are integer expressions, and the variables and subexpressions are constrained to be integers.
ExprX #>= ExprY
ExprX is greater than or equal to ExprY. ExprX and ExprY are integer expressions, and the variables and subexpressions are constrained to be integers.
ExprX #=< ExprY
ExprX is less than or equal to ExprY. ExprX and ExprY are integer expressions, and the variables and subexpressions are constrained to be integers.
ExprX #> ExprY
ExprX is greater than ExprY. ExprX and ExprY are integer expressions, and the variables and subexpressions are constrained to be integers.
ExprX #< ExprY
ExprX is less than ExprY. ExprX and ExprY are integer expressions, and the variables and subexpressions are constrained to be integers.
ExprX #\= ExprY
ExprX is not equal to ExprY. ExprX and ExprY are integer expressions, and the variables are constrained to be integers.
ac_eq(X, Y, C)
Arc-consistent implementation of X #= Y + C. X and Y are constrained to be integer variables and to have “reasonable” bounds. C must be an integer.

Figure 8.2: Integral Arithmetic constraints

ExprX $= ExprY
ExprX is equal to ExprY. ExprX and ExprY are general expressions.
ExprX $>= ExprY
ExprX is greater than or equal to ExprY. ExprX and ExprY are general expressions.
ExprX $=< ExprY
ExprX is less than or equal to ExprY. ExprX and ExprY are general expressions.
ExprX $> ExprY
ExprX is greater than ExprY. ExprX and ExprY are general expressions.
ExprX $< ExprY
ExprX is less than ExprY. ExprX and ExprY are general expressions.
ExprX $\= ExprY
ExprX is not equal to ExprY. ExprX and ExprY are general expressions.

Figure 8.3: Non-Integral Arithmetic Constraints

The basic IC relational constraints come in two forms. The first form is for integer-only constraints, and is summarised in Figure 8.2. All of these constraints contain # in their name, which indicates that all numbers appearing in them must be integers, and all variables and subexpressions will be constrained to be integral. It is important to note that subexpressions are constrained to be integral, because it means, for instance, that X/2 + Y/2 #= 1 and X + Y #= 2 are different constraints, since the former constrains X and Y to be even.

The second form is the general form of the constraints, and is summarised in Figure 8.3. These constraints can be used with either integer or real variables and numbers. With the exception of integrality issues, the two versions of each constraint are equivalent. Thus if the constants are integers and the variables and subexpressions are integral, the two forms may be used interchangeably.

Most of the basic constraints operate by propagating bound information (performing interval reasoning). The exceptions are the disequality (not equals) constraints and the ac_eq/3 constraint, which perform domain reasoning (arc consistency). An example:

?- [X, Y] :: 0 .. 10, X #>= Y + 2.
X = X{2 .. 10}
Y = Y{0 .. 8}
There is 1 delayed goal.
Yes

In the above example, since the lower bound of Y is 0 and X must be at least 2 greater, the lower bound of X has been updated to 2. Similarly, the upper bound of Y has been reduced to 8. The delayed goal indicates that the constraint is still active: there are still some combinations of values for X and Y which violate the constraint, so the constraint remains until it is sure that no such violation is possible.

Note that if a domain ever becomes empty as the result of propagation (no value for the variable is feasible) then the constraint must necessarily have been violated, and the computation backtracks.

For a disequality constraint, no deductions can be made until there is only one variable left, at which point (if it is an integer variable) the variable’s domain can be updated to exclude the relevant value:

?- X :: 0 .. 10, X #\= 3.
X = X{[0 .. 2, 4 .. 10]}
Yes

?- [X, Y] :: 0 .. 10, X - Y #\= 3.
X = X{0 .. 10}
Y = Y{0 .. 10}
There is 1 delayed goal.
Yes

?- [X, Y] :: 0 .. 10, X - Y #\= 3, Y = 2.
X = X{[0 .. 4, 6 .. 10]}
Y = 2
Yes

For the ac_eq/3 constraint, “holes” in the domain of one variable are propagated to the other:

?- [X, Y] :: 0 .. 10, ac_eq(X, Y, 3).
X = X{3 .. 10}
Y = Y{0 .. 7}
There is 1 delayed goal.
Yes

?- [X, Y] :: 0 .. 10, ac_eq(X, Y, 3), Y #\= 4.
X = X{[3 .. 6, 8 .. 10]}
Y = Y{[0 .. 3, 5 .. 7]}
There is 1 delayed goal.
Yes

Compare with the corresponding bounds consistency constraint:

?- [X, Y] :: 0 .. 10, X #= Y + 3, Y #\= 4.
X = X{3 .. 10}
Y = Y{[0 .. 3, 5 .. 7]}
There is 1 delayed goal.
Yes

⊙: IC supports a range of mathematical operators beyond the basic +/2, -/2, */2, etc. See the IC chapter in the Constraint Library Manual for full details.

⊗: If one wishes to construct an expression to use in an IC constraint at run time, then one must wrap it in eval/1:

?- [X, Y] :: 0..10, Expr = X + Y, Sum #= Expr.
number expected in set_up_ic_con(7, 1, [0 * 1, 1 * Sum{-1.0Inf .. 1.0Inf}, -1 * (X{0 .. 10} + Y{0 .. 10})])
Abort

?- [X, Y] :: 0..10, Expr = X + Y, Sum #= eval(Expr).
X = X{0 .. 10}
Y = Y{0 .. 10}
Sum = Sum{0 .. 20}
Expr = X{0 .. 10} + Y{0 .. 10}
There is 1 delayed goal.
Yes

Reification provides access to the logical truth of a constraint expression and can be used by:

The ECLⁱPS^e system to infer the truth value, reflecting the value into a variable.
The programmer to enforce the constraint or its negation by giving a value to the truth variable.

This logical truth value is a boolean variable (domain 0..1), where the value 1 means the constraint is or is required to be true, and the value 0 means the constraint is or is required to be false.

When constraints appear in an expression context, they evaluate to their reified truth value. Practically, this means that the constraints are posted in a passive check but do not propagate mode. In this mode no variable domains are modified but checks are made to determine whether the constraint has become entailed (necessarily true) or disentailed (necessarily false).

The simplest and arguably most natural way to reify a constraint is to place it in an expression context (i.e. on either side of a $=, #=, etc.) and assign its truth value to a variable. For example:

?- X :: 0 .. 10, TruthValue $= (X $> 4).
TruthValue = TruthValue{[0, 1]}
X = X{0 .. 10}
There is 1 delayed goal.
Yes

?- X :: 6 .. 10, TruthValue $= (X $> 4).
TruthValue = 1
X = X{6 .. 10}
Yes

?- X :: 0 .. 4, TruthValue $= (X $> 4).
TruthValue = 0
X = X{0 .. 4}
Yes

All the basic relational constraint predicates also come in a three-argument form where the third argument is the reified truth value, and this form can also be used to reify a constraint directly. For example:

?- X :: 0 .. 10, $>(X, 4, TruthValue).
X = X{0 .. 10}
TruthValue = TruthValue{[0, 1]}
There is 1 delayed goal.
Yes

As noted above the boolean truth variable corresponding to a constraint can also be used to enforce the constraint (or its negation):

?- X :: 0 .. 10, TruthValue $= (X $> 4), TruthValue = 1.
X = X{5 .. 10}
TruthValue = 1
Yes

?- X :: 0 .. 10, TruthValue $= (X $> 4), TruthValue = 0.
X = X{0 .. 4}
TruthValue = 0
Yes

By instantiating the value of the reified truth variable, the constraint changes from being passive to being active. Once actively true (or actively false) the constraint will prune domains as though it had been posted as a simple non-reified constraint.

⊙: Additional information on reified constraints can be found in the ECLⁱPS^e Constraint Library Manual that documents IC: A Hybrid Finite Domain / Real Number Interval Constraint Solver.

and
Constraint conjunction. e.g. X $> 3 and X $< 8
or
Constraint disjunction. e.g. X $< 3 or X $> 8
=>
Constraint implication. e.g. X $> 3 => Y $< 8
neg
Constraint negation. e.g. neg X $> 3

Figure 8.4: Constraint Expression Connectives

IC also provides a number of connectives useful for combining constraint expressions. These are summarised in Figure 8.4. For example:

?- [X, Y] :: 0 .. 10, X #>= Y + 6 or X #=< Y - 6.
X = X{0 .. 10}
Y = Y{0 .. 10}
There are 3 delayed goals.
Yes

?- [X, Y] :: 0 .. 10, X #>= Y + 6 or X #=< Y - 6, X #>= 5.
Y = Y{0 .. 4}
X = X{6 .. 10}
There is 1 delayed goal.
Yes

In the above example, once it is known that X #=< Y - 6 cannot be true, the constraint X #>= Y + 6 is enforced.

Note that these connectives exploit constraint reification, and actually just reason about boolean variables. This means that they can be used as boolean constraints as well:

?- A => B.
A = A{[0, 1]}
B = B{[0, 1]}
There is 1 delayed goal.
Yes

?- A => B, A = 1.
B = 1
A = 1
Yes

?- A => B, A = 0.
B = B{[0, 1]}
A = 0
Yes