Constraint programming is a declarative formalism that lets you state relations between terms. This library provides CLP(FD), Constraint Logic Programming over Finite Domains.
There are two major use cases of this library:
When teaching Prolog, we strongly recommend that you introduce CLP(FD) constraints before explaining lower-level arithmetic predicates and their procedural idiosyncrasies. This is because constraints are easy to explain, understand and use due to their purely relational nature. In contrast, the modedness and directionality of low-level arithmetic primitives are non-declarative limitations that are better deferred to more advanced lectures.
If you are used to the complicated operational considerations that low-level arithmetic primitives necessitate, then moving to CLP(FD) constraints may, due to their power and convenience, at first feel to you excessive and almost like cheating. It isn't. Constraints are an integral part of many Prolog systems and are available to help you eliminate and avoid, as far as possible, the use of lower-level and less general primitives by providing declarative alternatives that are meant to be used instead.
For satisfactory performance, arithmetic constraints are implicitly rewritten at compilation time so that lower-level fallback predicates are automatically used whenever possible.
You can cite this library in your publications as:
@inproceedings{Triska12, author = {Markus Triska}, title = {The Finite Domain Constraint Solver of {SWI-Prolog}}, booktitle = {FLOPS}, series = {LNCS}, volume = {7294}, year = {2012}, pages = {307-316} }
A finite domain arithmetic expression is one of:
integer Given value variable Unknown integer ?(variable) Unknown integer -Expr Unary minus Expr + Expr Addition Expr * Expr Multiplication Expr - Expr Subtraction Expr ^
ExprExponentiation min(Expr,Expr)
Minimum of two expressions max(Expr,Expr)
Maximum of two expressions Expr mod Expr Modulo induced by floored division Expr rem Expr Modulo induced by truncated division abs(Expr)
Absolute value Expr //
ExprTruncated integer division
Arithmetic constraints are relations between arithmetic expressions.
The most important arithmetic constraints are:
Expr1 #>=
Expr2Expr1 is greater than or equal to Expr2 Expr1 #=<
Expr2Expr1 is less than or equal to Expr2 Expr1 #=
Expr2Expr1 equals Expr2 Expr1 #\=
Expr2Expr1 is not equal to Expr2 Expr1 #>
Expr2Expr1 is greater than Expr2 Expr1 #<
Expr2Expr1 is less than Expr2
CLP(FD) constraints let you declaratively express integer arithmetic. The CLP(FD) constraints #=/2, #>/2 etc. are meant to be used instead of the corresponding primitives is/2, =:=/2, >/2 etc.
An important advantage of arithmetic constraints is their purely relational nature. They are therefore easy to explain and use, and well suited for beginners and experienced Prolog programmers alike.
Consider for example the query:
?- X #> 3, X #= 5 + 2. X = 7.
In contrast, when using low-level integer arithmetic, we get:
?- X > 3, X is 5 + 2. ERROR: >/2: Arguments are not sufficiently instantiated
Due to the necessary operational considerations, the use of these low-level arithmetic predicates is considerably harder to understand and should therefore be deferred to more advanced lectures.
For supported expressions, CLP(FD) constraints are drop-in replacements of these low-level arithmetic predicates, often yielding more general programs.
Here is an example:
:- use_module(library(clpfd)). n_factorial(0, 1). n_factorial(N, F) :- N #> 0, N1 #= N - 1, F #= N * F1, n_factorial(N1, F1).
This predicate can be used in all directions. For example:
?- n_factorial(47, F). F = 258623241511168180642964355153611979969197632389120000000000 ; false. ?- n_factorial(N, 1). N = 0 ; N = 1 ; false. ?- n_factorial(N, 3). false.
To make the predicate terminate if any argument is instantiated, add
the (implied) constraint F #\=
0 before the recursive call.
Otherwise, the query n_factorial(N, 0)
is the only
non-terminating case of this kind.
This library uses goal_expansion/2
to automatically rewrite arithmetic constraints at compilation time. The
expansion's aim is to bring the performance of arithmetic constraints
close to that of lower-level arithmetic predicates whenever possible. To
disable the expansion, set the flag clpfd_goal_expansion
to false
.
The constraints in/2, #=/2, #\=/2, #</2, #>/2, #=</2, and #>=/2 can be reified, which means reflecting their truth values into Boolean values represented by the integers 0 and 1. Let P and Q denote reifiable constraints or Boolean variables, then:
#\
QTrue iff Q is false P #\/
QTrue iff either P or Q P #/\
QTrue iff both P and Q P #\
QTrue iff either P or Q, but not both P #<==>
QTrue iff P and Q are equivalent P #==>
QTrue iff P implies Q P #<==
QTrue iff Q implies P
The constraints of this table are reifiable as well.
Each CLP(FD) variable has an associated set of admissible integers which we call the variable's domain. Initially, the domain of each CLP(FD) variable is the set of all integers. The constraints in/2 and ins/2 are the primary means to specify tighter domains of variables.
Here are example queries and the system's declaratively equivalent answers:
?- X in 100..sup. X in 100..sup. ?- X in 1..5 \/ 3..12. X in 1..12. ?- [X,Y,Z] ins 0..3. X in 0..3, Y in 0..3, Z in 0..3.
Domains are taken into account when further constraints are stated, and by enumeration predicates like labeling/2.
Here is an example session with a few queries and their answers:
?- use_module(library(clpfd)). % library(clpfd) compiled into clpfd 0.06 sec, 633,732 bytes true. ?- X #> 3. X in 4..sup. ?- X #\= 20. X in inf..19\/21..sup. ?- 2*X #= 10. X = 5. ?- X*X #= 144. X in -12\/12. ?- 4*X + 2*Y #= 24, X + Y #= 9, [X,Y] ins 0..sup. X = 3, Y = 6. ?- X #= Y #<==> B, X in 0..3, Y in 4..5. B = 0, X in 0..3, Y in 4..5.
In each case, and as for all pure programs, the answer is declaratively equivalent to the original query, and in many cases the constraint solver has deduced additional domain restrictions.
In addition to being declarative replacements for low-level arithmetic predicates, CLP(FD) constraints are also often used to solve combinatorial problems such as planning, scheduling and allocation tasks. To let you conveniently model and solve such problems, this library provides several constraints beyond typical integer arithmetic, such as all_distinct/1, global_cardinality/2 and cumulative/1.
Using CLP(FD) constraints to solve combinatorial tasks typically consists of two phases:
It is good practice to keep the modeling part, via a dedicated predicate, separate from the actual search for solutions. This lets you observe termination and determinism properties of the modeling part in isolation from the search, and more easily try different search strategies.
As an example of a constraint satisfaction problem, 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.
Notice that we are not using labeling/2 in this predicate, so that we can first execute and observe the modeling part in isolation. Sample query and its result (actual variables replaced for readability):
?- puzzle(As+Bs=Cs). As = [9, A2, A3, A4], Bs = [1, 0, B3, A2], Cs = [1, 0, A3, A2, C5], A2 in 4..7, all_different([9, A2, A3, A4, 1, 0, B3, C5]), 91*A2+A4+10*B3#=90*A3+C5, A3 in 5..8, A4 in 2..8, B3 in 2..8, C5 in 2..8.
From this answer, we see that the modeling part terminates and is in fact deterministic. Moreover, we see from the residual goals that the constraint solver has deduced more stringent bounds for all variables. Such observations are only possible if modeling and search parts are cleanly separated.
Labeling can then be used to search for solutions in a separate predicate or goal:
?- puzzle(As+Bs=Cs), label(As). As = [9, 5, 6, 7], Bs = [1, 0, 8, 5], Cs = [1, 0, 6, 5, 2] ; false.
In this case, it suffices to label a subset of variables to find the puzzle's unique solution, since the constraint solver is strong enough to reduce the domains of remaining variables to singleton sets. In general though, it is necessary to label all variables to obtain ground solutions.
If you set the flag clpfd_monotonic
to true
,
then CLP(FD) is monotonic: Adding new constraints cannot yield new
solutions. When this flag is true
, you must wrap variables
that occur in arithmetic expressions with the functor (?)/1
.
For example, ?(X) #= ?(Y) + ?(Z)
. The wrapper can be
omitted for variables that are already constrained to integers.
Use call_residue_vars/2 and copy_term/3 to inspect residual goals and the constraints in which a variable is involved. This library also provides reflection predicates (like fd_dom/2, fd_size/2 etc.) with which you can inspect a variable's current domain. These predicates can be useful if you want to implement your own labeling strategies.
You can also define custom constraints. The mechanism to do this is
not yet finalised, and we welcome suggestions and descriptions of use
cases that are important to you. As an example of how it can be done
currently, let us define a new custom constraint oneground(X,Y,Z)
,
where Z shall be 1 if at least one of X and Y is instantiated:
:- use_module(library(clpfd)). :- multifile clpfd:run_propagator/2. oneground(X, Y, Z) :- clpfd:make_propagator(oneground(X, Y, Z), Prop), clpfd:init_propagator(X, Prop), clpfd:init_propagator(Y, Prop), clpfd:trigger_once(Prop). clpfd:run_propagator(oneground(X, Y, Z), MState) :- ( integer(X) -> clpfd:kill(MState), Z = 1 ; integer(Y) -> clpfd:kill(MState), Z = 1 ; true ).
First, clpfd:make_propagator/2 is used to transform a user-defined representation of the new constraint to an internal form. With clpfd:init_propagator/2, this internal form is then attached to X and Y. From now on, the propagator will be invoked whenever the domains of X or Y are changed. Then, clpfd:trigger_once/1 is used to give the propagator its first chance for propagation even though the variables' domains have not yet changed. Finally, clpfd:run_propagator/2 is extended to define the actual propagator. As explained, this predicate is automatically called by the constraint solver. The first argument is the user-defined representation of the constraint as used in clpfd:make_propagator/2, and the second argument is a mutable state that can be used to prevent further invocations of the propagator when the constraint has become entailed, by using clpfd:kill/1. An example of using the new constraint:
?- oneground(X, Y, Z), Y = 5. Y = 5, Z = 1, X in inf..sup.
=<
I =<
Upper.
Lower must be an integer or the atom inf, which
denotes negative infinity. Upper must be an integer or
the atom sup, which denotes positive infinity.
\/
Domain2labeling([], Vars)
.The variable selection strategy lets you specify which variable of Vars is labeled next and is one of:
The value order is one of:
The branching strategy is one of:
#\=
V, where V is determined by the value ordering options. This is the
default.
#=<
M
and X #>
M, where M is the midpoint of the domain of X.
At most one option of each category can be specified, and an option must not occur repeatedly.
The order of solutions can be influenced with:
min(Expr)
max(Expr)
This generates solutions in ascending/descending order with respect to the evaluation of the arithmetic expression Expr. Labeling Vars must make Expr ground. If several such options are specified, they are interpreted from left to right, e.g.:
?- [X,Y] ins 10..20, labeling([max(X),min(Y)],[X,Y]).
This generates solutions in descending order of X, and for each
binding of X, solutions are generated in ascending order of Y. To obtain
the incomplete behaviour that other systems exhibit with "maximize(Expr)
"
and "minimize(Expr)
", use once/1,
e.g.:
once(labeling([max(Expr)], Vars))
Labeling is always complete, always terminates, and yields no redundant solutions.
?- maplist(in, Vs, [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]), all_distinct(Vs). false.
\
=, #<, #>, #=<
or #>=. For example:
?- [A,B,C] ins 0..sup, sum([A,B,C], #=, 100). A in 0..100, A+B+C#=100, B in 0..100, C in 0..100.
\
=, #<, #>, #=<
or #>=.?- Vs = [A,B,C,D], Vs ins 1..4, all_different(Vs), A #< B, C #< D, A #< C, findall(pair(A,B)-pair(C,D), label(Vs), Ms). Ms = [ pair(1, 2)-pair(3, 4), pair(1, 3)-pair(2, 4), pair(1, 4)-pair(2, 3)].
?- #\ X in -3..0\/10..80. X in inf.. -4\/1..9\/81..sup.
?- X #= 4 #<==> B, X #\= 4. B = 0, X in inf..3\/5..sup.
The following example uses reified constraints to relate a list of finite domain variables to the number of occurrences of a given value:
:- use_module(library(clpfd)). vs_n_num(Vs, N, Num) :- maplist(eq_b(N), Vs, Bs), sum(Bs, #=, Num). eq_b(X, Y, B) :- X #= Y #<==> B.
Sample queries and their results:
?- Vs = [X,Y,Z], Vs ins 0..1, vs_n_num(Vs, 4, Num). Vs = [X, Y, Z], Num = 0, X in 0..1, Y in 0..1, Z in 0..1. ?- vs_n_num([X,Y,Z], 2, 3). X = 2, Y = 2, Z = 2.
?- findall(N, (N mod 3 #= 0 #\/ N mod 5 #= 0, N in 0..999, indomain(N)), Ns), sum(Ns, #=, Sum). Ns = [0, 3, 5, 6, 9, 10, 12, 15, 18|...], Sum = 233168.
?- tuples_in([[X,Y]], [[1,2],[1,5],[4,0],[4,3]]), X = 4. X = 4, Y in 0\/3.
As another example, consider a train schedule represented as a list of quadruples, denoting departure and arrival places and times for each train. In the following program, Ps is a feasible journey of length 3 from A to D via trains that are part of the given schedule.
:- use_module(library(clpfd)). trains([[1,2,0,1], [2,3,4,5], [2,3,0,1], [3,4,5,6], [3,4,2,3], [3,4,8,9]]). threepath(A, D, Ps) :- Ps = [[A,B,_T0,T1],[B,C,T2,T3],[C,D,T4,_T5]], T2 #> T1, T4 #> T3, trains(Ts), tuples_in(Ps, Ts).
In this example, the unique solution is found without labeling:
?- threepath(1, 4, Ps). Ps = [[1, 2, 0, 1], [2, 3, 4, 5], [3, 4, 8, 9]].
=<
S_j or S_j +
D_j =<
S_i for all 1 =<
i <
j =<
n. Example:
?- length(Vs, 3), Vs ins 0..3, serialized(Vs, [1,2,3]), label(Vs). Vs = [0, 1, 3] ; Vs = [2, 0, 3] ; false.
global_cardinality(Vs, Pairs, [])
. Example:
?- Vs = [_,_,_], global_cardinality(Vs, [1-2,3-_]), label(Vs). Vs = [1, 1, 3] ; Vs = [1, 3, 1] ; Vs = [3, 1, 1].
?- length(Vs, _), circuit(Vs), label(Vs). Vs = [] ; Vs = [1] ; Vs = [2, 1] ; Vs = [2, 3, 1] ; Vs = [3, 1, 2] ; Vs = [2, 3, 4, 1] .
cumulative(Tasks, [limit(1)])
.task(S_i, D_i, E_i, C_i, T_i)
. S_i denotes
the start time, D_i the positive duration, E_i the end time, C_i the
non-negative resource consumption, and T_i the task identifier. Each of
these arguments must be a finite domain variable with bounded domain, or
an integer. The constraint holds iff at each time slot during the start
and end of each task, the total resource consumption of all tasks
running at that time does not exceed the global resource limit (which is
1 by default). Options is a list of options. Currently, the
only supported option is:
For example, given the following predicate that relates three tasks of durations 2 and 3 to a list containing their starting times:
tasks_starts(Tasks, [S1,S2,S3]) :- Tasks = [task(S1,3,_,1,_), task(S2,2,_,1,_), task(S3,2,_,1,_)].
We can use cumulative/2 as follows, and obtain a schedule:
?- tasks_starts(Tasks, Starts), Starts ins 0..10, cumulative(Tasks, [limit(2)]), label(Starts). Tasks = [task(0, 3, 3, 1, _G36), task(0, 2, 2, 1, _G45), ...], Starts = [0, 0, 2] .
automaton(_, _, Signature, Nodes, Arcs, [], [], _)
,
a common use case of automaton/8.
In the following example, a list of binary finite domain variables is
constrained to contain at least two consecutive ones:
:- use_module(library(clpfd)). two_consecutive_ones(Vs) :- automaton(Vs, [source(a),sink(c)], [arc(a,0,a), arc(a,1,b), arc(b,0,a), arc(b,1,c), arc(c,0,c), arc(c,1,c)]).
Example query:
?- length(Vs, 3), two_consecutive_ones(Vs), label(Vs). Vs = [0, 1, 1] ; Vs = [1, 1, 0] ; Vs = [1, 1, 1].
source(Node)
and sink(Node)
terms. Arcs
is a list of
arc(Node,Integer,Node)
and arc(Node,Integer,Node,Exprs)
terms that denote the automaton's transitions. Each node is represented
by an arbitrary term. Transitions that are not mentioned go to an
implicit failure node. Exprs is a list of arithmetic
expressions, of the same length as Counters. In each
expression, variables occurring in Counters correspond to old
counter values, and variables occurring in Template
correspond to the current element of Sequence. When a
transition containing expressions is taken, each counter is updated as
stated by the result of the corresponding arithmetic expression. By
default, counters remain unchanged. Counters is a list of
variables that must not occur anywhere outside of the constraint goal. Initials
is a list of the same length as Counters. Counter arithmetic
on the transitions relates the counter values in Initials to Finals.
The following example is taken from Beldiceanu, Carlsson, Debruyne and Petit: "Reformulation of Global Constraints Based on Constraints Checkers", Constraints 10(4), pp 339-362 (2005). It relates a sequence of integers and finite domain variables to its number of inflexions, which are switches between strictly ascending and strictly descending subsequences:
:- use_module(library(clpfd)). sequence_inflexions(Vs, N) :- variables_signature(Vs, Sigs), automaton(_, _, Sigs, [source(s),sink(i),sink(j),sink(s)], [arc(s,0,s), arc(s,1,j), arc(s,2,i), arc(i,0,i), arc(i,1,j,[C+1]), arc(i,2,i), arc(j,0,j), arc(j,1,j), arc(j,2,i,[C+1])], [C], [0], [N]). variables_signature([], []). variables_signature([V|Vs], Sigs) :- variables_signature_(Vs, V, Sigs). variables_signature_([], _, []). variables_signature_([V|Vs], Prev, [S|Sigs]) :- V #= Prev #<==> S #= 0, Prev #< V #<==> S #= 1, Prev #> V #<==> S #= 2, variables_signature_(Vs, V, Sigs).
Example queries:
?- sequence_inflexions([1,2,3,3,2,1,3,0], N). N = 3. ?- length(Ls, 5), Ls ins 0..1, sequence_inflexions(Ls, 3), label(Ls). Ls = [0, 1, 0, 1, 0] ; Ls = [1, 0, 1, 0, 1].
?- transpose([[1,2,3],[4,5,6],[7,8,9]], Ts). Ts = [[1, 4, 7], [2, 5, 8], [3, 6, 9]].
This predicate is useful in many constraint programs. Consider for instance Sudoku:
:- use_module(library(clpfd)). sudoku(Rows) :- length(Rows, 9), maplist(length_list(9), Rows), append(Rows, Vs), Vs ins 1..9, maplist(all_distinct, Rows), transpose(Rows, Columns), maplist(all_distinct, Columns), Rows = [A,B,C,D,E,F,G,H,I], blocks(A, B, C), blocks(D, E, F), blocks(G, H, I). length_list(L, Ls) :- length(Ls, L). blocks([], [], []). blocks([A,B,C|Bs1], [D,E,F|Bs2], [G,H,I|Bs3]) :- all_distinct([A,B,C,D,E,F,G,H,I]), blocks(Bs1, Bs2, Bs3). problem(1, [[_,_,_,_,_,_,_,_,_], [_,_,_,_,_,3,_,8,5], [_,_,1,_,2,_,_,_,_], [_,_,_,5,_,7,_,_,_], [_,_,4,_,_,_,1,_,_], [_,9,_,_,_,_,_,_,_], [5,_,_,_,_,_,_,7,3], [_,_,2,_,1,_,_,_,_], [_,_,_,_,4,_,_,_,9]]).
Sample query:
?- problem(1, Rows), sudoku(Rows), maplist(writeln, Rows). [9,8,7,6,5,4,3,2,1] [2,4,6,1,7,3,9,8,5] [3,5,1,9,2,8,7,4,6] [1,2,8,5,3,7,6,9,4] [6,3,4,8,9,2,1,5,7] [7,9,5,4,6,1,8,3,2] [5,1,9,2,8,6,4,7,3] [4,7,2,3,1,9,5,6,8] [8,6,3,7,4,5,2,1,9] Rows = [[9, 8, 7, 6, 5, 4, 3, 2|...], ... , [...|...]].
:- use_module(library(clpfd)). n_factorial(N, F) :- zcompare(C, N, 0), n_factorial_(C, N, F). n_factorial_(=, _, 1). n_factorial_(>, N, F) :- F #= F0*N, N1 #= N - 1, n_factorial(N1, F0).
This version is deterministic if the first argument is instantiated:
?- n_factorial(30, F). F = 265252859812191058636308480000000.
#<
or #>.
For example:
?- chain([X,Y,Z], #>=). X#>=Y, Y#>=Z.
For example, to implement a custom labeling strategy, you may need to inspect the current domain of a finite domain variable. With the following code, you can convert a finite domain to a list of integers:
dom_integers(D, Is) :- phrase(dom_integers_(D), Is). dom_integers_(I) --> { integer(I) }, [I]. dom_integers_(L..U) --> { numlist(L, U, Is) }, Is. dom_integers_(D1\/D2) --> dom_integers_(D1), dom_integers_(D2).
Example:
?- X in 1..5, X #\= 4, fd_dom(X, D), dom_integers(D, Is). D = 1..3\/5, Is = [1,2,3,5], X in 1..3\/5.