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.