Centrale Informatique MP 2014

Thème de l'épreuve Résolution automatique de sudokus
Principaux outils utilisés logique
Mots clefs sudoku, variables propositionnelles, équivalence logique

Corrigé

(c'est payant, sauf le début): - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Extrait gratuit du corrigé

(télécharger le PDF)
           

Énoncé complet

(télécharger le PDF)
                    

Rapport du jury

(télécharger le PDF)
     

Énoncé obtenu par reconnaissance optique des caractères


Informatique  4 heures Calculatrices autorisées N Les candidats indiqueront en tête de leur copie le langage de programmation choisi (Pascal ou Caml). Les candidats ayant choisi Caml devront donner le type de chaque fonction écrite. Les candidats travaillant en Pascal pourront écrire des fonctions ou des procédures. Le sujet comporte trois parties: la partie I est essentiellement consacrée à présenter le problème étudié; la partie III nécessite d'avoir compris le principe de l'encodage décrit et étudié dans la partie II, mais il n'est pas besoin d'avoir répondu aux questions de la partie II pour l'aborder. I Présentation du jeu de sudoku Règles du jeu Le sudoku est un jeu de réflexion très répandu depuis quelques années. Il se présente sous l'aspect d'une grille carrée à 81 cases (9 lignes et 9 colonnes), elle--même scindée en 9 sous--grilles de taille 3 >< 3 appelées blocs (cf figure 1). Cette grille est initialement partiellement remplie par des chiffres compris entre 1 et 9 : c'est la grille initiale. Le but du jeu consiste à compléter entièrement la grille en remplissant les cases initialement vides par des chiffres de 1 à 9, de telle manière qu'une fois la grille remplie, chacun des chiffres compris entre 1 et 9 apparaisse une et une seule fois dans chacune des 9 lignes, chacune des 9 colonnes et chacun des 9 blocs de la grille : on obtient alors une grille finale associée à la grille initiale. 0 0 8 5 0 OO\]OEOEH>CÆMHO Exemple de grille initiale Représentation de la grille initiale ci--contre (où le bloc numéro 3 est grisé) Figure 1 On suppose dans tout le sujet que la grille initiale est ainsi faite qu'elle admet une et une seule grille finale qui lui soit associée. Résoudre une grille de sudoku consiste donc à déterminer la grille finale associée à une grille initiale donnée. La figure 1 à gauche représente une grille initiale (dont 24 cases sont remplies). Les blocs sont matérialisés par un trait plus épais. L'objet du problème est d'étudier un algorithme de résolution des grilles de sudoku fondé sur la manipulation de formules logiques. En effet, le principe de la résolution d'une grille de sudoku peut s'énoncer facilement par les cinq règles logiques ci--dessous. Construire à partir d'une grille initiale I donnée une grille finale F telle que : (K) toute case de F contient une et une seule fois l'un des chiffres 1 à 9 ; (L) toute ligne de F contient une et une seule fois chacun des chiffres 1 à 9 ; (C) toute colonne de F contient une et une seule fois chacun des chiffres 1 à 9 ; (B) tout bloc de F contient une et une seule fois chacun des chiffres 1 à 9 ; (I) toute case de I remplie conserve la même valeur dans F. À ces cinq règles, il convient donc d'ajouter implicitement que la grille F existe et est unique. On peut remarquer que les quatre premières conditions (K), (L), (C) et (B) présentent de la redondance d'un point de vue logique, mais cette redondance s'avère utile pour déduire plus facilement de nouveaux faits permettant de remplir la grille. Représentation d'une grille de sudoku Une grille est représentée par un tableau a deux dimensions a 9 lignes et 9 colonnes numérotées chacune de 0 a 8. Elle est découpée en 9 blocs numérotés également de 0 a 8 dans l'ordre de lecture de gauche a droite et de haut en bas et les 9 cases d'un bloc donné sont également numérotées de 0 a 8 selon le même procédé. Ainsi, la même case d'une grille peut être référencée de deux manières différentes : pour (i, 3) EUR [[0, 8]]2, on appelle case d'indice (i, ]) la case de la grille située a l'intersection de la ligne i et de la colonne j ; pour (b, 7") EUR [[0, 8]]2, on appelle case de bloc (b,r) la case de la grille située dans le bloc numéro 19 ayant le numéro 7". Une case non encore remplie est affectée de la valeur 0. La figure 1 a droite représente le tableau correspondant a la grille initiale donnée a gauche, dans laquelle le bloc numéro 3 est grisé. Les éléments du bloc grisé de numéros 0, 1, 2, 3, 4, 5, 6, 7 et 8 sont donc respectivement affectés des valeurs 0, 1, O, O, O, 7, 6, 0 et 0. La case d'indice (5,0) est aussi la case de bloc (3,6) : elle est grisée de manière plus foncée. -- Caml Une grille de sudoku est représentée par un tableau défini par make_matrix 9 9 0 ; pour (i, 3) EUR [[0, 8]]2, l'accès a la case d'indice (i,j) d'un tel tableau T se fait par l'expression T. (i) . (j). -- Pascal Une grille de sudoku est représentée par un tableau rectangulaire array [O. .8,0. .8] of integer ; pour (i,j) EUR [[0, 8]]2, l'accès à la case d'indice (i,j) d'un tel tableau T se fait par l'expression T[i,j]. Préliminaires On commence par écrire quelques fonctions qui seront utiles dans les parties suivantes. I .A -- Écrire une fonction appartient d'appartenance d'un élément a une liste. I .B -- Écrire une fonction supprime de suppression de toutes les occurrences d'un élément dans une liste. I. C' -- Écrire une fonction ajoute d'ajout d'un élément dans une liste sans redondance (si l'élément appartient déjà à la liste, on renvoie la liste sans la modifier). I.D -- Écrire une fonction/ procédure indice qui, étant donné un couple (b,r) EUR [[0, 8]]2 correspondant a la case de bloc (b, 7") dans une grille, renvoie l'indice (i, j) de cette case dans la grille. Cette fonction pourra utiliser judicieusement les quotients et restes de divisions euclidiennes par 3 et on justifiera les formules utilisées. Par exemple, la case de bloc (3,6) est la case d'indice (5,0) (c'est la case grisée en plus foncé dans la figure 1) : indice appliqué au couple (3, 6) doit donc renvoyer le couple (5,0). -- Caml La fonction aura pour signature indice : int * int --> int * int = < fun > On rappelle que pour deux entiers a et b, les expressions a quo b et a mod b calculent respectivement leur quotient et leur reste dans la division euclidienne. -- Pascal La procédure aura pour en--tête procedure indice (b, r : integer ; var i , j : integer) ; et modifiera la valeur des entiers i et j. On rappelle que pour deux entiers a et b, les expressions a DIV b et a MOD b calculent respectivement leur quotient et leur reste dans la division euclidienne. II Codage de la formule initiale Représentation des formules logiques Dans tout le problème, A, V et fi dénotent respectivement les connecteurs de conjonction, de disjonction et de négation. Etant donné un ensemble V de variables propositionnelles, on considère l'ensemble 5" des formules logiques construites a partir de V et de l'ensemble de connecteurs {A, V, o}. 2014--03-11 11:16:53 Page 2/7 OE=C BY-NC-SA Une valuation sur V est une application 0 : V --> [B (où [B : {vrai, faux} désigne l'ensemble des booléens) ; cette application 0 s'étend en une application Eva : 5" --> [B, attribuant une valeur de vérité a toute formule F E 5" sous la valuation a. Une formule logique F est satisfiable s'il existe une valuation 0 telle que Eva(F) : vrai. Deux formules logiques F et G sont équivalentes si EvU(F) : Eva(G) pour toute valuation a, et on note alors F E G . Un littéral est une formule logique réduite a 19 ou a = p, où 19 est une variable propositionnelle. Une clause est une formule logique écrite sous la forme d'une disjonction de littéraux. La clause vide est la clause ne contenant aucun littéral, elle est notée J. et est considérée comme non satisfiable. Une clause unitaire est une clause réduite à un seul littéral ; une clause unitaire positive (respectivement négative) est une formule logique réduite à 19 (respectivement à =p), où 19 est une variable propositionnelle. Une formule en forme normale conjonctiue est une formule logique écrite sous la forme d'une conjonction de clauses. La formule vide est la formule ne contenant aucune clause, elle est notée D et est considérée comme satisfiable. Dans tout le problème, les variables propositionnelles sont indexées par un triplet d'entiers (i, j, k) et notées OElî',j)? avec la sémantique suivante: pour un triplet (i, j,k) EUR [[0,8]] >< [[0,8]] >< [[1,9]], une valuation 0 assigne la valeur vrai a OE(ki,j) lorsque la case d'indice (i, j) de la grille de sudoku contient la valeur k. L'ensemble V utilisé dans le problème est donc constitué des 93 = 729 variables propositionnelles oe(k [[0,8]]2 >< [[1,9]]. À titre d'exemples : -- la clause oe(5070) V OE(5078) V OE(58,0) ...), où (i,j, k) parcourt Voe5 (s s) exprime qu'une au moins des quatre cases situées aux coins de la grille est occupée par un 5 ; 8 9 -- la formule sous forme normale conjonctive /\ (V :Ul'î ?)) exprime que chacune des valeurs de la colonne 7 i=O k=1 ' est constituée de chiffres compris entre 1 et 9 ; 8 -- la clause \/ oeY' 1ndice(3,j) exprime que l'une des cases du bloc numéro 3 de la grille contient le chiffre 6 (où j=0 indice est la fonction/ procédure de la question LD). 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 oe(7178) /\ (ÇUÊOA> V = æ(5277 listes ( ( (1,8, 7) ) ; ( (O, 4, 3) ; (2, 7,5) ) ) (où un triplet surligné désigne un littéral négatif). Plus précisément : )) est représentée formellement par la liste de -- Caml On déclare le type litteral comme suit : type litteral = X of int * int * int | NonX of int * int * int; ; Dans un triplet d'entiers de type int * int * int, le premier élément correspond au numéro de ligne, le second au numéro de colonne et le troisième a la valeur comprise entre 1 et 9. Une clause est de type litteral list et une formule logique (en forme normale conjonctive) de type litteral list list. -- Pascal On déclare le type litteral comme suit : type litteral = record signe : boolean; i : integer; j : integer; k: integer end; On dispose d'une fonction litt(signez boolean; i: integer; j : integer; k: integer) : litteral qui permet de créer des littéraux. Par exemple litt (true , 0 , 0 , 9) renvoie le littéral OEÊO,O) et litt (false , (21,4 listes pour lesquelles on dispose des primitives usuelles suivantes : -- Nil qui est la liste vide ; on peut tester si une liste 1 est vide avec l'expression l=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(fl : 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. 1, 4, 2) renvoie le littéral _'£C ). On suppose qu'on a défini les types clause et formule comme des On suppose que l'on peut tester l'égalité de deux littéraux 11 et 12 a l'aide de l'expression 11 = 12. Cette opération n'est pas disponible pour les clauses et les formules. 2014--03-11 11:16:53 Page 3/7 OE=C BY-NC-SA Avant de décrire des stratégies de résolution d'une grille de sudoku, on va coder l'information contenue dans la grille initiale par une formule logique en forme normale conjonctive. Oe codage se fait en deux temps : on code déjà la règle générale du jeu, représentée par les quatre règles logiques (K), (L), (O) et (B) ; puis on code l'information propre a la grille initiale fournie, qui repose sur la cinquième règle (1). II.A -- Formule logique décrivant la règle du jeu On s'intéresse dans cette partie a coder par une formule logique en forme normale conjonctive l'information fournie par la règle du jeu. Chacune des quatre règles logiques (K), (L), (O) et (B) peut être scindée en deux sous-régles : (K1) toute case de F contient au moins une fois l'un des chiffres 1 a 9 ; (L1) toute ligne de F contient au moins une fois chacun des chiffres 1 a 9 ; (O1) toute colonne de F contient au moins une fois chacun des chiffres 1 a 9 ; (B1) tout bloc de F contient au moins une fois chacun des chiffres 1 a 9 ; (K2) toute case de F contient au plus une fois l'un des chiffres 1 a 9 ; (L2) toute ligne de F contient au plus une fois chacun des chiffres 1 a 9 ; (O2) toute colonne de F contient au plus une fois chacun des chiffres 1 a 9 ; (B2) tout bloc de F contient au plus une fois chacun des chiffres 1 a 9. II.A.1) le a ) Pour (i, J') E [[0, 8]]2, écrire une clause qui traduit la phrase mathématique : 3 [EUR EUR [[1, 9j], :c< [[1, 9j], exprimer mathématiquement le fait que la ligne de numéro i de la grille contient au plus une fois la valeur [{ et écrire une formule en forme normale conjonctive qui traduit cette condition. b) En déduire une phrase mathématique qui traduit la condition (L2) et une formule L2 en forme normale conjonctive qui exprime (L2). c} Déterminer le nombre de clauses que contient L2. d) Écrire une fonction lig2 qui renvoie la liste qui représente la formule logique L2. II.A.5) Obtenir de même des formules logiques C 2, B 2 et K 2 exprimant les conditions (O2), (B2) et (K2). On suppose avoir écrit des fonctions lig1, c011, case2, col2 et bloc2 qui renvoient respectivement les listes qui représentent les formules logiques L1, Cl, K 2, C 2 et B 2. =K1AL1AC1ABlAK2AL2AC2AB2:F On pose alors Frègle règle est la formule logique en forme normale conjonctive décrivant la règle du jeu. Elle contient 11988 clauses. II.B -- Formule logique décrivant la grille initiale On s'intéresse dans cette partie a coder par une formule logique en forme normale conjonctive l'information fournie par la grille initiale à compléter. On pourrait pour cela se contenter de considérer une formule logique F construite à partir de la cinquième règle (1) donnée au début de l'énoncé: pour toute case de la grille d'indice (i, j) initialement remplie par la valeur k EUR [[1, 9]], on considère la clause réduite au littéral positif OE(ki,j) et, si r est le nombre de cases remplies dans la grille initiale, on pose F comme étant la conjonction des r clauses ainsi obtenues. Mais, pour accélérer la phase d'inférences logiques qui sera menée dans la partie 111, on n'hésite pas a introduire a nouveau de la redondance en déduisant d'emblée un certain nombre de faits que l'on ajoute à la formule F liée à la grille initiale. Ces nouveaux faits sont de deux ordres : -- si dans la grille initiale, la case d'indice (i, j) est déjà remplie par la valeur [EUR EUR [[1, 9]], on peut considérer d'emblée, en plus de la clause unitaire positive oeâgj) (déjà prise en compte par la formule F ci--dessus), les 8 clauses unitaires négatives _IOE(i,j) avec l EUR [[1, 9]] \ {lc} ; on enrichit ainsi la formule F en une formule F1 2014--03-11 11:16:53 Page 4/7 OE=C BY-NC-SA 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, ]) 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 [{ EUR [[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 [{ est interdite pour la case d'indice (i, 3), on peut donc considérer la clause unitaire négative fioe,'Y,,j) ; ainsi, pour la case d'indice (1, 3) de l'exemple de la figure 1 a 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 fioe,2, 3), fioeÎ, 3), fi OEÎ,,3), _'OE(5173), _'ÇC(7173) et _'OEÊ3173) ; on note alors F2 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 Fg : F1 /\ F2. rille II.B.1) Écrire une fonction donnees qui, a partir d'une grille de sudoku initiale (donnée sous la forme d'un tableau), renvoie la formule F,, toujours sous la forme d'une liste de listes de littéraux. II.B.2) a ) Étant donnée une case d'indice (i, 3) EUR [[0, 8]]2, exprimer en fonction de i et j le numéro de bloc 19 EUR [[0, 8]] auquel cette case appartient. b) Écrire une fonction interdites_i j qui, étant données une grille de sudoku initiale et une case d'indice (i, ]) non remplie de la grille initiale, renvoie la conjonction des clauses unitaires négatives correspondant aux valeurs interdites pour la case d'indice (i, j). e} Écrire une fonction interdites qui, a partir d'une grille de sudoku initiale, renvoie la formule F2. II.B.3) Montrer que le nombre de clauses de la formule F% est majoré par 729. rille Formule initiale complète D'après II.A et HB, la formule logique a associer à une grille initiale qui code a la fois les informations qu'elle contient et qui peut permettre de la resoudre est donc F,,,,,,aoe : g,...e /\ Frèg,e. On supposera dans la partie III avoir écrit une fonction formule_initia1e qui, a partir d'une grille initiale, renvoie la formule F,n,t,a,e. -- Caml Cette fonction a pour signature : formule_initiale : int vect vect --> littera1 list list = < fun > -- Pascal Cette fonction a pour en--tête : function formule_initia1e (t : array of integer) : formule; III Résolution d'une grille de sudoku III.A -- Règle de propagation unitaire Nous supposons désormais que nous disposons d'une formule F, en forme normale conjonctive encodant un sudoku. Pour le résoudre on cherche à satisfaire F, nitiale nitiale' III.A.1) Combien existe--t--il de valuations satisfaisant F,,,,,,aoe ? III.A.2) Déterminer le nombre de lignes de la table de vérité de F, Il semble donc illusoire de construire une telle table de vérité en un temps raisonnable. Nous proposons donc une méthode qui n'est pas assurée de conclure dans tous les cas mais qui utilise un nombre polynomial d'opérations. nitiale' Soit F une formule en forme normale conjonctive. On suppose que F contient une clause unitaire réduite au littéral l. Un tel littéral est appelé littéral isolé. Nous pouvons alors simplifier la formule F de la manière suivante : -- en supprimant toutes clauses de F qui contiennent l ; -- en supprimant fil de toutes les clauses de F (ainsi si une clause ne contient que fil elle est remplacée par la clause vide J.) Par exemple la formule F = (n OE(30,2)) /\ (fiOEÊ'072) V OE(6275) fi OEÎO 2). En simplifiant F par ce littéral, on obtient la formule F ' : fi oe ) /\ (513,3072) V fioe,7174)) contient un unique littéral isolé 7 (174)' 2014--03-11 11:16:53 Page 5/7 OE=C BY-NC-SA III.A.3) On justifie formellement cette simplification. Soit F une formule en forme normale conjonctive conte-- nant un littéral isolé Z (associé à la variable propositionnelle p : on a donc Z = 19 ou l : pp). F peut s'écrire alors sous la forme F : Z /\ F1 /\ F2 /\ F3, où : -- F1 est une formule constituée de clauses contenant chacune le littéral Z ; -- F2 est une formule constituée de clauses contenant chacune le littéral fil et ne contenant pas le littéral l ; -- F3 est une formule constituée de clauses ne contenant chacune ni le littéral Z, ni le littéral fi Z. Remarquons que chacune des formules F1, F2 et F 3 peut être réduite à la formule vide, satisfiable. La formule simplifiée de F par le littéral Z est alors la formule F' : F2' /\ F3, où F2' s'obtient a partir de F2 en supprimant toutes les occurrences du littéral fil dans chacune des clauses de F2. Soit 0 une valuation de V \ {p}. Montrer que o satisfait F' si et seulement s'il existe une valuation 5 de V prenant les mêmes valeurs que 0 sur V \ {p} qui satisfait F. On précisera la valeur de Ü(p). L'algorithme de résolution du sudoku que nous proposons est appelé algorithme de propagation unitaire et consiste à appliquer la simplification présentée ci--dessus de manière répétée tant que l'on peut déduire de nouveaux littéraux isolés. III.A.4) Appliquer l'algorithme de propagation unitaire a la formule _ 4 6 7 1 6 F _ ælo,o) A (OE(2,2) V OE(3,6) V OE(7,7)l A (O OE(070) V fioe(376>) III.A.5) a ) Sur l'exemple de la figure 1, déterminer la valeur ko de la case d'indice (O, 7) dans la grille finale en raisonnant a la manière d'un joueur de sudoku (le raisonnement suivi sera décrit). b) Retrouver le résultat ko de la question précédente en appliquant l'algorithme de propagation unitaire, c'est--à--dire montrer que l'on peut, au terme d'un certain nombre de simplifications a partir de la formule F. 1nitiale associée à cette grille initiale, déduire le littéral isolé æ(k007 160 (0,7)' ). On ne select10nnera dans la formule Finitiale que des clauses utiles à l'obtention du littéral isolé oe III.A.6) Écrire une fonction nouveau_lit_isole qui, a partir d'une formule F, renvoie un littéral isolé de F. Si F ne contient pas de tel littéral, la fonction renverra le littéral a:(__1 _1) qui n'est pas utilisé comme variable propositionnelle par ailleurs. III.A.7 ) Écrire une fonction simplification qui, a partir d'un littéral Z et d'une formule F, renvoie la formule simplifiée F' après propagation du littéral Z dans F. III.A.8) Écrire une fonction propagation qui, a partir d'un tableau t représentant le sudoku et d'une formule F représentant les contraintes du sudoku, renvoie la formule obtenue par propagation unitaire. Cette fonction modifiera le tableau t quand de nouveaux littéraux isolés découverts au cours de l'algorithme permettent de déduire la valeur d'une case du sudoku. III.A.9) Que peut--on dire sur le tableau modifié t et la formule renvoyée par la fonction propagation dans le cas où l'algorithme de propagation unitaire permet de résoudre le sudoku ? Et dans le cas où il ne permet pas de le résoudre ? III.A.10) On appelle taille d'une formule F le nombre total de littéraux apparaissant dans ses clauses. Évaluer le nombre d'opérations effectuées par les fonctions nouveau_lit_isole, simplification, puis par la fonction propagation quand elles s'appliquent à une formule de taille n. On donnera une estimation de la forme 0( f (n)) que l'on justifiera. III.B -- Règle du littéral infructueuoe On décrit maintenant une autre méthode de déduction plus puissante combinant la propagation unitaire et une opération appelée règle du littéral infractaeaæ décrite ci--dessous. Étant donné une formule F en forme normale conjonctive et une variable propositionnelle oe, -- si l'algorithme de propagation unitaire appliqué a la formule F /\ p :o permet de déduire la clause vide alors on ajoute la clause at à F ; -- si l'algorithme de propagation unitaire appliqué à la formule F /\ oe permet de déduire la clause vide alors on ajoute la clause fi:c à F. III.B.1) Justifier formellement que si l'on peut déduire la clause vide a partir de la formule F /\ _'£C alors F E F /\ oe. III.B.2) Écrire une fonction variables qui, a partir d'une formule, renvoie la liste de ses variables sans doublons. On supposera qu'on dispose d'une fonction flatten qui a 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) }. 2014--03-11 11:16:53 Page 6/7 OE=C BY-NC-SA III.B.3) Écrire une fonction deduction qui, a partir d'un tableau, d'une variable 55 et d'une formule F , renvoie 1 si la règle du littéral infructueux permet d'ajouter la clause :c a F, --1 si elle permet d'ajouter la clause fi r à F et 0 sinon. On supposera qu'on dispose d'une fonction copier_matrice qui a 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 ce ou fi oe. 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, a partir d'un tableau t représentant le sudoku et d'une formule F représentant les contraintes du sudoku, met en oeuvre 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, a 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. Eæpérimentalement, la règle de propagation unitaire permet de résoudre les sudokus les plus faciles et environ la moitié des sudo/ms les plus difficiles. A notre connaissance, il n'eæiste pas de sudoku ne pouvant être résolu intégralement à l'aide de la règle du littéral infructueuæ. oooFlNooo 2014--03-11 11:16:53 Page 7/7 OE=C BY-NC-SA

