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} \lor x_{i, 2} \lor \dots \lor 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} \lor \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

$pr e ˊ sence m + exclusion n (2 m) = m + \frac{n m ( m - 1 )}{2} 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é :

$m$ / $n$	variables	clauses	valuations $2^{mn}$	appels de Quine
$3$ / $2$	$6$	$9$	$64$	$21$
$4$ / $3$	$12$	$22$	$4096$	$97$
$5$ / $4$	$20$	$45$	$1048576$	$521$

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.

Énoncé

Corrigé

Exercices semblables