3-coloration d'un graphique avec des formules propositionnelles

Question

J'essaie de résoudre un problème spécifique, donc toute aide serait grandement appréciée :

Soit $G = (V,E)$ un graphe non orienté avec un ensemble de sommets $V$ et un ensemble d'arêtes $E$.Une 3-coloration de $G$ est une application $\chi:V o \{R,G,Y\}$ telle que si $\{x,y\}\in E$ alors $\chi(x) eq \chi(y)$.(Laissez $R,G,Y$ représenter respectivement le rouge, le bleu et le jaune).

Supposons que $n > 1$ et soit $V_n = \{0,1,\cdots,n-1\}$ et soit $G_n = (V_n,E_n)$ un graphe non orienté avec un ensemble de sommets $V_n$.Pour chaque $i$, $0 \leq i < n$ soit $R_i,B_i,Y_i$ des variables propositionnelles.Nous pouvons penser que $i$ est un nœud, donc $R_i$ dit que le nœud $i$ a une couleur rouge.

Donnez une formule propositionnelle $ a_n $ en utilisant les variables $ {r_i, b_i, y_i | 0 leq i <n } $ tel que $ a_n $ est satisfaisable sif $ g_n $ a une couleur.Faites cela de telle manière que $A_n$ puisse être calculé efficacement à partir de $G_n$ (par ex.ne définissez pas $A_n$ comme étant $R_1$ si $G_n$ a trois colorations et ($R_1 \wedge eg R_1$) sinon).

Mon inclination pour une question comme celle-ci est de mettre en place une sorte de formule CNF, c'est-à-dire de proposer un ensemble de clauses visant à prendre en charge différentes propriétés.Par exemple, je crois que pour quelque chose comme ça, j'ai besoin d'une clause qui traite du cas où chaque nœud a une couleur, peut-être qu'une clause qui traite de chaque nœud ne peut pas avoir plus d'une couleur, et que chaque nœud ne peut pas avoir la même couleur qu'un nœud adjacent. nœud?Je ne sais pas vraiment comment illustrer ce dernier point ou s'il y a des cas qui me manquent.