Ce que coûte une modélisation : le pigeonnier

1. Le codage. Une variable $x_{i,j}$ par couple : « le pigeon $i$ est dans la case $j$ ».

• Chaque pigeon est quelque part : pour chaque $i$, la clause $(x_{i,1}\vee x_{i,2}\vee \cdots \vee x_{i,n})$.
• Deux pigeons ne partagent pas une case : pour chaque case $j$ et chaque paire $i_1<i_2$, la clause $(\neg x_{i_1,j}\vee \neg x_{i_2,j})$.

On remarquera qu'on n'écrit pas « chaque pigeon est dans au plus une case » : la question ne l'exige pas, et une clause qu'on n'écrit pas est une clause que le solveur n'explore pas. Un modèle pourra loger un pigeon dans deux cases — il suffira d'en garder une.

2. Le compte. $m\times n$ variables, et

$$\underset{\text{preˊsence}}{\underbrace{m}}+\underset{\text{exclusion}}{\underbrace{n\left(\genfrac{}{}{0ex}{}{m}{2}\right)}}=m+\frac{nm(m-1)}{2}\text{clauses.}$$

Vérifié : $m=3,n=2$ donne $3+2\cdot 3=9$ ; $m=4,n=3$ donne $4+3\cdot 6=22$ ; $m=5,n=4$ donne $5+4\cdot 10=45$ clauses sur $20$ variables.

3. Elle est insatisfiable — c'est le principe des tiroirs : cinq pigeons, quatre cases, deux au moins se rencontrent. Mesuré :

Le rapport est le message : $521$ appels au lieu d'un million de valuations, sur la même instance et sans changer d'algorithme. La simplification décrite au problème 20.2 coupe les branches dès qu'une clause devient vide — et ici, elle le devient vite.

L'avertissement qui va avec. Le pigeonnier est aussi l'exemple classique de ce que aucun solveur du commerce ne sait faire : la croissance reste exponentielle en $m$, parce que toute preuve d'insatisfiabilité par résolution doit, pour cette famille, avoir une taille exponentielle. Modéliser en sat ne rend rien facile : cela rend seulement le problème exprimable.