In this example, we are attempting to place I pigeons into J
holes in such a way that each hole contains at most one pigeon. One
interesting property of this task is that it can be formulated using
only cardinality constraints (card/2).
Another interesting aspect is that this task has no short resolution
refutations in general.
In the following, we use Prolog
DCG notation to describe a list Cs of CLP(B)
constraints that must all be satisfied.
:- use_module(library(clpb)).
:- use_module(library(clpfd)).
pigeon(I, J, Rows, Cs) :-
length(Rows, I), length(Row, J),
maplist(same_length(Row), Rows),
transpose(Rows, TRows),
phrase((all_cards(Rows,[1]),all_cards(TRows,[0,1])), Cs).
all_cards([], _) --> [].
all_cards([Ls|Lss], Cs) --> [card(Cs,Ls)], all_cards(Lss, Cs).
Example queries:
?- pigeon(9, 8, Rows, Cs), sat(*(Cs)).
false.
?- pigeon(2, 3, Rows, Cs), sat(*(Cs)),
append(Rows, Vs), labeling(Vs),
maplist(portray_clause, Rows).
[0, 0, 1].
[0, 1, 0].
etc.
