Page précédente LERIA Faculté des Sciences Université d'Angers
English version


Un problème de coloration d'échiquier pour les solveurs SAT ( téléchargement des instances)


Ce problème de coloration d'échiquier a été présenté comme le premier problème des cinquièmes "Annual U.S.A Mathematical Olympiad", en 1976. La première partie de ce problème est de prouver qu'il n'est pas possible de colorier en noir ou en blanc les cases d'un échiquier de taille $ 4\times 7$ tel que les 4 coins de tous les rectangles de cet échiquier n'aient pas tous la même couleur, comme le montre la figure 1. Un rectangle avec ces 4 coins de la même couleur est dit rectangle chromatique (CR) (ligne pleine, figure 1). De plus, les échiquiers possédant au moins un CR sont appelés des échiquiers chromatiques et ceux ne contenant aucun CR sont appelés des échiquiers NCR. La seconde partie du problème était de trouver une coloration d'un échiquier $ 4 \times 6$ répondant à la contrainte de coloration (figure 1).

Figure 1: A $ 4\times 7$ échiquier CR (gauche) et un $ 4\times 6$ échiquier NCR (droite)
\includegraphics[width=3cm,height=3cm]{4-7CB.eps} \includegraphics[width=3cm,height=3cm]{4-6CB.eps}

Beresin, Levine et Winn [1] ont donné la preuve pour la première partie et une solution pour la seconde. Ils ont aussi généralisé leurs résultats à tous les échiquiers $ m \times n$ coloriés avec $ t$ couleurs. Ils ont établi les conditions suivant lesquelles un échiquier avait au moins un CR. En appliquant leur principe et la propriété de coloration au cases de deux et trois couleurs, ils ont trouvé les conditions nécessaires et suffisantes sur $ n$ et $ m$ pour décider si un échiquier est CR ou NCR. Pour résumer, le problème de savoir si un échiquier $ m \times n$ est CR ou NCR est résolu pour deux et trois couleurs.

Coder ce problème en problème SAT


Une instance d'un problème SAT est défini par un ensemble de variables booléennes (aussi appelées atomes) $ {\cal X}$ et d'une formule booléenne $ \phi \colon \{0,1\}^n \to \{0,1\}$. Un littéral est une variable ou sa négation. Une clause est une disjonction de littéraux. La formule $ \phi$ est en forme normale conjonctive (CNF) si c'est une conjonction de clauses. Une affectation est une fonction $ v \colon {\cal X} \to \{0,1\}$. La formule est dite satisfiable s'il existe une affectation satisfaisant $ \phi$ et insatisfiable autrement. Dans ce problème, $ \phi$ sera en CNF.

Soit une échiquier de taille $ n \times n$, l'ensemble de ses cases$ {\cal B} = [1..n] \times [1..n]$ est de taille $ n^2$, donc les éléments de $ {\cal B}$ peuvent être considérés comme un ensemble de variables $ \{X_1,..X_{n^2}\}$ par un isomorphisme :

$\displaystyle flat \colon {\cal B} \to \{X_1,..X_{n^2}\} $

$\displaystyle \forall X=(x,y) \in {\cal B}, flat(X)=X_{x + n\times y} $

Cette fonction produit une représentation aplatie de l'échiquier.

Un rectangle de l'échiquier peut être associé à toutes les paires de points $ A=(a_1,a_2)$ et $ B=(b_1,b_2)$ telles que $ \forall i, a_i \neq b_i$. Le rectangle correspondant est donc pleinement définit par ses 4 coins :

\begin{displaymath} \begin{array}{ l} R(A,B) = (X_{a_1+n\times a_2},X_{b_1+n\times a_2},X_{a_1+n\times b_2},X_{b_1+n\times b_2})\\ \end{array} \end{displaymath}

Il est à noter que chaque rectangle peut être référencé par les deux paires de points complémentaires (i.e. $ R((x_1,y_1),(x_2,y_2))=R((x_1,y_2),(x_2,y_1))$). Nous considérons $ {\cal R}$ l'ensemble de tous les rectangles distincts pour un échiquier donné.

Maintenant, une instance de ce problème peut être définie entièrement par ses deux paramètres : le nombre de couleurs $ N_{col}$ et la taille de l'échiquier $ n$.

Soit $ n$ et $ N_{col}$, nous commençons par créer l'ensemble des variables propositionelles $ \{ X_{ij} \mid i \in [1..n^2],j \in [1..N_{col}]\}$ ($ X_{ij}$ est vraie quand la $ i^{th}$ variable du problème initial est de couleur $ j$). Nous devons nous assurer que chaque case n'aura qu'une et une seule couleur :

$\displaystyle \forall i \in [1..n^2] ( \bigvee_{j\in [1..N_{col}]} X_{ij} \wedg......!\bigwedge_{j,k\in [1..N_{col}],j \neq k} \!\!(\neg X_{ij} \vee \neg X_{ik}))$

Puis nous devons interdire la création de rectangles chromatiques en utilisant les caractéristiques de ces rectangles.

$\displaystyle \forall i_1,i_2,i_3,i_4, (X_{i_1},X_{i_2},X_{i_3},X_{i_4}) \in {\......col}]} (\neg X_{i_1k} \vee \neg X_{i_2k}\vee \neg X_{i_3k} \vee \negX_{i_4k})$

Ceci impose que pour une couleur donnée $ k$, les 4 variables propositionelles $ X_{i_1k},X_{i_2k},X_{i_3k}$ and $ X_{i_4k}$ formant un rectangle ne sont pas vraies simultanément.

Notre problème SAT est donc la conjonction de toutes ces clauses.

Bibliography

1
May Beresin, Eugene Levine, and John Winn.
A chessboard coloring problem.
The College Mathematics Journal, 20(2):106-114, 1989.



Téléchargement: