Polyominos, pavages et solveurs SAT
Étudiant: MALABRE Etienne
Chercheur: HYVERNAT Pierre
Introduction au problème
Quelque soit notre âge, nous avons tous connus des jeux à bases de blocs/cases à placer, sous forme de jeux vidéo pour certain, sous forme de briques pour d'autre. Souvent un problème ce pose, est ce que je peut remplir cette forme avec telle pièce ? Le problème de pavage est exactement, celui-ci, on nous donne un ou plusieurs type de pièce, et une forme, et on veut savoir si on peut remplir la dite forme avec les pièces données ?
Dans notre cas pour répondre à ce problème, on utiliseras un SAT solver (ici SAT13). Celui-ci prendra un suite d'instruction logique, composé donc uniquement de ET, OU et NON logique, et plus particulièrement en FNC
Utilisation de SAT13
SAT13 est un solveur qui accepte une formule logique en forme normale conjonctive (FNC), composée uniquement d'opérations ET, OU et NON. Plus précisément :
- Chaque ligne représente une clause (un OU logique entre plusieurs littéraux).
- L’ensemble des lignes est évalué comme un ET logique.
- Un littéral est soit une variable, soit sa négation (utilisant le symbole
~).
A B ~C ~A D
Ceci correspond à :
(A ∨ B ∨ ¬C) ∧ (¬A ∨ D)
Représentation du problème
Pour représenter un problème de pavage :
- Une forme (ou grille) est décrite dans un fichier
tab.txt, où les cases utilisables sont indiquées par le caractère#. - Une pièce est décrite par une liste de coordonnées relatives comme
[[0,0], [0,1], [0,2], [1,2]].
Nous générons alors toutes les clauses logiques qui modélisent :
- les positions valides des pièces,
- la contrainte que chaque case soit couverte au moins une fois,
- la contrainte qu'elle ne soit couverte qu'une seule fois,
- l’implication logique entre une pièce placée et les cases couvertes.
Lecture de la grille
def lecteur_tab(file: str) -> list:
...
Retourne la liste des coordonnées des cases utilisables dans la grille (les #).
Manipulation des pièces
trouve_origine(piece): Trouve le coin supérieur gauche de la pièce.placement_piece(origine, piece): Calcule la pièce translatée selon une origine.version_piece(piece): Retourne les 8 versions (rotations et symétries) d’une pièce.
Vérification de placements valides
def verif_version(origine, pieces, tab) -> list:
...
Retourne les versions valides de la pièce à une position donnée (qui restent dans la grille).
Génération de clauses
Clause de placement
def creation_clause_tab(piece, tab) -> str:
...
Exemple de clause :
~P0_2_1 C_3_1
(signifie : si la version 0 de la pièce est placée à (2,1), alors la case (3,1) est couverte)
Contrainte d’unicité
Empêche que deux pièces différentes recouvrent la même case.
def creation_contrainte_unicite(tab, piece) -> str:
...
Exemple :
~P1_0_1 ~P2_1_1
Contrainte de couverture
Impose qu’au moins une pièce couvre chaque case.
<scode> def creation_contrainte_couverture(tab, piece) -> str:
...
Exemple :
P0_0_0 P1_1_0
Clause de couverture complète
def creation_clause_complet(tab) -> str:
...
Assure que chaque case utile est bien prise en compte.
Exemple :
C_0_0 C_1_0 C_2_0
Soit la pièce suivante :
piece = [[0,0], [0,1], [0,2], [1,2]]
Et une grille donnée dans tab.txt. En exécutant :
tab = lecteur_tab("tab.txt")
generates_clauses(piece, tab)
On obtiendras le fichier clausepavage.txt avec les contraintes.
code complet disponible sur le github