Constraint programming is a declarative formalism that lets you describe conditions a solution must satisfy. This library provides CLP(FD), Constraint Logic Programming over Finite Domains. It can be used to model and solve various combinatorial problems such as planning, scheduling and allocation tasks.
Most predicates of this library are finite domain constraints, which are relations over integers. 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 integer Given value a variable Unknown value -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 / Expr Truncated integer division
The most important finite domain constraints are:
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 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 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. If a variable
occurs at the place of a constraint that is being reified, it is
implicitly constrained to the Boolean values 0 and 1. Therefore, the
following queries all fail: ?-
#\
2., ?-
#\
#\
2. etc.
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. ?- Vs = [X,Y,Z], Vs ins 1..3, all_different(Vs), X = 1, Y #\= 2. Vs = [1, 3, 2], X = 1, Y = 3, Z = 2. ?- 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.
A common usage of this library is to first post the desired constraints among the variables of a model, and then to use enumeration predicates to search for solutions. 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.
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]), 1000*9+91*_A2+ -90*_A3+_A4+ -9000*1+ -900*0+10*_B3+ -1*_C5#=0, _A3 in 5..8, _A4 in 2..8, _B3 in 2..8, _C5 in 2..8.
Here, the constraint solver has deduced more stringent bounds for all variables. Keeping the modeling part separate from the search lets you view these residual goals, observe termination and determinism properties of the modeling part in isolation from the search, and more easily experiment with different search strategies. Labeling can then be used to search for solutions:
?- 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.
You can also use CLP(FD) constraints as a more declarative alternative for ordinary integer arithmetic with is/2, >/2 etc. For 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 rewrite constraints at compilation time. The expansion's aim is to transparently bring the performance of CLP(FD) constraints close to that of conventional arithmetic predicates (</2, =:=/2, is/2 etc.) when the constraints are used in modes that can also be handled by built-in arithmetic. To disable the expansion, set the flag clpfd_goal_expansion to false.
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.
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} }
=<
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.
\/
Domain2The 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:
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, V, [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]), all_distinct(V). 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.
?- 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] .
:- 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)]). ?- length(Vs, 3), two_consecutive_ones(Vs), label(Vs). Vs = [0, 1, 1] ; Vs = [1, 1, 0] ; Vs = [1, 1, 1].
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_(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_(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.