TAOCP 7.1.1 Exercise 41
Let $x_{ij}$ be a Boolean variable for $1 \le i \le m$, $1 \le j \le n$, with the intended meaning that pigeon $i$ is placed in hole $j$.
Exercise 41. [20] (The pigeonhole principle.) The island of San Serriffe contains $m$ pigeons and $n$ holes. Find a conjunctive normal form that is satisfiable if and only if each pigeon can be the sole occupant of at least one hole.
Verified: yes
Solve time: 1m12s
Solution
Let $x_{ij}$ be a Boolean variable for $1 \le i \le m$, $1 \le j \le n$, with the intended meaning that pigeon $i$ is placed in hole $j$.
Introduce auxiliary variables $y_{ij}$ for $1 \le i \le m$, $1 \le j \le n$, with the intended meaning that hole $j$ is chosen as a witness hole for pigeon $i$ in which $i$ is the sole occupant.
Define the formula
$$ F ;=; \bigwedge_{i=1}^m F_i $$
where for each $i$,
$$ F_i ;=; \left(\bigvee_{j=1}^n y_{ij}\right) ;\wedge; \bigwedge_{j=1}^n (\bar{y}{ij} \vee x{ij}) ;\wedge; \bigwedge_{j=1}^n \bigwedge_{\substack{k=1 \ k \ne i}}^m (\bar{y}{ij} \vee \bar{x}{kj}). $$
Each clause is a disjunction of literals, so $F$ is in conjunctive normal form.
Assume $F$ is satisfiable. Fix $i$ and choose $j$ such that $y_{ij} = 1$, which exists by $\bigvee_{j=1}^n y_{ij}$. From $(\bar{y}{ij} \vee x{ij})$ and $y_{ij}=1$, it follows that $x_{ij}=1$. From $(\bar{y}{ij} \vee \bar{x}{kj})$ for all $k \ne i$ and $y_{ij}=1$, it follows that $x_{kj}=0$ for all $k \ne i$. Hence hole $j$ contains pigeon $i$ and no other pigeon occupies hole $j$. This holds for every $i$, so each pigeon has at least one hole in which it is the sole occupant.
Assume for each $i$ there exists $j$ such that $x_{ij}=1$ and $x_{kj}=0$ for all $k \ne i$. Define $y_{ij}=1$ for one such chosen pair $(i,j)$ and define $y_{ij}=0$ for all other pairs.
For each fixed $i$, at least one $y_{ij}=1$, so $\bigvee_{j=1}^n y_{ij}=1$ holds.
If $y_{ij}=0$, then $(\bar{y}{ij} \vee x{ij})=1$ and $(\bar{y}{ij} \vee \bar{x}{kj})=1$ for all $k \ne i$.
If $y_{ij}=1$, then by construction $x_{ij}=1$ and $x_{kj}=0$ for all $k \ne i$, so $(\bar{y}{ij} \vee x{ij})=1$ and $(\bar{y}{ij} \vee \bar{x}{kj})=1$ for all $k \ne i$.
Thus every clause in each $F_i$ is satisfied, hence $F$ is satisfied.
This completes the proof. ∎