Extrait du corrigé obtenu par reconnaissance optique des caractères


 Centrale Informatique MP 2014 -- Corrigé Ce corrigé est proposé par Vincent Puyhaubert (Professeur en CPGE) ; il a été relu par Benjamin Monmege (ENS Cachan) et Guillaume Batog (Professeur en CPGE). L'épreuve d'informatique du concours Centrale s'intéresse cette année au jeu populaire du sudoku. Il permet d'écrire deux fonctions permettant de trouver la solution en pratique de manière quasi-systématique. La construction de ces fonctions passe par le codage d'une occurrence du jeu par une fonction booléene imposante (environ 12 000 clauses, et la bagatelle de 729 variables propositionnelles). On utilise alors essentiellement le cours de logique pour simplifier cette formule et en déduire la solution du sudoku. · La première partie demande d'écrire quelques fonctions élémentaires de manipulation de listes. Elle ne doit poser aucune difficulté. · La deuxième partie a pour objectif de traduire les règles du jeu, puis le remplissage initial de la grille, par une formule booléenne sous forme normale conjonctive. La partie théorique consiste simplement à recenser un certain nombre de contraintes. La programmation est franchement plus rébarbative puisqu'il faut parfois imbriquer jusqu'à quatre boucles. · La dernière partie concerne la résolution du jeu. Elle utilise l'argument simple consistant à dire qu'une conjonction de la forme x F avec x un littéral n'est satisfaite que si x est satisfait, et qu'alors F est équivalente à une formule F où x et son complémentaire ont disparu. On en déduit une première méthode de résolution par simplifications en chaîne, suivie d'une seconde qui utilise un test supplémentaire pour poursuivre lorsque la première méthode ne permet pas de conclure. L'épreuve dans son ensemble est bien rédigée, l'auteur faisant preuve d'un gros effort de pédagogie. Si vous avez toujours rêvé de faire résoudre vos sudokus par la machine, ce sujet est à travailler sans hésiter. Cependant, on peut regretter que les chapitres abordés dans cette épreuve soient réduits au cours de logique, c'est-à-dire une fraction très restreinte du programme de prépa. Indications Partie I I.A Rédiger une fonction récursive. Faire de même pour les deux questions suivantes. I.D Commencer par regarder ce qui se passe dans une matrice 3 × 3 dont les cases sont numérotées dans l'ordre de l'énoncé. Partie II II.A.1.a Utiliser une disjonction de 9 littéraux. II.A.1.b Quantifier la phrase mathématique obtenue à la question précédente. II.A.1.c Écrire K1 comme une conjonction de clauses de la forme de la question II.A.1.a. II.A.1.e Utiliser une référence sur une liste complétée au fur et à mesure à l'aide de boucles. On pourra écrire la fonction en deux temps à l'aide d'une première fonction qui construit les clauses de la formule. II.A.2 Même technique qu'à la question II.A.1. II.A.3.a Pour la formule B1, utiliser le fait que les variables associées au bloc d'indice b sont indexées par indice(b, r) pour r [[ 0 ; 8 ]]. II.A.3.b Utiliser les mêmes idées qu'à la question II.A.1.e. II.A.4.a Traduire la propriété par le fait que deux cases différentes de la ligne i ne peuvent contenir la valeur k simultanément. II.A.4.b Considérer la conjonction de toutes les formules de la question précédente. II.A.4.d Utiliser quatre boucles for imbriquées. II.A.5 Adapter la formule obtenue pour L2 à la question II.A.4.b. II.B.1 Commencer à nouveau par construire une fonction qui crée la conjonction des littéraux définissant la condition initiale : « la case (i, j) contient la valeur k et aucune autre valeur ». II.B.2.a Définir la fonction réciproque de celle de la question I.D. II.B.2.b Utiliser une référence sur une liste initialement vide, et ajouter à cette liste une clause ¬xp(i,j) pour chaque valeur p de T non nulle contenue dans la même ligne, la même colonne, et le même bloc que la case d'indice (i, j). II.B.2.c Concaténer les listes obtenues à l'aide de interdites_ij pour les couples (i, j) tels que T.(i).(j) est nul. II.B.3 Remarquer que Fgrille ne contient jamais un littéral et son complémenté. Partie III III.A.1 Comparer le nombre de valuations satisfaisant Finitiale et le nombre de solutions au sudoku. III.A.2 Déterminer le nombre de valuations de n variables propositionnelles. III.A.3 Remarquer qu'une valuation satisfaisant F doit nécessairement attribuer une valeur à p qui satisfait le littéral . III.A.5.a Déterminer une valeur parmi {1, 2, 3, 4, 7, 9} ne pouvant se trouver nulle part ailleurs qu'en case (0, 7). III.A.6 Écrire un programme qui renvoie le littéral contenu dans la première clause trouvée à un seul élément dans F. III.A.7 Renvoyer à partir de la liste des clauses de F une liste obtenue récursivement en supprimant (resp. modifiant) celles qui contiennent (resp. ¬ ). III.A.8 Appliquer récursivement les simplifications jusqu'à obtenir une formule sans littéral isolé. III.A.10 Vérifier que les fonctions nouveau_lit_isole et simplification parcourent un nombre borné de fois chaque clause. III.B.1 Remarquer qu'une formule contenant une clause vide n'est pas satisfaisable, et que par ailleurs, F (F x) (F (¬ x)) pour toute formule F et tout littéral x. III.B.2 Utiliser la fonction flatten pour récupérer les littéraux d'une formule (et non pas les variables comme le demande l'énoncé). III.B.3 Ajouter x à la formule F et simplifier cette nouvelle formule (penser à utiliser une copie de T). Vérifier ensuite si la liste vide appartient au résultat. III.B.4 Définir une fonction qui cherche parmi les littéraux apparaissant dans F si l'un d'entre eux réussit le test de la règle du littéral infructueux. I. Présentation du jeu de sudoku I.A La structure de liste se prête naturellement à une fonction récursive, qui peut s'écrire de la manière suivante : let rec match [] -> |t::q appartient x l = l with false -> (t=x) || appartient x q ;; La fonction appartient est déjà prédéfinie en Caml sous le nom mem. Pour autant, l'énoncé demande clairement de la redéfinir. On notera que la signature de cette fonction est 'a -> 'a list -> bool. La fonction est dite polymorphe, ce qui signifie qu'elle peut s'appliquer à n'importe quelle liste, indépendamment du type des éléments qu'elle contient. I.B Il suffit à nouveau d'écrire une fonction récursive. let rec match [] -> |t::q supprime x l = l with [] -> if t=x then supprime x q else t::supprime x q;; I.C La fonction appartient permet de tester si l'élément x que l'on veut ajouter à la liste l s'y trouve déjà. Il n'y a plus qu'à renvoyer la bonne liste en fonction du résultat du test. let ajoute x l = if appartient x l then l else x::l;; I.D Commençons par regarder ce qu'il se passe au sein d'une matrice de taille 3 × 3 dont les éléments sont numérotées selon l'ordre de l'énoncé : 0 1 2 0 0 3 6 1 1 4 7 2 2 5 8 Si r est le numéro d'une case, on constate alors que ses indices de ligne et de colonne sont respectivement donnés par le quotient et le reste de la division euclidienne de r par 3. On en déduit les formules suivantes : la case de bloc (b, r) dans une grille est celle d'indice (i, j) avec i = 3 · b1 + r1 et j = 3 · b2 + r2 avec (b1 , b2 ) (respectivement (r1 , r2 )) les quotients et restes de la division euclidienne de b (respectivement r) par 3. Cela permet d'en déduire la fonction suivante : let indice (b,r) = (3*(b quo 3)+(r quo 3), 3*(b mod 3)+(r mod 3));;