# 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.

For the pigeon test program there are the following sources:

• pigeon.p: The Prolog text.
• The CLP(FD) text.