# pigeon Test Program

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.

## Kommentare