A.7 clpfd.pl -- Constraint Logic Programming over Finite Domains

author
Markus Triska

Constraint programming is a declarative formalism that lets you describe conditions a solution should satisfy. This library provides CLP(FD), Constraint Logic Programming over Finite Domains. It can be used to model and solve various combinatorial problems from diverse areas such as planning, scheduling, and graph colouring.

As an example, consider the cryptoarithmetic puzzle SEND + MORE = MONEY, where different letters denote distinct integers between 0 and 9. It can be modeled in CLP(FD) as follows:

:- use_module(library(clpfd)).

puzzle([S,E,N,D] + [M,O,R,E] = [M,O,N,E,Y]) :-
        Vars = [S,E,N,D,M,O,R,Y], Vars ins 0..9,
        all_different(Vars),
                  S*1000 + E*100 + N*10 + D +
                  M*1000 + O*100 + R*10 + E #=
        M*10000 + O*1000 + N*100 + E*10 + Y,
        M #> 0, S #> 0,
        label(Vars).

?- puzzle(P).
P = ([9, 5, 6, 7]+[1, 0, 8, 5]=[1, 0, 6, 5, 2])

Most predicates of this library are constraints: They generalise arithmetic evaluation of integer expressions in that propagation can proceed in all directions. This library also provides enumeration predicates, which let you systematically search for solutions on variables whose domains have become finite. A finite domain expression is one of:

an integerGiven value
a variableUnknown value
-ExprUnary minus
Expr + ExprAddition
Expr * ExprMultiplication
Expr - Expr.Subtraction
min(Expr,Expr)Minimum of two expressions
max(Expr,Expr)Maximum of two expressions
Expr mod ExprRemainder of integer division
abs(Expr)Absolute value
Expr / ExprInteger division

The most important finite domain constraints are given in the table below.

Expr1 #>= Expr2Expr1 is larger than or equal to Expr2
Expr1 #=< Expr2Expr1 is smaller than or equal to Expr2
Expr1 #= Expr2Expr1 equals Expr2
Expr1 #\= Expr2Expr1 is not equal to Expr2
Expr1 #> Expr2Expr1 is strictly larger than Expr2
Expr1 #< Expr2Expr1 is strictly smaller than Expr2

The constraints #=/2, #\=/2, #</2, #>/2, #=</2, #>=/2 and #\/1 can be reified, which means reflecting their truth values into Boolean 0/1 variables. Let P and Q denote conjunctions (#/\/2) or disjunctions (#\//2) of reifiable constraints or Boolean variables, then:

#\ QTrue iff Q is false
P #<==> QTrue iff P and Q are equivalent
P #==> QTrue iff P implies Q
P #<== QTrue iff Q implies P

If SWI Prolog is compiled with support for arbitrary precision integers (using GMP), there is no limit on the size of domains.

+Var in +Domain
Constrain Var to elements of Domain. Domain is one of:
Lower .. Upper
All integers I such that Lower =< I =< Upper. The atoms inf and sup denote negative and positive infinity, respectively.
Domain1 \/ Domain2
The union of Domain1 and Domain2.
?Vars ins +Domain
Constrain the variables or integers in Vars to Domain.
indomain(?Var)
Bind Var to all feasible values of its domain on backtracking. The domain of Var must be finite.
label(+Vars)
Equivalent to labeling([], Vars).
labeling(+Options, +Vars)
Labeling means systematically trying out values for the finite domain variables Vars until all of them are ground. The domain of each variable in Vars must be finite. Options is a list of options that let you exhibit some control over the search process. Two sets of options exist: One for variable selection strategy, and one for optimisation. The variable selection strategy lets you specify which variable should be labeled next and is one of:
leftmost
Label the variables in the order they occur in Vars. This is the default.
ff
First fail. Label the leftmost variable with smallest domain next, in order to detect infeasibility early. This is often a good strategy.
min
Label the leftmost variable whose lower bound is the lowest next.
max
Label the leftmost variable whose upper bound is the highest next.

The second set of options lets you influence the order of solutions:

min(Expr)
max(Expr)

This generates solutions in ascending/descending order with respect to the evaluation of the arithmetic expression Expr. All variables of Expr must also be contained in Vars.

If more than one option of a category is specified, the one occurring rightmost in the option list takes precedence over all others of that category. Labeling is always complete and always terminates.

all_different(+Vars)
Constrain Vars to be pairwise distinct.
sum(+Vars, +Op, +Expr)
Constrain the sum of a list. The sum/3 constraint demands that "sumlist(Vars) Op Expr" hold, e.g.:
        sum(List, #=< 100)
?X #>= ?Y
X is greater than or equal to Y.
?X #=< ?Y
X is less than or equal to Y.
?X #= ?Y
X equals Y.
?X #\= ?Y
X is not Y.
?X #> ?Y
X is greater than Y.
?X #< ?Y
X is less than Y.
#\ +Q
The reifiable constraint Q does not hold.
?P #<==> ?Q
P and Q are equivalent.
?P #==> ?Q
P implies Q.
?P #<== ?Q
?Q implies ?P.
?P #/\ ?Q
P and Q hold.
?P #\/ ?Q
P or Q holds.
lex_chain(+Lists)
Constrains Lists to be lexicographically non-decreasing.
tuples_in(+Tuples, +Relation)
Relation is a list of ground lists of integers. Tuples is a list of lists containing integers and finite domain variables. Tuples are constrained to be elements of Relation.
all_distinct(+Ls)
Like all_different/1, with stronger propagation.
serialized(+Starts, +Durations)
Constrain a set of intervals to a non-overlapping sequence. Starts = [S_1,...,S_n], is a list of variables or integers, Durations = [D_1,...,D_n] is a list of non-negative integers. Constrains Starts and Durations to denote a set of non-overlapping tasks, i.e.: S_i + D_i =< S_j or S_j + D_j =< S_i for all 1 =< i < j =< n.
See also
Dorndorf et al. 2000, "Constraint Propagation Techniques for the Disjunctive Scheduling Problem"