# Imports : z3 (solveur SMT) + time (benchmark).
import time
import z3
print("z3 version :", z3.get_version_string())z3 version : 4.16.0Z3-Python-09 : L’enigme d’Einstein (Zebra puzzle)
← Serie Z3-Python | Z3-Python-08 (ordonnancement) →
Le problème
L’enigme d’Einstein (ou Zebra puzzle) est un classique de logique : 5 maisons alignees, chacune habitee par une personne de nationalite, couleur, boisson, cigarette et animal différents. On dispose de 15 indices (le Britannique vit dans la rouge, le Danois boit du the, la verte est a gauche de la blanche, etc.) et la question est : qui possede le poisson ?
A la main, la resolution procede par deductions progressives sur un tableau - c’est long et trompeur. L’espace de recherche brut est enorme : chaque attribut est une permutation des 5 maisons, soit \((5!)^5 = 24\,883\,200\,000\) combinaisons. Une enumeration exhaustive (brute force) testant les 15 indices pour chaque combinaison prend plusieurs minutes.
C’est typiquement la ou un solveur SMT comme Z3 fait la différence : on decrit les 25 variables (position de chaque valeur), le domaine, les 5 contraintes de permutation (Distinct) et les 15 indices, et Solver trouve l’unique solution en quelques millisecondes. Ce notebook porte en Python l’exemple C# 18_Einsteins_Riddle de la serie sœur Z3.Linq.
Modelisation : l’encodage par position
L’astuce centrale consiste a inverser le point de vue. Au lieu de demander « quelle couleur a la maison k ? », on définit pour chaque valeur d’attribut une variable entiere egale a la position (numéro de maison 0..4) ou elle se trouve :
Brit,Swede,Dane,Norwegian,German: position de chaque nationaliteRed,Green,White,Yellow,Blue: position de chaque couleurTea,Coffee,Milk,Water,Beer: position de chaque boissonPallMall,Dunhill,Blend,BlueMaster,Prince: position de chaque cigaretteDog,Bird,Cat,Horse,Fish: position de chaque animal
Soit 25 variables entieres. Les contraintes se traduisent alors très naturellement :
- Domaine : chaque variable \(\in \{0,1,2,3,4\}\).
- Permutation : dans chaque groupe d’attributs, les 5 positions sont deux a deux distinctes (
Distinct) - chaque valeur occupe une maison différente. - Les 15 indices : des egalites de position (
Brit == Red: le Britannique et la rouge sont dans la même maison) ou des adjacences (|Blend - Cat| == 1: le fumeur de Blend est voisin du Chat).
def build_einstein_solver():
"""Construit le solveur Z3 de l'enigme d'Einstein (25 vars de position, 15 indices).
Retourne (solver, var_dict, group_labels) pour reuse dans les exercices."""
s = z3.Solver()
# 25 variables de position (0..4) : une par valeur d'attribut.
groups = {
"Nationalite": ["Brit", "Swede", "Dane", "Norwegian", "German"],
"Couleur": ["Red", "Green", "White", "Yellow", "Blue"],
"Boisson": ["Tea", "Coffee", "Milk", "Water", "Beer"],
"Cigarette": ["PallMall", "Dunhill", "Blend", "BlueMaster", "Prince"],
"Animal": ["Dog", "Bird", "Cat", "Horse", "Fish"],
}
v = {n: z3.Int(n) for grp in groups.values() for n in grp}
# (1) Domaine 0..4 pour les 25 variables
for var in v.values():
s.add(var >= 0, var <= 4)
# (2) Permutation : les 5 valeurs d'un meme attribut occupent des maisons distinctes
for grp in groups.values():
s.add(z3.Distinct([v[n] for n in grp]))
# (3) Les 15 indices
s.add(v["Brit"] == v["Red"]) # 1. le Britannique vit dans la rouge
s.add(v["Swede"] == v["Dog"]) # 2. le Suedois eleve des chiens
s.add(v["Dane"] == v["Tea"]) # 3. le Danois boit du the
s.add(v["Green"] == v["White"] - 1) # 4. la verte est juste a gauche de la blanche
s.add(v["Green"] == v["Coffee"]) # 5. la verte boit du cafe
s.add(v["PallMall"] == v["Bird"]) # 6. Pall Mall eleve des oiseaux
s.add(v["Yellow"] == v["Dunhill"]) # 7. la jaune fume du Dunhill
s.add(v["Milk"] == 2) # 8. la maison du milieu boit du lait
s.add(v["Norwegian"] == 0) # 9. le Norvegien dans la 1ere maison
s.add(z3.Or(v["Blend"] - v["Cat"] == 1, v["Cat"] - v["Blend"] == 1)) # 10. Blend voisin du Chat
s.add(z3.Or(v["Horse"] - v["Dunhill"] == 1, v["Dunhill"] - v["Horse"] == 1)) # 11. Cheval voisin du Dunhill
s.add(v["BlueMaster"] == v["Beer"]) # 12. BlueMaster boit de la biere
s.add(v["German"] == v["Prince"]) # 13. l'Allemand fume du Prince
s.add(z3.Or(v["Norwegian"] - v["Blue"] == 1, v["Blue"] - v["Norwegian"] == 1)) # 14. Norvegien voisin de la bleue
s.add(z3.Or(v["Blend"] - v["Water"] == 1, v["Water"] - v["Blend"] == 1)) # 15. Blend voisin de l'Eau
return s, v, groups
print("Modele encode : 25 variables de position, 5 groupes Distinct, 15 indices.")Modele encode : 25 variables de position, 5 groupes Distinct, 15 indices.Resolution et temoin
On appelle s.check() : si sat, on extrait le modèle puis on inverse l’encodage par position - pour chaque maison \(h \in \{0..4\}\), on cherche quelle valeur de chaque attribut y se trouve (la valeur dont la position vaut \(h\)). Cela reconstitue le tableau classique de la solution.
# Labels francais pour l'affichage (associes au nom de variable).
LABELS_FR = {
"Nationalite": [("Britannique", "Brit"), ("Suedois", "Swede"), ("Danois", "Dane"), ("Norvegien", "Norwegian"), ("Allemand", "German")],
"Couleur": [("Rouge", "Red"), ("Verte", "Green"), ("Blanche", "White"), ("Jaune", "Yellow"), ("Bleue", "Blue")],
"Boisson": [("The", "Tea"), ("Cafe", "Coffee"), ("Lait", "Milk"), ("Eau", "Water"), ("Biere", "Beer")],
"Cigarette": [("Pall Mall", "PallMall"), ("Dunhill", "Dunhill"), ("Blend", "Blend"), ("BlueMaster", "BlueMaster"), ("Prince", "Prince")],
"Animal": [("Chien", "Dog"), ("Oiseau", "Bird"), ("Chat", "Cat"), ("Cheval", "Horse"), ("Poisson", "Fish")],
}
def solve_and_display():
"""Resout l'enigme et affiche le tableau des 5 maisons."""
s, v, _ = build_einstein_solver()
assert s.check() == z3.sat, "UNSAT (inattendu pour cette enigme)"
m = s.model()
pos = {n: m[v[n]].as_long() for n in v} # nom de variable -> position (0..4)
def val_at(group, h):
"""Retourne le label francais de la valeur du groupe present a la maison h."""
for fr, key in LABELS_FR[group]:
if pos[key] == h:
return fr
return "?"
cols = ["Maison", "Nationalite", "Couleur", "Boisson", "Cigarette", "Animal"]
widths = [7, 13, 9, 9, 13, 9]
print(" ".join(c.ljust(w) for c, w in zip(cols, widths)))
print(" " + "-" * (sum(widths) + 2 * (len(cols) - 1)))
for h in range(5):
row = [str(h + 1)] + [val_at(g, h) for g in ["Nationalite", "Couleur", "Boisson", "Cigarette", "Animal"]]
print(" ".join(c.ljust(w) for c, w in zip(row, widths)))
print()
print(f">>> Reponse : c'est le {val_at('Nationalite', pos['Fish'])} qui possede le Poisson (maison {pos['Fish'] + 1}).")
return m, v
solution_model, solution_vars = solve_and_display()Maison Nationalite Couleur Boisson Cigarette Animal
----------------------------------------------------------------------
1 Norvegien Jaune Eau Dunhill Chat
2 Danois Bleue The Blend Cheval
3 Britannique Rouge Lait Pall Mall Oiseau
4 Allemand Verte Cafe Prince Poisson
5 Suedois Blanche Biere BlueMaster Chien
>>> Reponse : c'est le Allemand qui possede le Poisson (maison 4).Interpretation
Z3 trouve l’unique solution en quelques millisecondes. La resolution humaine procederait par deductions progressives - on place le Norvegien en 1 (Norwegian == 0), le lait en 3 (Milk == 2), puis on propage les egalites et adjacences - mais c’est précisément ce travail de propagation de contraintes que le solveur automatise, sans erreur ni oubli.
La reponse a la question « qui possede le poisson ? » tombe directement du modèle extrait. Notons qu’aucun indice ne parle du poisson : c’est par elimination (les 4 autres animaux sont localises par les indices) que sa position se deduit.
Vérification du témoin : relire les indices
Un modèle extrait n’est pas un résultat à prendre sur parole — vérifions que le tableau ci-dessus satisfait bien quelques indices choisis dans l’énoncé original :
- Le Norvégien vit à côté de la maison bleue : Norvégien en maison 1, Bleue en maison 2 — voisins.
- Le fumeur de Blend a un voisin qui garde le chat : Blend en maison 2, Chat en maison 1 — voisins.
- La maison verte est immédiatement à gauche de la blanche : Verte en 4, Blanche en 5.
- La maison du centre boit du lait : Lait en maison 3.
Ce geste de re-lecture croisée est l’équivalent d’un test unitaire sur le solveur : il valide l’encodage (une contrainte mal traduite produirait un témoin qui échoue à la vérification), pas seulement la satisfiabilité.
Approche naive vs solveur : mesurer l’ecart
Plutot que d’affirmer que le solveur est plus rapide, mesurons l’ecart. L’espace de recherche brut est \((5!)^5\) : chaque attribut est une permutation des 5 maisons, independamment. On chronometre aussi la resolution Z3, puis on prouve l’unicite de la solution en ajoutant la negation du temoin trouve et en re-resolvant (on attend unsat).
# (1) Espace de recherche brut
import math
space = math.factorial(5) ** 5 # (5!)^5 = 24_883_200_000
brute_seconds = space / 1e8 # a ~1e8 tests/s, sans compter le test des 15 indices
# (2) Chronometre la resolution Z3
t0 = time.perf_counter()
s1, v1, _ = build_einstein_solver()
assert s1.check() == z3.sat
m1 = s1.model()
z3_ms = (time.perf_counter() - t0) * 1000
# (3) Unicite : on nie le temoin trouve (au moins une variable differe) -> on attend unsat
s2, v2, _ = build_einstein_solver()
negation = z3.Or([v2[n] != m1[v1[n]].as_long() for n in v2]) # une solution differente existe-t-elle ?
s2.add(negation)
unique = (s2.check() == z3.unsat)
print(f"Espace de recherche brut : (5!)^5 = {space:,} combinaisons")
print(f"Brute force estime (~1e8/s) : {brute_seconds:.1f} s (hors test des 15 indices)")
print(f"Z3 solve temps : {z3_ms:.1f} ms")
print(f"Solution unique (UNSAT si nie) : {unique}")
print(f" -> Z3 resout en millisecondes un espace de ~{space/1e9:.0f} milliards, et prouve l'unicite sans enumeration.")Espace de recherche brut : (5!)^5 = 24,883,200,000 combinaisons
Brute force estime (~1e8/s) : 248.8 s (hors test des 15 indices)
Z3 solve temps : 13.8 ms
Solution unique (UNSAT si nie) : True
-> Z3 resout en millisecondes un espace de ~25 milliards, et prouve l'unicite sans enumeration.Lecture du benchmark
Sur cette enigme, l’ecart est frappant : Z3 resout les 25 variables entrelacees en quelques millisecondes, alors que la brute force doit affronter ~25 milliards de combinaisons (soit plusieurs minutes même a cadence elevee, et bien plus avec le test des 15 indices a chaque candidat).
La propagation fait tout le travail : Norwegian == 0 et Milk == 2 sont des ancres imposees par les indices 9 et 8, puis les egalites de position et les adjacences reduisent les domaines restants jusqu’a ce qu’il ne reste qu’une seule combinaison coherente. C’est exactement la mecanique qu’un humain deployerait a la main sur le tableau - mais le solveur la realise sans erreur et la prouve complete (unicite via unsat sur la negation).
Exercices
Les trois exercices suivants vous font reutiliser l’encodage par position et la fonction build_einstein_solver. Chaque stub est self-contained : redefinissez le solveur, ajustez les contraintes, puis check().
Exercice 1 – Un 16e indice : le Chat boit de l’Eau
Objectif : ajouter l’indice Cat == Water (le Chat et l’Eau sont dans la même maison) et observer si l’enigme reste satisfaisable (sat) ou devient contradictoire (unsat).
Indices : reprenez build_einstein_solver(), ajoutez s.add(v["Cat"] == v["Water"]) avant check(). Que se passe-t-il ? (Pensez a comparer avec la solution trouvee plus haut : le Chat et l’Eau y sont-ils dans la même maison ?)
# Exercice 1 : ajoutez l'indice Cat == Water et testez la satisfiabilite.
# Etape 1 : reprenez build_einstein_solver() -> s, v, _.
# Etape 2 : s.add(v["Cat"] == v["Water"]).
# Etape 3 : s.check() -> sat ou unsat ?
def tester_chat_eau():
"""Retourne 'sat' ou 'unsat' apres ajout de l'indice Cat == Water."""
# TODO etudiant : construire le solveur, ajouter l'indice, retourner le verdict
return None
print("Exercice 1 a completer : ajoutez Cat == Water et testez la satisfiabilite.")Exercice 1 a completer : ajoutez Cat == Water et testez la satisfiabilite.Exercice 2 – Enumerer toutes les solutions
Objectif : enumerer toutes les solutions de l’enigme par blocage iteratif (on resout, on compte, on ajoute une contrainte interdisant le temoin trouve, on re-resout) jusqu’a unsat. Le compte attendu est 1 (solution unique), ce qui confirme le benchmark ci-dessus.
Indices : boucle while s.check() == z3.sat ; a chaque tour, comptez++, puis s.add(z3.Or([v[n] != m[v[n]].as_long() for n in v])) pour interdire le temoin courant et forcer une solution différente au tour suivant.
# Exercice 2 : enumerer toutes les solutions par blocage iteratif.
# Etape 1 : s, v, _ = build_einstein_solver().
# Etape 2 : while s.check() == z3.sat: compte += 1; m = s.model(); s.add(z3.Or([v[n] != m[v[n]].as_long() for n in v])).
# Etape 3 : afficher le compte (attendu : 1).
def compter_solutions():
"""Retourne le nombre total de solutions de l'enigme (attendu : 1)."""
# TODO etudiant : boucle de blocage iteratif
return None
print("Exercice 2 a completer : enumerer toutes les solutions par blocage iteratif.")Exercice 2 a completer : enumerer toutes les solutions par blocage iteratif.Exercice 3 – Mini-Zebra a 4 maisons / 4 attributs
Objectif : modeliser une mini-enigme a 4 maisons et 4 attributs (4 nationalites, 4 couleurs, 4 animaux) avec 8 indices de votre choix, et verifyez que build_einstein_solver se generalise (le modèle est paramètre par les données).
Indices : definissez groups_4 avec 4 valeurs par attribut, domaine 0..3, 3 groupes Distinct, puis 8 indices (identites de position + adjacences) inventes. Inspirez-vous de la structure de build_einstein_solver.
# Exercice 3 : modelisez un mini-Zebra a 4 maisons / 4 attributs.
# Indice : groups_4 = {"Nat": [...4...], "Couleur": [...4...], "Animal": [...4...]}, domaine 0..3.
# Etape 1 : definissez groups_4 (4 valeurs par attribut) et un solveur avec domaine 0..3 + 3 Distinct.
# Etape 2 : ajoutez 8 indices (identites + adjacences) de votre choix.
# Etape 3 : check() -> solution unique ?
def resoudre_mini_zebra():
"""Retourne (solver, var_dict) pour une mini-enigme 4 maisons / 4 attributs."""
# TODO etudiant : definir groups_4 + solveur + 8 indices
return None
print("Exercice 3 a completer : modelisez un mini-Zebra a 4 maisons / 4 attributs.")Exercice 3 a completer : modelisez un mini-Zebra a 4 maisons / 4 attributs.Conclusion
L’enigme d’Einstein illustre le gain du declaratif sur une classe de problemes ou l’approche humaine (deduction progressive sur un tableau) et l’approche naive (brute force) sont toutes deux laborieuses :
- L’encodage par position (une variable entiere = position de chaque valeur) transforme un puzzle apparemment qualitatif en un système de contraintes arithmetiques : egalites (
Brit == Red), adjacences (|Blend - Cat| == 1), permutations (Distinct). - La propagation de contraintes resout les 25 variables entrelacees en millisecondes la ou la brute force affronte ~25 milliards de combinaisons ; le solveur prouve l’unicite en niant le temoin et en observant
unsat. - Le modèle est paramètre par les données : ajouter un indice, un attribut ou une maison se fait en modifiant l’instance, sans re-ecrire l’algorithme de resolution.
Contraste avec le job-shop (notebook 08) : ici Solver suffit (on cherche une solution realisable, pas un optimum) - c’est la satisfiabilite pure, la ou l’ordonnancement relevait de l’optimisation (Optimize.minimize du makespan). Les deux postures du solveur, posees au notebook 01, trouvent ici leur illustration complementaire.
Suite logique : retour a la serie Z3-Python, ou explorez la version C# Z3.Linq qui aborde la même enigme via la couche declarative LINQ.