Probleme – Coloration en \textsc{sat}, et une famille de clauses qu'on peut jeter

Exercice · niveau 3 (difficile) · informatique (MP2I/MPI), chapitre 20 — Logique propositionnelle

Énoncé

On reprend le codage de la coloration donné dans le cours, et on l'éprouve sur le graphe de Petersen : $10$ sommets, $15$ arêtes.

Compter les variables et les clauses en fonction de $n$ , $m$ et $k$ .
Pour quelles valeurs de $k$ la formule est-elle satisfiable ?
Montrer que les clauses « au plus une couleur » peuvent être supprimées sans changer la réponse. Que perd-on ?
Que gagne-t-on à les supprimer ?

Corrigé

1. Le compte. $nk$ variables $x_{u, c}$ , et trois familles de clauses :

$au moins une n + au plus une n (2 k) + voisins distincts mk = n + \frac{nk ( k - 1 )}{2} + mk .$

Pour Petersen ( $n = 10$ , $m = 15$ ), mesuré :

$k$	variables	au moins une	au plus une	arêtes	total
$2$	$20$	$10$	$10$	$30$	$50$
$3$	$30$	$10$	$30$	$45$	$85$
$4$	$40$	$10$	$60$	$60$	$130$

La famille « au plus une » est quadratique en $k$ : c'est elle qui domine dès que les couleurs sont nombreuses.

2. Les valeurs de $k$ . Mesuré par l'algorithme de Quine du problème 20.2 :

$k = 2$	insatisfiable
$k = 3$	satisfiable, et le modèle donne une coloration propre
$k = 4$	satisfiable

Le nombre chromatique de Petersen est donc $3$ . Que $k = 2$ échoue se voit à la main : Petersen contient un cycle de longueur $5$ , et un cycle impair n'est jamais $2$ -coloriable. Que $k = 3$ réussisse ne se voit pas à la main — et c'est précisément l'intérêt de déléguer.

3. On peut les jeter. Notons $Φ$ la formule complète et $Φ^{'}$ celle privée des clauses « au plus une ».

Un modèle de $Φ$ est un modèle de $Φ^{'}$ : on a retiré des contraintes.

Réciproquement, soit $w$ un modèle de $Φ^{'}$ . Chaque sommet $u$ porte au moins une couleur (première famille) ; choisissons-en une, notée $c (u)$ , arbitrairement parmi celles que $w$ lui donne. Si ${u, v}$ est une arête, la troisième famille interdit que $u$ et $v$ partagent une couleur quelconque : en particulier $c (u) \neq = c (v)$ . Donc $c$ est une coloration propre, et l'on en refait un modèle de $Φ$ en ne gardant que $c (u)$ .

Les deux formules sont donc équisatisfiables, et une coloration se lit dans un modèle de l'une comme de l'autre.

Ce qu'on perd est mesurable : avec $Φ$ , chaque sommet reçoit exactement une couleur ; avec $Φ^{'}$ , un modèle peut en donner plusieurs — c'est ce qu'a rendu le solveur pour $k = 3$ et $k = 4$ . Le modèle n'est plus lisible directement : il faut le post-traiter par le « choisissons-en une » ci-dessus. On échange une garantie de forme contre une économie de clauses, et c'est un marché qu'on ne passe qu'en le sachant.

4. Le gain, mesuré sur Petersen :

$k$	clauses de $Φ$	clauses de $Φ^{'}$	économie
$2$	$50$	$40$	$20 %$
$3$	$85$	$55$	$35 %$
$4$	$130$	$70$	$46 %$

L'économie croît avec $k$ , puisqu'on supprime le seul terme quadratique. Pour $k = 20$ couleurs sur un graphe de $1000$ sommets, on passerait de $190000$ clauses « au plus une » à zéro.

En pratique — Écrire la contrainte la plus faible qui suffit

C'est la leçon de ce problème, et elle vaut pour toute modélisation. On est tenté d'écrire tout ce qu'on sait du problème — « un sommet a une seule couleur » est vrai, après tout. Mais une clause n'est utile que si son absence rend la réponse fausse. Ici elle ne la rend pas fausse : elle rend seulement le modèle moins net.

La discipline est celle du chapitre chap:discipline : on spécifie ce dont on a besoin, pas ce qu'on croit vrai. Et l'on documente le post-traitement, faute de quoi le lecteur du modèle sera surpris de voir un sommet bleu et rouge à la fois.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.