☰

Constraint programming over finite domains (new)

Author(s): Emilio Jesús Gallego Arias, Rémy Haemmerlé, Jose F. Morales.

This package extends Ciao with constraints over finite domains (FD). The solver is an instance of the Constraint Logic Programming (CLP) scheme as introduced by Jaffar and Lassez [JL87]. It uses classical propagation techniques as described in Van Hentenryck's book [Van89] and Diaz's clp(FD) implementation [CD96].

The package provides predicates for checking consistency of FD constraints. A FD is a small subset of integers, and FD constraints are relations over integer. Hence only integer or variables are allowed in such constraints. FD variables (i.e., variables that occur in an FD constraint) get associated with a domain either explicitly declared by the program or implicitly imposed by the solver. As soon as variables get an empty domain the computation fails, hence forcing backtracking.

The package defines basic operators, automatically imports basic constraints and enumerating predicates form the module clpfd_rt, and provides high-level Meta-Constraints through a transparent compilation process.

Completeness Considerations

For efficiency reason, the solver is not complete on non-ground constraints, in the sense that it may not be able to determine that a set of constraints is actually satisfiable. In such cases, the system silently succeeds. To ensure full completeness, the programmer may use the labeling/2 predicate that uses an automatic backtracking search to find ground solutions for a list of FD variables. Labeling is complete, always terminates, and yields no redundant solutions. See an example of use of labeling in the following Example.

On success, the top-level will display the domain associated with each FD variable remaining free in the query. This domain should not be understood as values permitted for the corresponding variable, but only as values not excluded by the incomplete propagation mechanism of the solver. Note that the answer output by the top-level is by itself incomplete as the remaining constraints are not showed.

Meta-Constraints

There are five meta-constraints, namely #=/2 (constraint equal), #\=/2 (constraint not equal), #</2 (constraint less than), #=</2 (constraint less or equal), #>/2 (constraint greater than), and #>=/2 (constraint greater or equal). These meta-constraints are defined over arithmetic expressions with FD variables (see regular type fd_expr/1 in module clpfd_rt.). Such constraints are "meta" in the sens that their arguments are interpreted at compile-time and all variables occurring free in the arguments will be implicitly constrained to take integer values only. In particular, note that variables constrained in such a way would not be unifiable with complex FD expressions. For instance, the call:

X + Y #> Z.

is not equivalent to the call:

A = X + Y, A #> Z.

While the first call succeeds, the second one will throw an exception to indicate that A cannot be unified with the non-integer term X + Y. It is possible to view meta-constraints as a convenient way to define an infinite number of FD constraints. For instance A #> Z and X + Y #> Z can be considered respectively as binary and ternary constraints over FD variables.

It is possible to delay interpretation of meta-constraints at call time by explicitly prefixing the call with clpfd_rt. For instance, the following call will not throw any exception:

A = X + Y, clfd_rt:(A #> Z).

Example

The problem is to put N queens on an NxN chessboard so that there is no pair of queens threatening each other. Each variable is a queen. Each queen has a designated row. The problem is to find a different column for each one.

The main constraint of the problem is that no queen threaten another. This is encoded by the diff/3 predicate and should hold for any pair of queens.

The main call is queens(N, L, Lab) which looks for a solution L for the N queens problem using labeling Lab. Observe the call to labeling/2 at the end of definition of queens/3, which tries to find a solution for the problem.

/*-------------------------------------------------------------------------*/
/* Benchmark (Finite Domain)                                               */
/*                                                                         */
/* Name           : queens.pl                                              */
/* Title          : N-queens problem                                       */
/* Original Source: P. Van Hentenryck's book                               */
/*                                                                         */
/* Put N queens on an NxN chessboard so that there is no couple of queens  */
/* threatening each other.                                                 */
/*                                                                         */
/* Solution:                                                               */
/* N=4  [2,4,1,3]                                                          */
/* N=8  [1,5,8,6,3,7,2,4]                                                  */
/* N=16 [1,3,5,2,13,9,14,12,15,6,16,7,4,11,8,10]                           */
/*-------------------------------------------------------------------------*/

:- module(queens, _, [clpfd, fsyntax]).

:- use_module(engine(io_basic), [nl/0]).
:- use_module(library(write),           [write/1]).
:- use_module(engine(runtime_control),      [statistics/2]).
:- use_module(library(lists),           [length/2]).
:- use_module(library(clpfd/fd_range), [fd_range_type/1]).
:- use_module(library(clpfd/fd_constraints)).

%:- module(queens, [main_/2]).
%:- use_module(library(clpfd)).

% Example:
%
% ?- main(18,[ff],clpfd).
% [1,3,5,13,16,4,11,7,14,17,2,18,6,8,10,12,9,15]
% time : 13.937	(fd, prolog_interval_list)
%
% ?- main(18,[ff],fd).
% [1,3,5,13,16,4,11,7,14,17,2,18,6,8,10,12,9,15]
% time : 9.797	(fd, prolog_interval_list)

main(N, Lab, Const) :-
    statistics(runtime, _),
    queens(N, L, Lab, Const),
    statistics(runtime, [_, Y]),
    write(L),
    nl,
    write('time : '),
    write(Y),
    write('\t('), write(~diff_type), write(', '), write(~fd_range_type), 
    write(')'),
    nl.

queens(N, L, Lab, Const) :-
    length(L, N),
    domain(L, 1, N),
    safe(L, Const),
    labeling(Lab, L).

safe([], _Const).
safe([X|L], Const) :-
    noattack(L, X, 1, Const),
    safe(L, Const).

noattack([], _, _, _Const).
noattack([Y|L], X, I, Const) :-
    diff(Const, X, Y, I),
    I1 is I + 1,
    noattack(L, X, I1, Const).

:- discontiguous diff/4.

diff(clpfd, X, Y, I) :-
    X #\= Y,
    X #\= Y+I,
    X+I #\= Y.

diff_type(fd).

diff(fd, X,Y,I):-
    fd_diff(~wrapper(X), ~wrapper(Y), I).

fd_diff(X, Y, I):-
    fd_constraints:'a<>b'(X,Y),
    fd_constraints:'a<>b+t'(X,Y,I),
    fd_constraints:'a<>b+t'(Y,X,I).

:- use_package('clpfd/indexicals').

diff(idx, X,Y,I):-
    idx_diff(~wrapper(X), ~wrapper(Y), I).

idx_diff(X, Y, I) +:
    X in -{val(Y), val(Y)+c(I), val(Y)-c(I)},
    Y in -{val(X), val(X)-c(I), val(X)+c(I)}.

:- use_module(library(clpfd/fd_term)).

diff(kernel, X,Y,I):-
    kernel_diff(~wrapper(X), ~wrapper(Y), I).

kernel_diff(X, Y, I) :-
    fd_term:add_propag(Y, val, 'queens:cstr'(X, Y, I)),
    fd_term:add_propag(X, val, 'queens:cstr'(Y, X, I)).

% Y is always singleton.
cstr(X, Y, I):-
    fd_term:integerize(Y, Y0),
    fd_term:prune(X, Y0),
    Y1 is Y0 + I,
    fd_term:prune(X, Y1),
    Y2 is Y0 - I,
    fd_term:prune(X, Y2).

Usage and interface

Generated with LPdoc using Ciao