Polyominos, pavages et solveurs SAT

Étudiant : MALABRE Étienne Chercheur : HYVERNAT Pierre

Introduction au problème

Quel que soit notre âge, nous avons tous connu des jeux basés sur des blocs ou des cases à placer : sous forme de jeux vidéo pour certains, sous forme de briques pour d'autres. Souvent, une question se pose : Puis-je remplir cette forme avec cette pièce ?

Le problème de pavage correspond précisément à cette interrogation : on nous donne un ou plusieurs types de pièces, ainsi qu’une forme (ou grille), et il s'agit de déterminer s’il est possible de remplir entièrement cette forme avec les pièces fournies.

Dans notre cas, pour résoudre ce problème, nous utilisons un solveur SAT (ici, SAT13). Celui-ci prend en entrée une suite d'instructions logiques composées uniquement d’opérateurs ET, OU et NON, plus particulièrement sous la forme normale conjonctive (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

Cela correspond à :

(A ∨ B ∨ ¬C) ∧ (¬A ∨ D)

Représentation du problème

Pour représenter un problème de pavage :

1. Une forme (ou grille) est décrite dans un fichier tab.txt, où les cases utilisables sont indiquées par le caractère #.
2. Une pièce est décrite par une liste de coordonnées relatives, par exemple : [[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 en (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.

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

Exemple de pièce

Soit la pièce suivante :

piece = [[0,0], [0,1], [0,2], [1,2]]

Et une grille donnée dans le fichier tab.txt. En exécutant :

tab = lecteur_tab("tab.txt")
generates_clauses(piece, tab)

On obtient le fichier clausepavage.txt contenant les contraintes.

Le code complet est disponible sur le GitHub du projet.