Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

projet sudoku INF242

No description
by

Adrien Coquard

on 21 May 2012

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of projet sudoku INF242

Présentation INF242
Résolution de sudoku par Coquard Adrien
Couly Dorian
Duband Samuel
Portier Benoit Plan :
Présentation du problème
Les règles de logique
La programmation
Analyse des résultats 1/ Présentation du probléme Exemple simple : Trouver où est placé le chiffre 8 de la première ligne Il ne peut pas être sur la dernière case puisqu’il est déjà présent dans la dernière
colonne
Il ne peut pas non plus être dans la première ou troisième case puisqu'il est déjà
présent dans la première région
Il se place donc dans la sixième case A l’aide des chiffres déjà en place, il faut remplir la grille de façon à ce que les chiffres de 1 à 9 apparaissent une et une seule fois sur chaque ligne, chaque colonne et chaque région qui correspond à un carré de 3x3 cases .
Il existe différentes techniques pour résoudre les sudoku difficiles , il semble intéressant d'en décrire quelques unes Voici quelques techniques de résolution : Candidat unique mais pas seul : Un candidat n'est pas toujours seul dans une ligne, mais il peut être unique!
Dans cet exemple, vous pouvez constater que le candidat 4 n'est présent que dans une seule case de la ligne. C'est donc dans cette case que vous devez le placer. Et ensuite corriger l'indication de ce candidat dans les autres cases concernées de la grille. (région et colonne, dans cet exemple) Candidats identiques

Deux candidats, mais lequel choisir ?
Cette méthode ne donne pas la possibilité de répondre à la question du choix, mais donne la possibilité de supprimer des candidats indésirables. Car en effet, si deux cases ne contiennent que deux fois les mêmes candidats On peut être certain que ces deux candidats vont finalement terminer dans l'une et dans l'autre. Et donc supprimer ces candidats des autres cases de la ligne Quand il y en a pour 2, y en a pour 3!
Suivant le même principe Et finalement donc Cette méthode s'applique dans les cas suivants:
- avec 2 candidats dans 2 cases
- avec 3 candidats dans 3 cases
- avec 4 candidats dans 4 cases
...
- avec N candidats dans N cases Il existe aussi des sudoku n'ayant pas une taille de 9. Les plus classiques sont des
carrés d'entiers : 4,9,16,25... Ces cas la vont être solvables via le programme créé , en effet nous traiterons les cas jusqu'à 81.
Sachant que la valeur de la taille des petits carrés est la racine de la taille du sudoku 2/ Les règles de logique Comment savoir si un ligne, colonne et carré ne
possèdent qu'une et une seule fois chaque numéro ?

En comparant chaque case avec celles de la même colonne, ligne ou carré.
On prend x(i,j,n) vrai si la case de la i-ieme colonne et de la j-ième ligne contient la valeur 'n').
Il y aura donc taille*taille*taille de clauses ∧ ∧ Voici les règles de logique utilisés :

i ∀ j ∃ n [ x(i,j,n) ˄ x [¬(x=i) ˄ ¬ x(x,j,n)] ˄ y [¬(y=j) ˄ ¬ x(i,y,n)] ˄ z [¬(z=n) ˄ ¬ x(i,j,z)] ˄ f∀ g ∀ [¬ g=i ˄ ¬ f=j ˄¬ x(f,g,c)] ]

- case de coordonnées a , b sélectionné avec la valeur c
- pas deux fois le même chiffre sur la même ligne
- pas deux fois le même chiffre sur la même colonne
- pas deux chiffres sur la même case
- pas deux fois le même chiffre dans le même carré

Avec i,j,n,x,y,z compris entre 1 et la taille d'un coté de la grille ,
k: 1 et racine de la taille de la grille ;
g: ((i-1)/racine de taille)* racine de taille+k ;
f : ((j-1)/racine de taille)* racine de taille+k ;

g et f permettent de parcourir les cases du petit carré où il y a la case i,j. 3/ La programmation Le programme dimac_s :
./dimacs_s *grille_sudoku* *fichier_de_sortie*

Ce programme permet de traduire les règles de logique présentées précédemment . Soit la formule suivante pour comparer sur les colonnes :

[¬ x(1,1,1) ¬ x(1,2,1)] [¬ x(1,1,1) ¬ x(1,3,1)] [¬ x(1,1,1)
¬ x(1,4,1)] [¬ x(1,1,1) ¬ x(1,5,1)] [¬ x(1,1,1) ¬ x(1,6,1)]
[¬ x(1,1,1) ¬ x(1,7,1)] ...

Décrit par le bout de code suivant :
for i in 1..n_su*n_su loop - - pour toutes les colonnes
for j in 1..n_su*n_su loop - - pour toutes les valeurs
for k in 1..n_su*n_su loop - - pour toutes les lignes
for n in 1..n_su*n_su loop - - comparés aux autres valeur de la
if n > k then - - colonne (n>k car quand n<k le cas est deja traite) .
new_line(sortie_di);
put(sortie_di,(10000*i+100*k+j)*(-1)); - - soit l'une, soit l'autre ou
put(sortie_di,(10000*i+100*n+j)*(-1)); - - aucune des deux .
put(sortie_di,0);
end if;
end loop;
end loop;
end loop;
end loop;

