The pigeonhole principle is a very basic combinatorial principle. It states that distributing n items into m boxes whereby n>m, will result in at least one box carrying two items. We use a Boolean formulation of the problem as our test case. We show that the principle holds for n=6 and m=5.

The pure Prolog solution uses a small SAT solver and generates the problem clauses via some DCG rules. The SAT solver implements a simplified variant of the Davis–Putnam algo-rithm. The filter/4 predicate allows to compute Φ[l=0] respectively Φ[l=1] for a clause set Φ and a literal l. Our algorithm then simply fetches always the first new literal:

function sat(Φ) {

if Φ={} then

return true;

if Φ={{}, c1, .., cn} then

return false;

Φ={{l, r1, .., rm}, c1, .., cn}

return sat(Φ[l=0]) or sat(Φ[l=1]);

}

The CLP(FD) solution models Boolean variables by integer variables in the range 0..1. A clause can then easily be represented as an inequality. The CPL(FD) solution leaves the choice of a solving algorithm to the constraint system. The constraint system might choose a solving algorithm that is better than our SAT solver.

For the pigeon test program there are the following sources:

**pigeon.p:**- pigeon3.p: The CLP(FD) text.