Consider the following pigeonhole problem:
• There are n pigeons and m holes.
• Each pigeon has to live in a hole.
• Each hole can have at most one pigeon.
We would like to find a hole for every pigeon. Clearly, the problem is not solvable if n > m.
Let pij be an atom for 1 ≤ i ≤ n and 1 ≤ j ≤ m. The atom pij is T iff the pigeon i live in the hole j. Consider the following clause:
pi1 ∨ pi2 ∨ ··· ∨ pim.
This clause says that pigeon i lives in a hole. Moreover, consider
¬pik ∨ ¬pjk.
1≤i<j≤n
This formula says that at most one pigeon lives in hole k. Please write a program such that:
• it accepts two positive numbers n and m as inputs.
• it outputs a CNF formula in DIMACS SAT format.
• the generated CNF formula specifies the pigeonhole problem with n pigeons and m holes.
