Description

HOMEWORK 2
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.
You can use any programming language of your choice. Please send me the following files:
(1) your program source code with instructions on how to use it;
(2) the output files (in DIMACS SAT format) for
• n = 3 and m = 3;
• n = 4 and m = 3.
(3) the outputs of MiniSat on the above two input files.
1