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 integer Given value a variable Unknown value -Expr Unary minus Expr + Expr Addition Expr * Expr Multiplication Expr - Expr. Subtraction min(Expr,Expr) Minimum of two expressions max(Expr,Expr) Maximum of two expressions Expr mod Expr Remainder of integer division abs(Expr) Absolute value Expr / Expr Integer 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.
=<
I =<
Upper.
The atoms
inf and sup denote negative and positive infinity,
respectively.
\/
Domain2The second set of options lets you influence the order of solutions:
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.
sum(List, #=< 100)
=<
S_j or S_j +
D_j =<
S_i for all 1 =<
i <
j =<
n.