Constraint programming over finite domains

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, the constraint equal, #=/2, the constraint not equal, #</2, the constraint less than, the constraint not equal, #=</2, the constraint less or equal, #>/2, the constraint more than, and #>/2, the constraint more or equals. These meta-constraint are defined over arithmetic expression 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. 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, expander, fsyntax]).

:- use_module(library(write),           [write/1]).
:- use_module(library(prolog_sys),      [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)).

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.

:- use_module(library(clpfd(fd_constraints))).

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

Known bugs and planned improvements

• See clpfd/clpfd_options for a list of configurable options in the solver. This part is undocummented.