<- 17 - Unsat Cores | README Z3
Navigation : Index Z3 | Index SymbolicAI | Index general
Duree estimee : 40-50 minutes
L’enigme d’Einstein (ou Zebra puzzle) est un problème de logique attribue - probablement a tort - a Albert Einstein. Cinq maisons alignees, cinq nationalites, cinq couleurs, cinq boissons, cinq cigarettes, cinq animaux. A partir de quinze indices, determiner la disposition complete et, surtout : a qui appartient le poisson ?
L’espace de recherche est colossal : 5 attributs x 5! permutations chacun = (120)^5 de l’ordre de 2,5 milliards de combinaisons. La resolution humaine procede par deduction pas-a-pas (remplir un tableau en propageant les indices). C’est le terrain ideal pour montrer comment un solveur SMT propage globalement des contraintes entrelacees plutot que d’enumerer.
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
Console.WriteLine("Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.Linq");Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.LinqL’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 animalSoit 25 variables entieres, chacune dans {0, 1, 2, 3, 4}. Trois familles de contraintes :
{0..4} (une position valide).Z3Methods.Distinct) - chaque nationalite est dans une maison différente.Brit == Red), des decalages (“la verte est juste a gauche de la blanche” se code Green == White - 1), et des adjacences (“voisin de” se code |X - Y| == 1, c’est-a-dire la disjonction (X - Y == 1) || (Y - X == 1)).Cet encodage transforme un puzzle de logique en un CSP sur les entiers : tous les indices deviennent des contraintes lineaires ou des disjonctions que le solveur propage.
// L'enigme d'Einstein : 5 maisons, 5 attributs, 15 indices.
// Encodage par position : chaque champ = numero de maison (0..4) ou la valeur apparait.
public class Einstein
{
// Nationalites
public int Brit = 0, Swede = 0, Dane = 0, Norwegian = 0, German = 0;
// Couleurs
public int Red = 0, Green = 0, White = 0, Yellow = 0, Blue = 0;
// Boissons
public int Tea = 0, Coffee = 0, Milk = 0, Water = 0, Beer = 0;
// Cigarettes
public int PallMall = 0, Dunhill = 0, Blend = 0, BlueMaster = 0, Prince = 0;
// Animaux
public int Dog = 0, Bird = 0, Cat = 0, Horse = 0, Fish = 0;
}
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<Einstein>();
// (1) Domaine 0..4 pour les 25 variables
th = th.Where(t =>
t.Brit>=0&&t.Brit<=4 && t.Swede>=0&&t.Swede<=4 && t.Dane>=0&&t.Dane<=4 && t.Norwegian>=0&&t.Norwegian<=4 && t.German>=0&&t.German<=4 &&
t.Red>=0&&t.Red<=4 && t.Green>=0&&t.Green<=4 && t.White>=0&&t.White<=4 && t.Yellow>=0&&t.Yellow<=4 && t.Blue>=0&&t.Blue<=4 &&
t.Tea>=0&&t.Tea<=4 && t.Coffee>=0&&t.Coffee<=4 && t.Milk>=0&&t.Milk<=4 && t.Water>=0&&t.Water<=4 && t.Beer>=0&&t.Beer<=4 &&
t.PallMall>=0&&t.PallMall<=4 && t.Dunhill>=0&&t.Dunhill<=4 && t.Blend>=0&&t.Blend<=4 && t.BlueMaster>=0&&t.BlueMaster<=4 && t.Prince>=0&&t.Prince<=4 &&
t.Dog>=0&&t.Dog<=4 && t.Bird>=0&&t.Bird<=4 && t.Cat>=0&&t.Cat<=4 && t.Horse>=0&&t.Horse<=4 && t.Fish>=0&&t.Fish<=4);
// (2) Permutation : 5 groupes Distinct (chaque attribut occupe les 5 maisons)
th = th.Where(t => Z3Methods.Distinct(t.Brit, t.Swede, t.Dane, t.Norwegian, t.German));
th = th.Where(t => Z3Methods.Distinct(t.Red, t.Green, t.White, t.Yellow, t.Blue));
th = th.Where(t => Z3Methods.Distinct(t.Tea, t.Coffee, t.Milk, t.Water, t.Beer));
th = th.Where(t => Z3Methods.Distinct(t.PallMall, t.Dunhill, t.Blend, t.BlueMaster, t.Prince));
th = th.Where(t => Z3Methods.Distinct(t.Dog, t.Bird, t.Cat, t.Horse, t.Fish));
// (3) Les 15 indices
th = th.Where(t => t.Brit == t.Red); // 1. Le Britannique vit dans la maison rouge
th = th.Where(t => t.Swede == t.Dog); // 2. le Suedois eleve des chiens
th = th.Where(t => t.Dane == t.Tea); // 3. le Danois boit du the
th = th.Where(t => t.Green == t.White - 1); // 4. la verte est juste a gauche de la blanche
th = th.Where(t => t.Green == t.Coffee); // 5. le proprietaire de la verte boit du cafe
th = th.Where(t => t.PallMall == t.Bird); // 6. fumeur de Pall Mall eleve des oiseaux
th = th.Where(t => t.Yellow == t.Dunhill); // 7. la jaune fume du Dunhill
th = th.Where(t => t.Milk == 2); // 8. la maison du milieu boit du lait
th = th.Where(t => t.Norwegian == 0); // 9. le Norvegien vit dans la 1ere maison
th = th.Where(t => (t.Blend - t.Cat == 1) || (t.Cat - t.Blend == 1)); // 10. Blend voisin du Chat
th = th.Where(t => (t.Horse - t.Dunhill == 1) || (t.Dunhill - t.Horse == 1)); // 11. Cheval voisin du Dunhill
th = th.Where(t => t.BlueMaster == t.Beer); // 12. fumeur de BlueMaster boit de la biere
th = th.Where(t => t.German == t.Prince); // 13. l'Allemand fume du Prince
th = th.Where(t => (t.Norwegian - t.Blue == 1) || (t.Blue - t.Norwegian == 1)); // 14. Norvegien voisin de la bleue
th = th.Where(t => (t.Blend - t.Water == 1) || (t.Water - t.Blend == 1)); // 15. Blend voisin de l'Eau
var sol = th.Solve();
if (sol == null) {
Console.WriteLine("UNSAT : aucune solution (inattendu pour cette enigme)");
} else {
// Inversion : pour chaque maison h, quelle valeur de chaque attribut y est ?
var nat = new[]{("Britannique",sol.Brit),("Suedois",sol.Swede),("Danois",sol.Dane),("Norvegien",sol.Norwegian),("Allemand",sol.German)};
var col = new[]{("Rouge",sol.Red),("Verte",sol.Green),("Blanche",sol.White),("Jaune",sol.Yellow),("Bleue",sol.Blue)};
var drk = new[]{("The",sol.Tea),("Cafe",sol.Coffee),("Lait",sol.Milk),("Eau",sol.Water),("Biere",sol.Beer)};
var smk = new[]{("Pall Mall",sol.PallMall),("Dunhill",sol.Dunhill),("Blend",sol.Blend),("BlueMaster",sol.BlueMaster),("Prince",sol.Prince)};
var pet = new[]{("Chien",sol.Dog),("Oiseau",sol.Bird),("Chat",sol.Cat),("Cheval",sol.Horse),("Poisson",sol.Fish)};
string Val((string,int)[] arr, int h) => arr.First(p => p.Item2 == h).Item1;
Console.WriteLine($"{"Maison",-10}{"Nationalite",-14}{"Couleur",-10}{"Boisson",-10}{"Cigarette",-14}{"Animal",-10}");
Console.WriteLine(new string('-', 68));
for (int h = 0; h < 5; h++) {
Console.WriteLine($"{h+1,-10}{Val(nat,h),-14}{Val(col,h),-10}{Val(drk,h),-10}{Val(smk,h),-14}{Val(pet,h),-10}");
}
Console.WriteLine();
Console.WriteLine($">>> Reponse : le {Val(nat, sol.Fish)} possede le Poisson (maison {sol.Fish+1}).");
}
}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 : le Allemand possede le Poisson (maison 4).Z3 trouve la solution unique en quelques millisecondes :
Reponse : c’est l’Allemand qui possede le poisson.
Pourquoi le solveur fait la différence (Prong-B) : la resolution humaine procede par deduction progressive - on place le Norvegien en 1 (Norwegian == 0), le lait en 3 (Milk == 2), on deduit la bleue en 2 (voisin du Norvegien), puis on enchaine les croisements. C’est fastidieux et erreur-prone. Le solveur, lui, propage simultanement les 15 indices : Norwegian == 0 et Milk == 2 fixent deux ancres, puis les egalites de position (Brit == Red, German == Prince…) et les adjacences reduisent les domaines en cascade jusqu’a la solution unique. Aucune enumeration des 2,5 milliards de combinaisons.
C’est aussi un exemple ou l’encodage est decisif : traduire “voisin de” en |X - Y| == 1 (une disjonction lineaire) rend l’adjacence directement exploitable par le solveur, la ou une enumeration devrait tester chaque paire de positions.
Pour mesurer l’ecart (plutot que l’affirmer), comparons la taille de l’espace de recherche a ce que fait Z3 :
(5!)^5 = 120^5 = 24 883 200 000 combinaisons, puis tester les 15 indices pour chacune. Cet espace de ~25 milliards de candidats est inatteignable par enumeration exhaustive - et le test des 15 indices rend chaque candidat nettement plus lent. C’est precisement cet ecart de complexite que Z3 evite : il propage les contraintes au lieu d’enumerer.Distinct + 15 indices, et laisser le solveur propager. La propagation fixe Norwegian = 0 et Milk = 2 sans aucun essai, puis reduit les domaines jusqu’a la solution unique.Mesurons également si la solution est unique : ajoutons une contrainte niant la solution trouvee (au moins un attribut différent) et re-solvons. Si Z3 repond UNSAT, la solution est prouvee unique.
using System.Diagnostics;
// (1) Z3 resout l'enigme complete - mesure du temps
var sw = Stopwatch.StartNew();
Einstein sol = null;
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<Einstein>()
.Where(t => t.Brit>=0&&t.Brit<=4&&t.Swede>=0&&t.Swede<=4&&t.Dane>=0&&t.Dane<=4&&t.Norwegian>=0&&t.Norwegian<=4&&t.German>=0&&t.German<=4
&& t.Red>=0&&t.Red<=4&&t.Green>=0&&t.Green<=4&&t.White>=0&&t.White<=4&&t.Yellow>=0&&t.Yellow<=4&&t.Blue>=0&&t.Blue<=4
&& t.Tea>=0&&t.Tea<=4&&t.Coffee>=0&&t.Coffee<=4&&t.Milk>=0&&t.Milk<=4&&t.Water>=0&&t.Water<=4&&t.Beer>=0&&t.Beer<=4
&& t.PallMall>=0&&t.PallMall<=4&&t.Dunhill>=0&&t.Dunhill<=4&&t.Blend>=0&&t.Blend<=4&&t.BlueMaster>=0&&t.BlueMaster<=4&&t.Prince>=0&&t.Prince<=4
&& t.Dog>=0&&t.Dog<=4&&t.Bird>=0&&t.Bird<=4&&t.Cat>=0&&t.Cat<=4&&t.Horse>=0&&t.Horse<=4&&t.Fish>=0&&t.Fish<=4)
.Where(t => Z3Methods.Distinct(t.Brit,t.Swede,t.Dane,t.Norwegian,t.German))
.Where(t => Z3Methods.Distinct(t.Red,t.Green,t.White,t.Yellow,t.Blue))
.Where(t => Z3Methods.Distinct(t.Tea,t.Coffee,t.Milk,t.Water,t.Beer))
.Where(t => Z3Methods.Distinct(t.PallMall,t.Dunhill,t.Blend,t.BlueMaster,t.Prince))
.Where(t => Z3Methods.Distinct(t.Dog,t.Bird,t.Cat,t.Horse,t.Fish))
.Where(t => t.Brit==t.Red && t.Swede==t.Dog && t.Dane==t.Tea)
.Where(t => t.Green==t.White-1 && t.Green==t.Coffee)
.Where(t => t.PallMall==t.Bird && t.Yellow==t.Dunhill)
.Where(t => t.Milk==2 && t.Norwegian==0)
.Where(t => (t.Blend-t.Cat==1)||(t.Cat-t.Blend==1))
.Where(t => (t.Horse-t.Dunhill==1)||(t.Dunhill-t.Horse==1))
.Where(t => t.BlueMaster==t.Beer && t.German==t.Prince)
.Where(t => (t.Norwegian-t.Blue==1)||(t.Blue-t.Norwegian==1))
.Where(t => (t.Blend-t.Water==1)||(t.Water-t.Blend==1));
sol = th.Solve();
}
sw.Stop();
// (2) Unicite : nie la solution trouvee, re-solve -> attend UNSAT
bool unique = false;
if (sol != null) {
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<Einstein>()
.Where(t => t.Brit>=0&&t.Brit<=4&&t.Swede>=0&&t.Swede<=4&&t.Dane>=0&&t.Dane<=4&&t.Norwegian>=0&&t.Norwegian<=4&&t.German>=0&&t.German<=4
&& t.Red>=0&&t.Red<=4&&t.Green>=0&&t.Green<=4&&t.White>=0&&t.White<=4&&t.Yellow>=0&&t.Yellow<=4&&t.Blue>=0&&t.Blue<=4
&& t.Tea>=0&&t.Tea<=4&&t.Coffee>=0&&t.Coffee<=4&&t.Milk>=0&&t.Milk<=4&&t.Water>=0&&t.Water<=4&&t.Beer>=0&&t.Beer<=4
&& t.PallMall>=0&&t.PallMall<=4&&t.Dunhill>=0&&t.Dunhill<=4&&t.Blend>=0&&t.Blend<=4&&t.BlueMaster>=0&&t.BlueMaster<=4&&t.Prince>=0&&t.Prince<=4
&& t.Dog>=0&&t.Dog<=4&&t.Bird>=0&&t.Bird<=4&&t.Cat>=0&&t.Cat<=4&&t.Horse>=0&&t.Horse<=4&&t.Fish>=0&&t.Fish<=4)
.Where(t => Z3Methods.Distinct(t.Brit,t.Swede,t.Dane,t.Norwegian,t.German))
.Where(t => Z3Methods.Distinct(t.Red,t.Green,t.White,t.Yellow,t.Blue))
.Where(t => Z3Methods.Distinct(t.Tea,t.Coffee,t.Milk,t.Water,t.Beer))
.Where(t => Z3Methods.Distinct(t.PallMall,t.Dunhill,t.Blend,t.BlueMaster,t.Prince))
.Where(t => Z3Methods.Distinct(t.Dog,t.Bird,t.Cat,t.Horse,t.Fish))
.Where(t => t.Brit==t.Red && t.Swede==t.Dog && t.Dane==t.Tea)
.Where(t => t.Green==t.White-1 && t.Green==t.Coffee)
.Where(t => t.PallMall==t.Bird && t.Yellow==t.Dunhill)
.Where(t => t.Milk==2 && t.Norwegian==0)
.Where(t => (t.Blend-t.Cat==1)||(t.Cat-t.Blend==1))
.Where(t => (t.Horse-t.Dunhill==1)||(t.Dunhill-t.Horse==1))
.Where(t => t.BlueMaster==t.Beer && t.German==t.Prince)
.Where(t => (t.Norwegian-t.Blue==1)||(t.Blue-t.Norwegian==1))
.Where(t => (t.Blend-t.Water==1)||(t.Water-t.Blend==1))
// nie la solution trouvee en litteraux ( Britannique=2, ..., Poisson=3 ) :
// l'encodage DSL ne reduit pas les valeurs capturees a l'execution -> litteraux.
.Where(t => t.Brit!=2||t.Swede!=4||t.Dane!=1||t.Norwegian!=0||t.German!=3||
t.Red!=2||t.Green!=3||t.White!=4||t.Yellow!=0||t.Blue!=1||
t.Tea!=1||t.Coffee!=3||t.Milk!=2||t.Water!=0||t.Beer!=4||
t.PallMall!=2||t.Dunhill!=0||t.Blend!=1||t.BlueMaster!=4||t.Prince!=3||
t.Dog!=4||t.Bird!=2||t.Cat!=0||t.Horse!=1||t.Fish!=3);
unique = (th.Solve() == null); // UNSAT => unique
}
}
long space = 120L * 120 * 120 * 120 * 120; // (5!)^5
Console.WriteLine($"Espace de recherche brut : (5!)^5 = {space:N0} combinaisons");
Console.WriteLine($"Brute force estime (~1e8/s) : {space/100_000_000.0:F1} s (sans compter le test des 15 indices)");
Console.WriteLine($"Z3 solve temps : {sw.Elapsed.TotalMilliseconds:F1} ms");
Console.WriteLine($"Solution trouvee : {(sol != null ? "OUI" : "NON")}");
Console.WriteLine($"Solution unique (UNSAT si nie) : {unique}");
Console.WriteLine($" -> Z3 resout en millisecondes un espace de 2,5 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 (sans compter le test des 15 indices)
Z3 solve temps : 122,2 ms
Solution trouvee : OUI
Solution unique (UNSAT si nie) : True
-> Z3 resout en millisecondes un espace de 2,5 milliards, et prouve l'unicite sans enumeration.Sur cette enigme, l’ecart est frappant et non plus de “même ordre de grandeur” comme sur le cryptarithme a 8 lettres :
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 en cascade. Aucune enumeration.C’est l’illustration la plus nette du Prong-B : un problème ou le moteur SMT exerce pleinement sa capacite distinctive - reduire un espace combinatoire gigantesque par propagation de contraintes globales, plutot que l’enumerer. La regression (un simple if ou une table de hachage) ne peut pas resoudre ce problème ; le solveur SMT, si.
Les trois exercices ci-dessous vous font reutiliser l’encodage par position. Chaque exercice suit le même squelette : redefinir le theoreme, ajuster les contraintes, puis Solve(). Rappel C.1 : les stubs ne levent jamais d’erreur - ils utilisent Console.WriteLine("Exercice a completer"). Le notebook s’execute de bout en bout même exercices non resolus.
Ajoutez l’indice supplementaire “le proprietaire du chat boit de l’eau” (soit Cat == Water) en plus des 15 indices existants. Le puzzle reste-t-il satisfiable ? Si non, que prouve Z3 ?
Étapes : 1. Reprenez le theoreme de la cellule 3 avec les 15 indices. 2. Ajoutez une 16e contrainte .Where(t => t.Cat == t.Water). 3. Appelez Solve() et observez le résultat (solution ou null).
// Exercice 1 : ajouter l'indice "le Chat boit de l'Eau" (Cat == Water)
// TODO etudiant :
// Etape 1 : reprendre le theoreme Einstein (domaine + 5 Distinct + 15 indices)
// Etape 2 : ajouter .Where(t => t.Cat == t.Water)
// Etape 3 : Solve() -> la solution reste-t-elle SAT, ou devient-elle UNSAT ?
Console.WriteLine("Exercice 1 a completer : ajoutez l'indice Cat == Water et testez la satisfiabilite");Exercice 1 a completer : ajoutez l'indice Cat == Water et testez la satisfiabiliteLa cellule 6 demontre l’unicite en niant la solution sur 5 attributs. Generalisez : ecrivez une boucle qui, après avoir trouve la solution, enumere toutes les solutions (méthode du blocage iteratif - bloquer la solution trouvee, re-solve, jusqu’a UNSAT) et affiche combien il y en a. Indice : a chaque itération, ajoutez une contrainte “au moins un attribut != solution courante” et re-solvez. Comptez les itérations. Vous devez trouver 1 (solution unique).
// Exercice 2 : enumerer toutes les solutions de l'enigme (boucle de blocage iteratif)
// TODO etudiant :
// 1. Solve() -> si sol != null, compter++, ajouter contrainte (au moins un attribut != sol)
// 2. Recommencer jusqu'a UNSAT (sol == null)
// 3. Afficher le nombre total de solutions (attendu : 1)
Console.WriteLine("Exercice 2 a completer : enumerer toutes les solutions par blocage iteratif");Exercice 2 a completer : enumerer toutes les solutions par blocage iteratifConstruisez un mini-Zebra a 4 maisons, 4 nationalites, 4 couleurs et 4 animaux, avec 8 indices de votre choix (identites + adjacences). Definissez une nouvelle classe (par ex. MiniZebra) avec 16 variables entieres dans {0..3}, et resolvez-le. Question subsidiaire : votre jeu d’indices donne-t-il une solution unique ? Si non, combien de solutions Z3 trouve-t-il ?
// Exercice 3 : mini-Zebra a 4 maisons / 4 attributs
// TODO etudiant :
// 1. Classe MiniZebra { 4 nationalites, 4 couleurs, 4 animaux } (int, domaine 0..3)
// 2. 4 groupes Distinct (4 attributs)
// 3. 8 indices (identites + adjacences) de votre choix
// 4. Solve() -> solution unique ?
Console.WriteLine("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 attributsL’enigme d’Einstein est le terrain le plus complet pour apprehender la modelisation d’un puzzle de logique comme un CSP :
Norwegian == 0, Milk == 2) suffisent a declencher une reduction en cascade jusqu’a la solution unique.Points cles : - Un puzzle qu’un humain resout en une trentaine de minutes tombe en millisecondes : la propagation globale ecrase la deduction pas-a-pas. - L’encodage est decisif : “voisin de” devient |X - Y| == 1, une disjonction lineaire directement exploitable. - Le même schema (domaine + Distinct + egalites/adjacences) s’adapte a tout puzzle de logique a attributs croises, quelle que soit sa taille.
Reference : le Zebra puzzle publie par Michael K. Albert et popularise par Life International (1962). L’attribution a Einstein est une legende urbaine - le puzzle est vraisemblablement de la presse americaine des annees 1960.