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