Home

Principe Général

Un plateau de jeu de squaro vierge ressemble à ceci :

O---O---O---O
| 3 | 2 | 2 |
O---O---O---O
| 2 | 1 | 1 |
O---O---O---O
| 1 | 0 | 1 |
O---O---O---O

C'est une grille de taille n*n, ou chaque case contient un nombre compris entre 1 et 4 (inclus). Ce nombre entier désigne le nombre de coins de la cases (modélisés ici par des O) qui devrons être noircis à l'état final. Si on représente les coins (appelés pixels par la suite) noirs par '@' et les pixels blancs par 'O', on aura pour cette grille à l'état final l'exemple suivant :

@---O---@---@
| 3 | 2 | 2 |
@---@---O---O
| 2 | 1 | 1 |
O---O---O---@
| 1 | 0 | 1 |
@---O---O---O

Modélisation d'un plateau

Le plateau est modélisé au sein du programme comme une superposition de deux "sous-plateaux" :

• la grille carrée de taille n représentant les cases portant les entiers de 1 à 4
• la grille carrée de taille n+1 représentant les pixels noirs ou blancs : ce sont des booléens.

On conviendra que le pixel est noir si et seulement si sa valeur booléenne est différente de 0 (valeur VRAI).

Un programme de génération aléatoire de plateaux résolubles est rédigé. Il défini aléatoirement chaque pixel comme noir ou blanc. ensuite il compte pour chaque case le nombre de pixels noirs dans les coins. Cette valeur devient celle de la case. Puis on réinitialise la grille de pixels (tous blancs). Ainsi on est sûr que la grille est résoluble.

Format de fichier plateaux

On défini un format de fichier pour représenter un plateau de manière permanente. L’extension utilisée sera par convention .plt, et le format sera tel l'exemple suivant :

Exemple_plateau.plt :

3
322
211
101
1011
1100
0001
1000

Cet exemple est la description de la précédente grille complétée.

• première ligne : Taille de la grille (n).
• lignes 2..(n+1): chaque caractère est un entier décrivant une case.
• lignes (n+2)..fin: de même avec les pixels

Modélisation Logique

Le but du squaro étant de remplir la grille de pixels en relation avec les valeurs des cases, nous prenons comme variables les (n+1)² booléens formant cette grille. Comme nous l'avons spécifié précédemment, la variable xi vaut VRAI si et seulement si le pixel est noir.

Nous définissons au sein du programme des structures de données permettant de travailler sur des éléments de logique :

• Clauses
• Formes normales conjonctives
• Assignations

Pour plus d'informations sur la manière dont le programme calcule la modélisation logique d'un plateau, voir CalculsCNF.md

L'algorithme DPLL est implémenté pour permettre de savoir si un ensemble de clauses est satisfaisable et mettre en évidence un modèle dans le case où l'ensemble est sat.

Format DIMACS

Le format de fichier permettant de sauvegarder des ensembles de clauses utilisé est DIMACS. Nous réalisons un programme prenant en entrée un fichier de plateau (.plt) et écrivant en sortie un fichier DIMACS décrivant ledit plateau. Ce fichier contient un ensemble de clauses dont les variables sont les (n+1)² pixels de la grille.

Nous pouvons alors appliquer DPLL à cet ensemble de clauses en utilisant les éléments de logique implémentés et en déduire si le plateau est résoluble et dans ce cas de donner une assignation pour les pixels.

Programmes mis en jeu

Le projet est ainsi découpé en plusieurs programmes permettant chacun de faire une tâche précise. Ces programmes sont :

• Génération aléatoire de plateaux
• Génération de fichier DIMACS pour un plateau
• Réduction en problème 3-SAT
• Résolution du problème par une implémenation de DPLL
• Résolution du problème par MiniSat
• Script ou programme principal permettant de gérer ces programmes à partir d'un menu (Guide).