Centrale Option Informatique MP 2014Sujet, corrigé et rapport du jury

I Présentation du jeu de sudoku

Règles du jeu

Représentation d'une grille de sudoku

Caml

Pascal

Préliminaires

Caml

Pascal

II Codage de la formule initiale

Représentation des formules logiques

• la clause x_((0, 0))^5 ∨ x_((0, 8))^5 ∨ x_((8, 0))^5 ∨ x_((8, 8))^5 exprime qu'une au moins des quatre cases situées aux coins de la grille est occupée par un 5 ;
• la formule sous forme normale conjonctive ⋀_(i = 0)^8(⋁_(k = 1)^9 x_((i, 7))^k) exprime que chacune des valeurs de la colonne 7 est constituée de chiffres compris entre 1 et 9 ;
• la clause ⋁_(j = 0)^8 x_(indice (3, j))^6 exprime que l'une des cases du bloc numéro 3 de la grille contient le chiffre 6 (où indice est la fonction/procédure de la question I.D).
  Pour la programmation, les clauses sont des listes de littéraux et les formules logiques (qui seront écrites exclusivement en forme normale conjonctive) des listes de clauses.
  Ainsi, en notant les listes entre ⟨⟩_–, la formule x_((1, 8))^7 ∧ (x_((0, 4))^3 ∨ ¬x_((2, 7))^5) est représentée formellement par la liste de listes ⟨⟨(1, 8, 7)⟩; ⟨(0, 4, 3); (2, 7, 5)^–⟩⟩ (où un triplet surligné désigne un littéral négatif). Plus précisément:

Caml

Pascal

• Nil qui est la liste vide ; on peut tester si une liste 1 est vide avec l'expression 1 = Nil;
• tete(c: clause) : litteral et tete(f : formule) : clause qui permettent d'obtenir le premier élement d'une liste ;
• queue(c: clause) : clause et queue(f : formule) : formule qui permettent d'obtenir la queue d'une liste ;
• ajout_en_tete(l : litteral ; c : clause) : clause et ajout_en_tete(c : clause ; f : formule) : formule qui permettent d'ajouter un élément en tête d'une liste ;
• concatener(f1: formule ; f2: formule) : formule qui permet de concaténer deux listes, cette fonction a un coût linéaire en la taille de la première liste.
  On suppose que l'on peut tester l'égalité de deux littéraux 11 et 12 à l'aide de l'expression 11 = 12. Cette opération n'est pas disponible pour les clauses et les formules.

II.A - Formule logique décrivant la règle du jeu

II.A.1)

II.A.3)

II.A.4)

II.B - Formule logique décrivant la grille initiale

• si dans la grille initiale, la case d'indice (i, j) est déjà remplie par la valeur k ∈ [ [1, 9] ], on peut considérer d'emblée, en plus de la clause unitaire positive x_((i, j))^k (déjà prise en compte par la formule F ci-dessus), les 8 clauses unitaires négatives ¬x_((i, j))^l avec l ∈ [ [1, 9] ]∖{k}; on enrichit ainsi la formule F en une formule F_1
  en forme normale conjonctive constituée de r clauses unitaires positives (celles de F ) et 8r négatives (où r est le nombre de cases remplies dans la grille initiale) ;
• si, dans une grille initiale, une case d'indice ( i, j ) n'est pas remplie (c'est-à-dire est occupée par la valeur 0 ), alors on sait que cette case ne peut être remplie par aucune valeur k ∈ [ [1, 9] ] apparaissant déjà dans la ligne i, ou dans la colonne j, ou dans le bloc auquel appartient la case d'indice ( i, j ); puisqu'une telle valeur k est interdite pour la case d'indice ( i, j ), on peut donc considérer la clause unitaire négative ¬x_((i, j))^k; ainsi, pour la case d'indice ( 1,3 ) de l'exemple de la figure 1 à droite, il n'est pas question de remplacer la valeur 0 par aucune des valeurs appartenant à {2, 3, 4, 5, 7, 9} : on peut donc ajouter les clauses ¬x_((1, 3))^2, ¬x_((1, 3))^3, ¬x_((1, 3))^4, ¬x_((1, 3))^5, ¬x_((1, 3))^7 et ¬x_((1, 3))^9; on note alors F_2 la formule en forme normale conjonctive constituée de la conjonction de toutes ces clauses unitaires négatives obtenues en parcourant toutes les cases non remplies de la grille initiale.
  La formule décrivant la grille initiale est donc F_(grille) = F_1 ∧ F_2.
  II.B.1) Écrire une fonction donnees qui, à partir d'une grille de sudoku initiale (donnée sous la forme d'un tableau), renvoie la formule F_1, toujours sous la forme d'une liste de listes de littéraux.

