## Description

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 *p _{ij }*be an atom for 1 ≤

*i*≤

*n*and 1 ≤

*j*≤

*m*. The atom

*p*is T iff the pigeon

_{ij }*i*live in the hole

*j*. Consider the following clause:

*p**i*1 ∨ *p**i*2 ∨ ··· ∨ *p**im.*

This clause says that pigeon *i *lives in a hole. Moreover, consider

^

¬*p**ik *∨ ¬*p**jk.*

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.