CLP(FD)

Constraint Logic Programming over Finite Domains — declarative integer arithmetic.

28.1 Basics

:- use_module(library(clpfd)).     % Scryer/SICStus: library(clpz) / library(clpfd)

?- X #= 1 + 2.                     % X = 3
?- 3 #= Y + 2.                     % Y = 1 — works backwards!
?- X #> 3, X #< 6.                 % X in 4..5
?- X in 1..10, X #> 5, X mod 2 #= 0, label([X]).   % X = 6 ; X = 8 ; X = 10
?- X * X #= 144, X #> 0.           % X = 12

28.2 Constraint operators

X #= Y, X #\= Y equal / not equal X #< Y, #>, #=<, #>= X in L..H, Xs ins L..H domains (inf, sup for unbounded; \/ for unions) all_different(Xs), all_distinct(Xs) pairwise distinct (all_distinct stronger propagation)

sum(Xs, #=, S), scalar_product(Cs, Vs, #=, S) element(I, List, V) V is the I-th element global_cardinality(Vs, Pairs) tuples_in(Tuples, Relation) cumulative(Tasks, [limit(L)]) reification & logical connectives zcompare(Order, A, B)

28.3 Labeling (search)

Options: variable selection (leftmost, ff, ffc, min, max), value order (up, down), branching (step, enum, bisect), optimization (min(E), max(E)).

label(Vars)                              % default search
labeling([ff], Vars)                     % first-fail heuristic
labeling([max(Expr)], Vars)              % optimization
labeling([min(Cost), bisect, down], Vs)

28.4 Reversible factorial

n_factorial(0, 1).
n_factorial(N, F) :-
    N #> 0, N1 #= N - 1, F #= N * F1,
    n_factorial(N1, F1).

?- n_factorial(5, F).      % F = 120
?- n_factorial(N, 120).    % N = 5
?- n_factorial(N, F).      % enumerates (0,1), (1,1), (2,2), (3,6), ...

28.5 SEND + MORE = MONEY

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]).

28.6 N-Queens

n_queens(N, Qs) :-
    length(Qs, N),
    Qs ins 1..N,
    safe_queens(Qs).

safe_queens([]).
safe_queens([Q|Qs]) :- safe_queens(Qs, Q, 1), safe_queens(Qs).

safe_queens([], _, _).
safe_queens([Q|Qs], Q0, D0) :-
    Q0 #\= Q,
    abs(Q0 - Q) #\= D0,
    D1 #= D0 + 1,
    safe_queens(Qs, Q0, D1).

?- n_queens(8, Qs), labeling([ff], Qs).
Qs = [1, 5, 8, 6, 3, 7, 2, 4].

28.7 Sudoku

sudoku(Rows) :-
    length(Rows, 9), maplist(same_length(Rows), Rows),
    append(Rows, Vs), Vs ins 1..9,
    maplist(all_distinct, Rows),
    transpose(Rows, Columns), maplist(all_distinct, Columns),
    Rows = [As, Bs, Cs, Ds, Es, Fs, Gs, Hs, Is],
    blocks(As, Bs, Cs), blocks(Ds, Es, Fs), blocks(Gs, Hs, Is).

blocks([], [], []).
blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3]) :-
    all_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
    blocks(Ns1, Ns2, Ns3).

problem(1, [[_,_,_,_,_,_,_,_,_],
            [_,_,_,_,_,3,_,8,5],
            [_,_,1,_,2,_,_,_,_],
            [_,_,_,5,_,7,_,_,_],
            [_,_,4,_,_,_,1,_,_],
            [_,9,_,_,_,_,_,_,_],
            [5,_,_,_,_,_,_,7,3],
            [_,_,2,_,1,_,_,_,_],
            [_,_,_,_,4,_,_,_,9]]).

?- problem(1, Rows), sudoku(Rows), maplist(labeling([ff]), Rows), maplist(portray_clause, Rows).

28.8 Scheduling & optimization

% Knapsack: maximize value under weight limit
knapsack(Take, Value) :-
    Weights = [12, 2, 1, 4, 1], Values = [4, 2, 1, 10, 2],
    length(Take, 5), Take ins 0..1,
    scalar_product(Weights, Take, #=<, 15),
    scalar_product(Values, Take, #=, Value),
    labeling([max(Value)], Take).

% Task scheduling with cumulative
schedule(Starts, End) :-
    Starts = [S1, S2, S3], Starts ins 0..20,
    Tasks = [task(S1, 3, _, 1, a), task(S2, 4, _, 1, b), task(S3, 2, _, 1, c)],
    cumulative(Tasks, [limit(1)]),          % one machine
    S1 + 3 #=< S3,                          % precedence
    End #= max(S2 + 4, S3 + 2),
    labeling([min(End)], [End|Starts]).

28.9 Reification

?- X in 0..5, B #<==> (X #> 3), B = 1.     % X in 4..5
count_positive(Xs, N) :-
    maplist([X, B]>>(B #<==> (X #> 0)), Xs, Bs),
    sum(Bs, #=, N).