Node:A Global Constraint Example, Previous:FD Set Operations, Up:Defining Global Constraints

A Global Constraint Example

The following example defines a new global constraint exactly(X,L,N), which is true if X occurs exactly N times in the list L of integers and domain variables. N must be an integer when the constraint is posted. A version without this restriction and defined in terms of reified equalities was presented earlier; see Reified Constraints.

This example illustrates the use of state information. The state has two components: the list of variables that could still be X, and the number of variables still required to be X.

The constraint is defined to wake up on any domain change.

/* An implementation of exactly(I, X[1]...X[m], N): Necessary condition: 0 =< N =< m. Rewrite rules: [1] |= X[i]=I ==> exactly(I, X[1]...X[i-1],X[i+1]...X[m], N-1): [2] |= X[i]\=I ==> exactly(I, X[1]...X[i-1],X[i+1]...X[m], N): [3] |= N=0 ==> X[1]\=I ... X[m]\=I [4] |= N=m ==> X[1]=I ... X[m]=I */ :- use_module(library(clpfd)). % the entrypoint exactly(I, Xs, N) :- dom_suspensions(Xs, Susp), fd_global(exactly(I,Xs,N), state(Xs,N), Susp). dom_suspensions([], []). dom_suspensions([X|Xs], [dom(X)|Susp]) :- dom_suspensions(Xs, Susp). % the solver method :- multifile clpfd:dispatch_global/4. clpfd:dispatch_global(exactly(I,_,_), state(Xs0,N0), state(Xs,N), Actions) :- exactly_solver(I, Xs0, Xs, N0, N, Actions). exactly_solver(I, Xs0, Xs, N0, N, Actions) :- ex_filter(Xs0, Xs, N0, N, I), length(Xs, M), ( N=:=0 -> Actions = [exit|Ps], ex_neq(Xs, I, Ps) ; N=:=M -> Actions = [exit|Ps], ex_eq(Xs, I, Ps) ; N>0, N<M -> Actions = [] ; Actions = [fail] ).
% rules [1,2]: filter the X's, decrementing N ex_filter([], [], N, N, _). ex_filter([X|Xs], Ys, L, N, I) :- X==I, !, M is L-1, ex_filter(Xs, Ys, M, N, I). ex_filter([X|Xs], Ys0, L, N, I) :- fd_set(X, Set), fdset_member(I, Set), !, Ys0 = [X|Ys], ex_filter(Xs, Ys, L, N, I). ex_filter([_|Xs], Ys, L, N, I) :- ex_filter(Xs, Ys, L, N, I). % rule [3]: all must be neq I ex_neq(Xs, I, Ps) :- fdset_singleton(Set0, I), fdset_complement(Set0, Set), eq_all(Xs, Set, Ps). % rule [4]: all must be eq I ex_eq(Xs, I, Ps) :- fdset_singleton(Set, I), eq_all(Xs, Set, Ps). eq_all([], _, []). eq_all([X|Xs], Set, [X in_set Set|Ps]) :- eq_all(Xs, Set, Ps). end_of_file. % sample queries: | ?- exactly(5,[A,B,C],1), A=5. A = 5, B in(inf..4)\/(6..sup), C in(inf..4)\/(6..sup) | ?- exactly(5,[A,B,C],1), A in 1..2, B in 3..4. C = 5, A in 1..2, B in 3..4