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 `~`).