20/05/2007

Formalisation du problème du Sudoku pour la réduction à SAT

 

Le Sudoku

Une grille de Sudoku est composée de cases, avec un carré parfait (c'est à dire que l'on a ) et cette grille est elle-même divisée en sous-grilles. Généralement, on prend et . Au départ certaines cases sont remplies par des chiffres et d'autres sont vides. Le but du jeu est de remplir les cases vides en respectant les règles suivantes :

 

• On ne doit pas avoir deux chiffres identiques sur une même ligne
• On ne doit pas avoir deux chiffres identiques sur une même colonne
• Il ne doit pas y avoir deux chiffres identiques dans l'une des sous-grilles de taille .

 

Figure: Grille de sudoku

Le Sudoku possède plusieurs propriétés :

 

• Un problème de Sudoku ne possède qu'une seule solution
• Il est possible de résoudre un Sudoku en raisonnant, donc sans faire de recherche de toutes les possibilités.

 

Formalisation

Pour représenter le problème sous forme de problème SAT, nous avons besoin de beaucoup de variables booléennes (qui correspondent aux littéraux). En effet il faut variables avec , et . La variable sera vraie si et seulement si la case () contient la valeur . On a besoin de variables pour avoir chaque case et on multiplie une troisième fois par pour avoir chaque case remplie du symbole , avec , ce qui donne variables.

Par exemple : si est vraie, alors on a la case remplie avec le chiffre .

Si on prend , il faudra variables.