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: