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