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é

 :
👈 gratuite pour tous les corrigés si tu crées un compte
👈 l'accès aux indications de tous les corrigés ne coûte que 1 € ⬅ clique ici
👈 gratuite pour tous les corrigés si tu crées un compte
- - - - - - - - - - -
👈 gratuite pour ce corrigé si tu crées un compte
- - - - - - - - - - - - - - - - - - - - - - - - -

É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