Systèmes Logiques
15 Janvier 2025
L’Énigme d’Einstein est une énigme, souvent attribuée à Einstein bien que cela soit peut probable, consistant à retrouver des informations sur des personnes à partir d’indications partielles sur leur situation. Ce genre d’énigmes, connues sous le nom de Zebra Puzzle en anglais, était très populaire comme jeux de logique dans différents magazines. C’est une bonne illustration de ce qu’on pourrait attendre d’une Intelligence Artificielle : quelles connaissances peut-on inférer d’un ensemble de faits connus ?
Dans cette section, on va s’intéresser à une version simplifiée de l’énigme d’Einstein et essayer d’inférer une méthode générale pour modéliser et résoudre ce genre de problème. L’énigme est la suivante (source, en anglais):
Dans une rue, il y a quatre maisons côte à côte (numérotées de 1 à 4). À partir des indices suivants, retrouvez pour chaque maison : sa couleur, le nom et le prénom de l’enfant qui y vit ainsi que le cadeau qu’il a reçu à Noël.
Voici une réponse partielle donnée par ChatGPT (à partir de la version anglaise), qui ne contient pas tous les noms prénoms mais les couleurs et les cadeaux (voir le transcript complet).
| Maison 1 | Maison 2 | Maison 3 | $Maison 4 |
|---|---|---|---|
| Young | Quinn | Patrick | _ |
| Ulysses | Skate | _ | Puzzle |
| Robot | Blanche | Rose | _ |
| King | Bleue | _ | Wyatt |
Cette proposition vous semble-t-elle correcte ? Pourquoi ?
Si vous avez un accès à ChatGPT, essayez par vous-même !
Cette réponse n’a pas beaucoup de sens. Par exemple :
Lorsque vous en aurez assez d’essayer de corriger ChatGPT, essayez de résoudre l’énigme par vous-même en remplissant le tableau suivant :
| Maison 1 | Maison 2 | Maison 3 | Maison 4 | |
|---|---|---|---|---|
| Nom | ||||
| Prénom | ||||
| Couleur | ||||
| Cadeau |
| Maison1 | Maison2 | Maison3 | Maison4 |
|---|---|---|---|
| Young | Quinn | Jackson | King |
| Ulysses | Wyatt | Patrick | Ian |
| Vert | Bleu | Blanc | Rose |
| Kit | Skate | Robot | Puzzle |
La solution que vous avez trouvée est-elle l’unique solution possible ? Pourquoi ?
Lorsqu’on construit la solution, on s’aperçoit normalement qu’à chaque étape, on peut remplir une nouvelle case sans ambiguité. Il ne peut donc pas y avoir d’autres solutions.
On veut aussi que si une maison est d’une certaine couleur, alors elle ne peut pas être d’une autre couleur : CRose1 ⇒ (¬CVert1∧¬CBleu1∧¬CVert1).
Il faut faire cela pour toutes les couleurs et toutes les maisons. Le mieux étant de le faire programmatiquement, voir solution.py pour une formalisation et logic.py en Python qui appelle un SAT solver à la fin pour résoudre le problème.
On peut l’écrire, ce qui donne en pratique l’horreur ci-dessous, ou
voir les codages utilisant les fonctions atleastone et
atmostone sur des ensembles de variables qu’on a généré
automatiquement. Dans le code, on a une simplification de
atmostone. En effet, si on a un ensemble P de variables propositionnelles et
qu’on veut accepter seulement les interprétations où au plus une
variable est mise à vrai, il suffit d’écrire la conjonction des clauses
¬x ∨ ¬y pour chaque
pair x, y ∈ P avec
x ≠ y. Si deux
variables a, b de
P sont mises à vraies, alors
¬a ∨ ¬b ne sera pas
satisfaite, donc la conjonction ne le sera pas non plus. Dans tous les
autres cas, la formule sera vraie.
(((CRose1∨CRose2∨CRose3∨CRose4)∧(CBlanc1∨CBlanc2∨CBlanc3∨CBlanc4)∧(CBleu1∨CBleu2∨CBleu3∨CBleu4)∧(CVert1∨CVert2∨CVert3∨CVert4))∧((¬(CRose1)∨¬(CRose2))∧(¬(CRose1)∨¬(CRose3))∧(¬(CRose1)∨¬(CRose4))∧(¬(CRose2)∨¬(CRose3))∧(¬(CRose2)∨¬(CRose4))∧(¬(CRose3)∨¬(CRose4))∧(¬(CBlanc1)∨¬(CBlanc2))∧(¬(CBlanc1)∨¬(CBlanc3))∧(¬(CBlanc1)∨¬(CBlanc4))∧(¬(CBlanc2)∨¬(CBlanc3))∧(¬(CBlanc2)∨¬(CBlanc4))∧(¬(CBlanc3)∨¬(CBlanc4))∧(¬(CBleu1)∨¬(CBleu2))∧(¬(CBleu1)∨¬(CBleu3))∧(¬(CBleu1)∨¬(CBleu4))∧(¬(CBleu2)∨¬(CBleu3))∧(¬(CBleu2)∨¬(CBleu4))∧(¬(CBleu3)∨¬(CBleu4))∧(¬(CVert1)∨¬(CVert2))∧(¬(CVert1)∨¬(CVert3))∧(¬(CVert1)∨¬(CVert4))∧(¬(CVert2)∨¬(CVert3))∧(¬(CVert2)∨¬(CVert4))∧(¬(CVert3)∨¬(CVert4))∧(¬(CRose1)∨¬(CBlanc1))∧(¬(CRose2)∨¬(CBlanc2))∧(¬(CRose3)∨¬(CBlanc3))∧(¬(CRose4)∨¬(CBlanc4))∧(¬(CRose1)∨¬(CBleu1))∧(¬(CRose2)∨¬(CBleu2))∧(¬(CRose3)∨¬(CBleu3))∧(¬(CRose4)∨¬(CBleu4))∧(¬(CRose1)∨¬(CVert1))∧(¬(CRose2)∨¬(CVert2))∧(¬(CRose3)∨¬(CVert3))∧(¬(CRose4)∨¬(CVert4))∧(¬(CBlanc1)∨¬(CRose1))∧(¬(CBlanc2)∨¬(CRose2))∧(¬(CBlanc3)∨¬(CRose3))∧(¬(CBlanc4)∨¬(CRose4))∧(¬(CBlanc1)∨¬(CBleu1))∧(¬(CBlanc2)∨¬(CBleu2))∧(¬(CBlanc3)∨¬(CBleu3))∧(¬(CBlanc4)∨¬(CBleu4))∧(¬(CBlanc1)∨¬(CVert1))∧(¬(CBlanc2)∨¬(CVert2))∧(¬(CBlanc3)∨¬(CVert3))∧(¬(CBlanc4)∨¬(CVert4))∧(¬(CBleu1)∨¬(CRose1))∧(¬(CBleu2)∨¬(CRose2))∧(¬(CBleu3)∨¬(CRose3))∧(¬(CBleu4)∨¬(CRose4))∧(¬(CBleu1)∨¬(CBlanc1))∧(¬(CBleu2)∨¬(CBlanc2))∧(¬(CBleu3)∨¬(CBlanc3))∧(¬(CBleu4)∨¬(CBlanc4))∧(¬(CBleu1)∨¬(CVert1))∧(¬(CBleu2)∨¬(CVert2))∧(¬(CBleu3)∨¬(CVert3))∧(¬(CBleu4)∨¬(CVert4))∧(¬(CVert1)∨¬(CRose1))∧(¬(CVert2)∨¬(CRose2))∧(¬(CVert3)∨¬(CRose3))∧(¬(CVert4)∨¬(CRose4))∧(¬(CVert1)∨¬(CBlanc1))∧(¬(CVert2)∨¬(CBlanc2))∧(¬(CVert3)∨¬(CBlanc3))∧(¬(CVert4)∨¬(CBlanc4))∧(¬(CVert1)∨¬(CBleu1))∧(¬(CVert2)∨¬(CBleu2))∧(¬(CVert3)∨¬(CBleu3))∧(¬(CVert4)∨¬(CBleu4))))
(((PIan1∨PIan2∨PIan3∨PIan4)∧(PPatrick1∨PPatrick2∨PPatrick3∨PPatrick4)∧(PUlysses1∨PUlysses2∨PUlysses3∨PUlysses4)∧(PWyatt1∨PWyatt2∨PWyatt3∨PWyatt4))∧((¬(PIan1)∨¬(PIan2))∧(¬(PIan1)∨¬(PIan3))∧(¬(PIan1)∨¬(PIan4))∧(¬(PIan2)∨¬(PIan3))∧(¬(PIan2)∨¬(PIan4))∧(¬(PIan3)∨¬(PIan4))∧(¬(PPatrick1)∨¬(PPatrick2))∧(¬(PPatrick1)∨¬(PPatrick3))∧(¬(PPatrick1)∨¬(PPatrick4))∧(¬(PPatrick2)∨¬(PPatrick3))∧(¬(PPatrick2)∨¬(PPatrick4))∧(¬(PPatrick3)∨¬(PPatrick4))∧(¬(PUlysses1)∨¬(PUlysses2))∧(¬(PUlysses1)∨¬(PUlysses3))∧(¬(PUlysses1)∨¬(PUlysses4))∧(¬(PUlysses2)∨¬(PUlysses3))∧(¬(PUlysses2)∨¬(PUlysses4))∧(¬(PUlysses3)∨¬(PUlysses4))∧(¬(PWyatt1)∨¬(PWyatt2))∧(¬(PWyatt1)∨¬(PWyatt3))∧(¬(PWyatt1)∨¬(PWyatt4))∧(¬(PWyatt2)∨¬(PWyatt3))∧(¬(PWyatt2)∨¬(PWyatt4))∧(¬(PWyatt3)∨¬(PWyatt4))∧(¬(PIan1)∨¬(PPatrick1))∧(¬(PIan2)∨¬(PPatrick2))∧(¬(PIan3)∨¬(PPatrick3))∧(¬(PIan4)∨¬(PPatrick4))∧(¬(PIan1)∨¬(PUlysses1))∧(¬(PIan2)∨¬(PUlysses2))∧(¬(PIan3)∨¬(PUlysses3))∧(¬(PIan4)∨¬(PUlysses4))∧(¬(PIan1)∨¬(PWyatt1))∧(¬(PIan2)∨¬(PWyatt2))∧(¬(PIan3)∨¬(PWyatt3))∧(¬(PIan4)∨¬(PWyatt4))∧(¬(PPatrick1)∨¬(PIan1))∧(¬(PPatrick2)∨¬(PIan2))∧(¬(PPatrick3)∨¬(PIan3))∧(¬(PPatrick4)∨¬(PIan4))∧(¬(PPatrick1)∨¬(PUlysses1))∧(¬(PPatrick2)∨¬(PUlysses2))∧(¬(PPatrick3)∨¬(PUlysses3))∧(¬(PPatrick4)∨¬(PUlysses4))∧(¬(PPatrick1)∨¬(PWyatt1))∧(¬(PPatrick2)∨¬(PWyatt2))∧(¬(PPatrick3)∨¬(PWyatt3))∧(¬(PPatrick4)∨¬(PWyatt4))∧(¬(PUlysses1)∨¬(PIan1))∧(¬(PUlysses2)∨¬(PIan2))∧(¬(PUlysses3)∨¬(PIan3))∧(¬(PUlysses4)∨¬(PIan4))∧(¬(PUlysses1)∨¬(PPatrick1))∧(¬(PUlysses2)∨¬(PPatrick2))∧(¬(PUlysses3)∨¬(PPatrick3))∧(¬(PUlysses4)∨¬(PPatrick4))∧(¬(PUlysses1)∨¬(PWyatt1))∧(¬(PUlysses2)∨¬(PWyatt2))∧(¬(PUlysses3)∨¬(PWyatt3))∧(¬(PUlysses4)∨¬(PWyatt4))∧(¬(PWyatt1)∨¬(PIan1))∧(¬(PWyatt2)∨¬(PIan2))∧(¬(PWyatt3)∨¬(PIan3))∧(¬(PWyatt4)∨¬(PIan4))∧(¬(PWyatt1)∨¬(PPatrick1))∧(¬(PWyatt2)∨¬(PPatrick2))∧(¬(PWyatt3)∨¬(PPatrick3))∧(¬(PWyatt4)∨¬(PPatrick4))∧(¬(PWyatt1)∨¬(PUlysses1))∧(¬(PWyatt2)∨¬(PUlysses2))∧(¬(PWyatt3)∨¬(PUlysses3))∧(¬(PWyatt4)∨¬(PUlysses4))))
(((NQuinn1∨NQuinn2∨NQuinn3∨NQuinn4)∧(NYoung1∨NYoung2∨NYoung3∨NYoung4)∧(NJackson1∨NJackson2∨NJackson3∨NJackson4)∧(NKing1∨NKing2∨NKing3∨NKing4))∧((¬(NQuinn1)∨¬(NQuinn2))∧(¬(NQuinn1)∨¬(NQuinn3))∧(¬(NQuinn1)∨¬(NQuinn4))∧(¬(NQuinn2)∨¬(NQuinn3))∧(¬(NQuinn2)∨¬(NQuinn4))∧(¬(NQuinn3)∨¬(NQuinn4))∧(¬(NYoung1)∨¬(NYoung2))∧(¬(NYoung1)∨¬(NYoung3))∧(¬(NYoung1)∨¬(NYoung4))∧(¬(NYoung2)∨¬(NYoung3))∧(¬(NYoung2)∨¬(NYoung4))∧(¬(NYoung3)∨¬(NYoung4))∧(¬(NJackson1)∨¬(NJackson2))∧(¬(NJackson1)∨¬(NJackson3))∧(¬(NJackson1)∨¬(NJackson4))∧(¬(NJackson2)∨¬(NJackson3))∧(¬(NJackson2)∨¬(NJackson4))∧(¬(NJackson3)∨¬(NJackson4))∧(¬(NKing1)∨¬(NKing2))∧(¬(NKing1)∨¬(NKing3))∧(¬(NKing1)∨¬(NKing4))∧(¬(NKing2)∨¬(NKing3))∧(¬(NKing2)∨¬(NKing4))∧(¬(NKing3)∨¬(NKing4))∧(¬(NQuinn1)∨¬(NYoung1))∧(¬(NQuinn2)∨¬(NYoung2))∧(¬(NQuinn3)∨¬(NYoung3))∧(¬(NQuinn4)∨¬(NYoung4))∧(¬(NQuinn1)∨¬(NJackson1))∧(¬(NQuinn2)∨¬(NJackson2))∧(¬(NQuinn3)∨¬(NJackson3))∧(¬(NQuinn4)∨¬(NJackson4))∧(¬(NQuinn1)∨¬(NKing1))∧(¬(NQuinn2)∨¬(NKing2))∧(¬(NQuinn3)∨¬(NKing3))∧(¬(NQuinn4)∨¬(NKing4))∧(¬(NYoung1)∨¬(NQuinn1))∧(¬(NYoung2)∨¬(NQuinn2))∧(¬(NYoung3)∨¬(NQuinn3))∧(¬(NYoung4)∨¬(NQuinn4))∧(¬(NYoung1)∨¬(NJackson1))∧(¬(NYoung2)∨¬(NJackson2))∧(¬(NYoung3)∨¬(NJackson3))∧(¬(NYoung4)∨¬(NJackson4))∧(¬(NYoung1)∨¬(NKing1))∧(¬(NYoung2)∨¬(NKing2))∧(¬(NYoung3)∨¬(NKing3))∧(¬(NYoung4)∨¬(NKing4))∧(¬(NJackson1)∨¬(NQuinn1))∧(¬(NJackson2)∨¬(NQuinn2))∧(¬(NJackson3)∨¬(NQuinn3))∧(¬(NJackson4)∨¬(NQuinn4))∧(¬(NJackson1)∨¬(NYoung1))∧(¬(NJackson2)∨¬(NYoung2))∧(¬(NJackson3)∨¬(NYoung3))∧(¬(NJackson4)∨¬(NYoung4))∧(¬(NJackson1)∨¬(NKing1))∧(¬(NJackson2)∨¬(NKing2))∧(¬(NJackson3)∨¬(NKing3))∧(¬(NJackson4)∨¬(NKing4))∧(¬(NKing1)∨¬(NQuinn1))∧(¬(NKing2)∨¬(NQuinn2))∧(¬(NKing3)∨¬(NQuinn3))∧(¬(NKing4)∨¬(NQuinn4))∧(¬(NKing1)∨¬(NYoung1))∧(¬(NKing2)∨¬(NYoung2))∧(¬(NKing3)∨¬(NYoung3))∧(¬(NKing4)∨¬(NYoung4))∧(¬(NKing1)∨¬(NJackson1))∧(¬(NKing2)∨¬(NJackson2))∧(¬(NKing3)∨¬(NJackson3))∧(¬(NKing4)∨¬(NJackson4))))
(((GSkateboard1∨GSkateboard2∨GSkateboard3∨GSkateboard4)∧(GPuzzle1∨GPuzzle2∨GPuzzle3∨GPuzzle4)∧(GRobot1∨GRobot2∨GRobot3∨GRobot4)∧(GKit1∨GKit2∨GKit3∨GKit4))∧((¬(GSkateboard1)∨¬(GSkateboard2))∧(¬(GSkateboard1)∨¬(GSkateboard3))∧(¬(GSkateboard1)∨¬(GSkateboard4))∧(¬(GSkateboard2)∨¬(GSkateboard3))∧(¬(GSkateboard2)∨¬(GSkateboard4))∧(¬(GSkateboard3)∨¬(GSkateboard4))∧(¬(GPuzzle1)∨¬(GPuzzle2))∧(¬(GPuzzle1)∨¬(GPuzzle3))∧(¬(GPuzzle1)∨¬(GPuzzle4))∧(¬(GPuzzle2)∨¬(GPuzzle3))∧(¬(GPuzzle2)∨¬(GPuzzle4))∧(¬(GPuzzle3)∨¬(GPuzzle4))∧(¬(GRobot1)∨¬(GRobot2))∧(¬(GRobot1)∨¬(GRobot3))∧(¬(GRobot1)∨¬(GRobot4))∧(¬(GRobot2)∨¬(GRobot3))∧(¬(GRobot2)∨¬(GRobot4))∧(¬(GRobot3)∨¬(GRobot4))∧(¬(GKit1)∨¬(GKit2))∧(¬(GKit1)∨¬(GKit3))∧(¬(GKit1)∨¬(GKit4))∧(¬(GKit2)∨¬(GKit3))∧(¬(GKit2)∨¬(GKit4))∧(¬(GKit3)∨¬(GKit4))∧(¬(GSkateboard1)∨¬(GPuzzle1))∧(¬(GSkateboard2)∨¬(GPuzzle2))∧(¬(GSkateboard3)∨¬(GPuzzle3))∧(¬(GSkateboard4)∨¬(GPuzzle4))∧(¬(GSkateboard1)∨¬(GRobot1))∧(¬(GSkateboard2)∨¬(GRobot2))∧(¬(GSkateboard3)∨¬(GRobot3))∧(¬(GSkateboard4)∨¬(GRobot4))∧(¬(GSkateboard1)∨¬(GKit1))∧(¬(GSkateboard2)∨¬(GKit2))∧(¬(GSkateboard3)∨¬(GKit3))∧(¬(GSkateboard4)∨¬(GKit4))∧(¬(GPuzzle1)∨¬(GSkateboard1))∧(¬(GPuzzle2)∨¬(GSkateboard2))∧(¬(GPuzzle3)∨¬(GSkateboard3))∧(¬(GPuzzle4)∨¬(GSkateboard4))∧(¬(GPuzzle1)∨¬(GRobot1))∧(¬(GPuzzle2)∨¬(GRobot2))∧(¬(GPuzzle3)∨¬(GRobot3))∧(¬(GPuzzle4)∨¬(GRobot4))∧(¬(GPuzzle1)∨¬(GKit1))∧(¬(GPuzzle2)∨¬(GKit2))∧(¬(GPuzzle3)∨¬(GKit3))∧(¬(GPuzzle4)∨¬(GKit4))∧(¬(GRobot1)∨¬(GSkateboard1))∧(¬(GRobot2)∨¬(GSkateboard2))∧(¬(GRobot3)∨¬(GSkateboard3))∧(¬(GRobot4)∨¬(GSkateboard4))∧(¬(GRobot1)∨¬(GPuzzle1))∧(¬(GRobot2)∨¬(GPuzzle2))∧(¬(GRobot3)∨¬(GPuzzle3))∧(¬(GRobot4)∨¬(GPuzzle4))∧(¬(GRobot1)∨¬(GKit1))∧(¬(GRobot2)∨¬(GKit2))∧(¬(GRobot3)∨¬(GKit3))∧(¬(GRobot4)∨¬(GKit4))∧(¬(GKit1)∨¬(GSkateboard1))∧(¬(GKit2)∨¬(GSkateboard2))∧(¬(GKit3)∨¬(GSkateboard3))∧(¬(GKit4)∨¬(GSkateboard4))∧(¬(GKit1)∨¬(GPuzzle1))∧(¬(GKit2)∨¬(GPuzzle2))∧(¬(GKit3)∨¬(GPuzzle3))∧(¬(GKit4)∨¬(GPuzzle4))∧(¬(GKit1)∨¬(GRobot1))∧(¬(GKit2)∨¬(GRobot2))∧(¬(GKit3)∨¬(GRobot3))∧(¬(GKit4)∨¬(GRobot4))))
GSkateboard2
NYoung1
(GPuzzle1∨GPuzzle4)
((CBlanc1∧GPuzzle2)∨(CBlanc2∧GPuzzle3)∨(CBlanc3∧GPuzzle4)∨(CBlanc4∧GPuzzle3)∨(CBlanc3∧GPuzzle2)∨(CBlanc2∧GPuzzle1))
((PUlysses1∧PWyatt2)∨(PUlysses2∧PWyatt3)∨(PUlysses3∧PWyatt4))
(NKing1∨NKing4)
((NYoung1⇒GKit1)∧(NYoung2⇒GKit2)∧(NYoung3⇒GKit3)∧(NYoung4⇒GKit4))
((CBlanc4∧CBleu3)∨(CBlanc3∧CBleu2)∨(CBlanc2∧CBleu1))
PPatrick3
((GRobot1∧CRose2)∨(GRobot2∧CRose3)∨(GRobot3∧CRose4)∨(GRobot4∧CRose3)∨(GRobot3∧CRose2)∨(GRobot2∧CRose1))
((NQuinn1⇒GSkateboard1)∧(NQuinn2⇒GSkateboard2)∧(NQuinn3⇒GSkateboard3)∧(NQuinn4⇒GSkateboard4))