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 SAT solver qui utilise comme donnée d'entré des assertions logique en FNC, comme dit plus haut. Ces données peuvent être fournit soit via l'entré par défaut du terminal, soit en lui donnant un fichier contenant les assertions, ou chaque saut de ligne correspond à un ET logique, et les espace entre les différentes variables, correspondent à des OU logiques, pour faire des négations on utilise le signe "~"