Le sudoku est un jeu en forme de grille défini en 1979 et inspiré du carré latin ainsi que du problème des 36 officiers du mathématicien suisse Leonhard Euler. Le but du jeu est de remplir cette grille avec des chiffres allant de 1 à 9 en respectant certaines contraintes. Ce jeu va nous permettre d'illustrer la réduction d'un problème à SAT.
Le formalisme
Un problème SAT est représenté au moyen de 
variables propositionnelles
qui peuvent prendre la valeur 
(faux) ou 
(vrai).
On appelle littéral une variable 
ou son complément 
.
Une clause est une disjonction de littéraux (par exemple (
ou 
) ou encore (
ou 
)).
Une formule logique sous forme normale conjonctive (CNF) est une conjonction de clauses.
Un littéral qui a la valeur est dit satisfait. Une clause est satisfaite si l'un de ces littéraux l'est. Une formule est satisfaite si toutes ses clauses le sont.
Le problème SAT est un problème NP-complet (d'après le théorème de Cook) qui consiste à dire s'il existe ou non une combinaison de valeurs pour les littéraux d'une formule donnée, telle que ces valeurs satisfont cette formule.
Exemple 1
Soient
des variables propositionnelles. Soit l'expression
.
Pour cet exemple simple, il est possible de déterminer les valeurs de toutes les variables par simples déduction. En effet, on s'aperçoit que 
vaut , on peut donc déduire 
de
et trouver que vaut . Ainsi, on peut en déduire 
à partir de
et trouver que vaut .
Cette résolution très simple n'est bien sûr pas applicable à tous les coups. Dans l'exemple, chaque valeur des variables pouvait se déduire. Dans le cas général, il faudrait développer l'arbre de recherche.
Exemple 2
Ce problème consiste à déterminer s'il est possible de placer pigeons dans 
pigeonniers, un pigeonnier ne pouvant être occupé au plus que par un seul pigeon.
Pour modéliser ce problème, on utilise 
variables propositionnelles 
avec 
variant de à , et 
variant de à . Si est vraie alors le pigeon trouve dans le pigeonnier .
Ce problème, archétype des problèmes combinatoires, est intéressant et sa solution est évidente mais le résoudre peut demander un important temps de calcul :
, le problème est consistant et la recherche d'une solution se fait de manière linéaire sachant que le nombre de solutions (
) est exponentiel,
, le problème est inconsistant mais les algorithmes standard (du type Davis et Putnam) prouvent l'inconsistance en un temps exponentiel.
Le problème, écrit en fonction des clauses de cardinalité, s'exprime par :
Problème
SAT
Nombre de variables
pigeons 
Non
pigeons 
Non
pigeons 
Oui
Quelques méthodes de résolution
Les méthodes de saturation
Ces méthode effectuent des tests de consistance locale pour détecter l'incohérence de la base de clauses. Elles essaient de prouver l'inconsistance de l'ensemble de clauses en réfutant (démontrant la fausseté) une d’elles.
On pourra notamment citer l'algorithme SL-Resolution.
Les algorithmes énumératif
Ces algorithmes consistent en une exploration systématique de l'ensemble des interprétations afin de déterminer si l’une d'entre elles est un modèle. Cette procédure peut aisément être assimilée à une forme de résolution que l'on nomme résolution dirigée.
On pourra notamment citer la célèbre procédure de Davis et Putnam.
La recherche locale
Ces méthodes commencent à donner des valeurs à chaque variables puis vont en modifier certaines itérativement de façon à réduire le nombre de clauses non satisfaites.
On pourra notamment citer le célèbre recuit-simulé.
L'approche programmation par contrainte (PPC)
Cette méthode consiste à programmer avec des relations appelées « contraintes''. Un problème comporte un certain nombre de variables, chacune ayant un domaine, et un certain nombre de contraintes. Trouver une solution à un problème de PPC consiste à décrire l'ensemble des affectations autorisées de chaque variable, de telle sorte que la totalité des contraintes soient satisfaites.
On pourra notamment citer le célèbre algorithme « Branch And Bound''.
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 :
.
Le Sudoku possède plusieurs propriété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 
![$[1..n]$](http://www.bugywood.org/complexite_structurelle/img48.png){kind=small}
. 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 ![$[1,3]$](http://www.bugywood.org/complexite_structurelle/img53.png){kind=small}
remplie avec le chiffre 
.
Si on prend , il faudra
variables.
Les clauses et la formule
Pour effectuer la réduction, on va construire une formule basée sur 4 types de clauses :
Ces clauses peut être formalisées comme suit :
Les méthodes d'inférence possibles
Comme certaines cases sont préfixées, il est possible de réduire les règles définies plus haut en plaçant directement leurs valeurs. On peut également éliminer tout de suite les valeurs qui représentent des nombres égaux à une valeur préfixée qui se trouve sur la même ligne, la même colonne ou dans la même sous-grille.
Après cette étape on peut utiliser les méthodes de résolution vues à la section 1.
Dans ces quelques pages, nous avons vu la réduction du problème du sudoku à SAT et cet exemple nous à permit de mieux comprendre le mécanisme de réduction.