Le bout de code utilisé pour les lignes utilise exactement la même structure ,
pour l'obtenir il suffit de modifier
put(sortie_di,(10000*i+100*k+j)*(-1)); - - soit l'une, soit l'autre ou
put(sortie_di,(10000*n+100*k+j)*(-1)); - - aucune des deux . resultat_di : ./resultat_di *fichier de sortie*
Via un fichier d'entiers généré par le sat_solveur ce programme affiche la solution de la grille si il y en a une.

Exemple avec le sudoku d'introduction: 4/ Analyse des résultats D’après ces résultats on peut clairement voir que Satzoo a résolu plus facilement les
sudokus lorsqu'ils ont un nombre élevé de chiffre initiaux. On en conclue
donc qu'il prend beaucoup de temps lorsqu'il doit mettre des chiffres aléatoirement dans la
grille. On voit que sans valeurs ajoutées la résolution de la grille est très rapide , cependant
dès qu'une valeur est ajoutée , l'ajout d'une valeur supplémentaire , jusqu'à plus 4 en tout cas ,
ne fait pas varier significativement le temps de résolution . Ces test ont pour but de déterminer si la place d'une valeur initiale ajoutée sur la grille
influe sur le temps de résolution , après les tests , il est clair que non . En effet le temps de
résolution de quatre grilles dont la diagonale est remplie avec une valeur ajouté , qui est
toujours la même , dans des cases différentes ne change pas significativement . Au cours des précédents tests , nous avons utilisé le sat-solveur Satzoo . Il nous a
semblé intéressant de comparer les performances de deux sat-solveurs différents , nous avons
donc demandé à un autre binôme le nom du sat-solveur qu'ils utilisaient : ligeling .
Comme vous pouvez le voir , le résultat du test est incontestable , ligeling est plus rapide que
Satzoo sur les résolutions de grille difficile , l'écart se creuse vraiment en augmentant la
difficulté .
A l'inverse , Satzoo est plus efficace lors de la résolution de grille facile .
Nous pensons que ligeling est plus efficace à remplir les cases vides , c'est à dire prendre une
décision de conditions initiales pour la résolution .
Format grille :

Le premier chiffre correspond a la taille d'un carré de la grille.
Son carré est donc égal a la taille de la grille elle même.

Puis pour remplir la grille il suffit d’écrire 0 lorsque la valeur de la case est inconnue et dans le cas contraire y inscrire la valeur. Ne pas oublier de mettre un espace entre chaque valeur pour que cela fonctionne bien.

Voici un exemple du format de grille utilisé durant notre projet :

3
0 0 0 0 4 3 5 0 0
0 1 0 0 0 0 2 0 0
0 7 5 0 0 0 0 6 0
1 0 7 2 5 0 4 0 0
0 0 0 1 0 0 0 0 6
0 5 4 0 0 9 0 0 2
0 0 0 0 2 5 0 0 0
0 0 0 0 0 8 1 0 5
5 4 8 0 0 0 0 2 7 Conclusion :

L'utilisation du sat-solveur est la solution la plus efficace dans la quête de la résolution des sudokus les plus difficiles .
En effet nous avons vu que celui-ci était plus efficace que les programmes codés dans les langages de haut niveau , surtout dans les grilles complexes ou de tailles importantes .
Cependant il existe des différences entre les sat-solveur eux mêmes .

Ce projet nous a permis de nous intéresser de plus près à la résolution de sudoku , en particulier aux règles de logique qui définissent ce jeu de plus en plus populaire , ainsi que de découvrir une des nombreuses utilisations d'un sat-solveur . Avec le même principe que pour les lignes et colonnes ,
il faut effectuer les vérifications suivantes :

Il n'y a pas deux fois la même valeur dans un carré
Il n'y a pas deux fois la même valeur dans une case
Il y a au moins une valeur dans chaque case

De plus , il faut prendre en compte les conditions initiales , c'est à dire donner la valeur vrai aux valeurs déja présentes dans la grille Comment , à partir d'un fichier grille qui sera décrit postérieurement ou d'un grille saisie à la main , arriver à une grille de sudoku résolue ? dimacs_s avec deux arguments
grille de sudoku au format prévu
nom du fichier dimacs de sortie sans argument
saisie de la taille de la grille
saisie de la grille via une partie graphique fichier dimacs décrivant les conditions initiales de la grille Satzoo commande à effectuer :
./Satzoo -print-model=1 dimacs:*le nom de votre fichier dimacs* > *fichier de sortie* fichier de sortie généré par Satzoo

Il faut ouvrir ce fichier et enlever toute la partie texte de celui ci , afin que le programme suivant puisse le lire correctement resultat_di Grille du sudoku initial
résolue
Full transcript