II.B.2)

Formule initiale complète

Caml

Pascal

III Résolution d'une grille de sudoku

III.A - Règle de propagation unitaire

• en supprimant toutes clauses de F qui contiennent l;
• en supprimant ¬l de toutes les clauses de F (ainsi si une clause ne contient que ¬l elle est remplacée par la clause vide ⊥ )
  Par exemple la formule F = (¬x_((0, 2))^3) ∧ (¬x_((0, 2))^3 ∨ x_((2, 5))^6) ∧ (x_((0, 2))^3 ∨ ¬x_((1, 4))^7) contient un unique littéral isolé ¬x_((0, 2))^3. En simplifiant F par ce littéral, on obtient la formule F^′ = ¬x_((1, 4))^7.
  III.A.3) On justifie formellement cette simplification. Soit F une formule en forme normale conjonctive contenant un littéral isolé l (associé à la variable propositionnelle p : on a donc l = p ou l = ¬p ). F peut s'écrire alors sous la forme F = l ∧ F_1 ∧ F_2 ∧ F_3, où :
• F_1 est une formule constituée de clauses contenant chacune le littéral l;
• F_2 est une formule constituée de clauses contenant chacune le littéral ¬l et ne contenant pas le littéral l;
• F_3 est une formule constituée de clauses ne contenant chacune ni le littéral l, ni le littéral ¬l.

III.A.5)

III.B - Règle du littéral infructueux

• si l'algorithme de propagation unitaire appliqué à la formule F ∧ ¬x permet de déduire la clause vide alors on ajoute la clause x à F;
• si l'algorithme de propagation unitaire appliqué à la formule F ∧ x permet de déduire la clause vide alors on ajoute la clause ¬x à F.
  III.B.1) Justifier formellement que si l'on peut déduire la clause vide à partir de la formule F ∧ ¬x alors F ≡ F ∧ x 。
  III.B.2) Écrire une fonction variables qui, à partir d'une formule, renvoie la liste de ses variables sans doublons.
  On supposera qu'on dispose d'une fonction flatten qui à partir d'une formule f renvoie la clause formée de tous les éléments des sous-listes de f. Par exemple flatten appliqué à ⟨⟨(1, 8, 7)⟩; ⟨(2, 7, 5)^–; (1, 8, 7)⟩⟩ renvoie ⟨(1, 8, 7); (2, 7, 5)^–; (1, 8, 7)⟩.
  III.B.3) Écrire une fonction deduction qui, à partir d'un tableau, d'une variable x et d'une formule F, renvoie 1 si la règle du littéral infructueux permet d'ajouter la clause x à F, − 1 si elle permet d'ajouter la clause ¬x à F et 0 sinon.
  On supposera qu'on dispose d'une fonction copier_matrice qui à partir d'un tableau renvoie un autre tableau distinct contenant les mêmes valeurs.
  III.B.4) Nous proposons un deuxième algorithme de propagation basé sur la règle du littéral infructueux. Celui-ci consiste à appliquer la propagation unitaire et, quand celle-ci ne permet plus de déduire de nouvelles clauses, à appliquer la règle du littéral infructueux pour obtenir une nouvelle clause unitaire de la forme x ou ¬x. Dès lors on peut reprendre la propagation unitaire. Le processus s'arrête lorsque ni la propagation unitaire ni la règle du littéral infructueux ne permettent de déduire de nouvelles clauses.
  Écrire une fonction propagation2 qui, à partir d'un tableau t représentant le sudoku et d'une formule F représentant les contraintes du sudoku, met en œuvre cet algorithme. Cette fonction modifiera le tableau t selon la valeur des cases pouvant être déduites.
  III.B.5) Écrire une fonction sudoku qui, à partir d'un sudoku donné sous forme d'un tableau t, modifie t et renvoie la grille complétée au maximum en utilisant les techniques précédentes.
  Expérimentalement, la règle de propagation unitaire permet de résoudre les sudokus les plus faciles et environ la moitié des sudokus les plus difficiles. À notre connaissance, il n'existe pas de sudoku ne pouvant être résolu intégralement à l'aide de la règle du littéral infructueux.