Twin C# de Z3-01-Introduction-Python.ipynb (parite .NET, marathon #4956).
Navigation : Index | Index SMT | Index SymbolicAI | << 01 - Introduction (Python) | 02 - Sudoku (C#) >>
Ce notebook est l’equivalent .NET de l’introduction au solveur SMT Z3. Il utilise le moteur reel Microsoft.Z3 (binding .NET officiel de Z3), le même solveur que la version Python (z3-solver), via le package NuGet Microsoft.Z3. Aucune re-implementation jouet : les contraintes sont resolues par le vrai moteur SOTA.
.NET (C#) (.NET Interactive).Microsoft.Z3 est restaure automatiquement par la première cellule.z3-solver, celui des notebooks Python de la série, par Z3NativeLoader.cs (voir l’en-tête du fichier). Pour retrouver exactement les sorties de ce notebook : pip install z3-solver==4.12.2.0, la version du package NuGet.Imports OK : Microsoft.Z3 version Z3 4.12.2.0On cherche deux entiers x et y tels que x + y = 10, x > 0, y > 0, et x > y. Z3 construit un Solver, on ajoute les contraintes, puis on appelle Check() qui renvoie un statut (SATISFIABLE, UNSATISFIABLE, UNKNOWN).
Pourquoi commencer par un système linéaire simple : c’est le cas où la décision (SAT/UNSAT) et la valeur (le modèle) sont l’une et l’autre triviales à vérifier à la main — x=9, y=1 satisfait x+y=10, x>y, x>0, y>0. L’enjeu n’est pas la difficulté du problème mais la mécanique de l’API : déclarer les constantes (MkIntConst), ajouter les assertions (solver.Assert), appeler Check(), récupérer le modèle (solver.Model). Maîtriser ce pipeline sur un cas évident permet ensuite de l’appliquer à des systèmes où la réponse n’est plus devinable — c’est l’escalier pédagogique classique du SMT : on apprend l’outil sur un problème qu’on sait résoudre sans lui.
var ctx1 = new Context();
var x = ctx1.MkIntConst("x");
var y = ctx1.MkIntConst("y");
var s = ctx1.MkSolver();
s.Add(ctx1.MkEq(ctx1.MkAdd(x, y), ctx1.MkInt(10)));
s.Add(ctx1.MkGt(x, ctx1.MkInt(0)));
s.Add(ctx1.MkGt(y, ctx1.MkInt(0)));
s.Add(ctx1.MkGt(x, y));
var resultat = s.Check();
Console.WriteLine("Resultat de s.Check() : " + resultat);
if (resultat == Status.SATISFIABLE)
{
var m = s.Model;
long xv = ((IntNum)m.Evaluate(x)).Int64;
long yv = ((IntNum)m.Evaluate(y)).Int64;
Console.WriteLine("Modele trouve :");
Console.WriteLine(" x = " + xv);
Console.WriteLine(" y = " + yv);
Console.WriteLine(" Verification : x + y = " + (xv + yv));
}Resultat de s.Check() : SATISFIABLE
Modele trouve :
x = 9
y = 1
Verification : x + y = 10Deux contraintes contradictoires (x > 5 ET x < 3) renvoient UNSATISFIABLE. Pour identifier quelles contraintes sont en conflit, on nomme chaque assertion avec AssertAndTrack puis on recupere le noyau (unsat core) : l’ensemble minimal de contraintes qui suffisent a provoquer l’insatisfiabilite.
Pourquoi le noyau d’insatisfiabilité est la fonctionnalité distinctive : un simple UNSATISFIABLE dit qu’il n’y a pas de solution mais pas pourquoi. Sur un système de contraintes réel (spécification d’un système, configuration d’un produit, règles métier), l’utilisateur a besoin de la contre-explication — quel sous-ensemble de règles se contredit. AssertAndTrack étiquette chaque assertion d’un booléen, et le solveur renvoie, parmi ces étiquettes, le sous-ensemble minimal qui reste insatisfiable. C’est ce qui distingue un SMT d’un simple solveur SAT : la traçabilité du conflit, pas seulement son existence. En production, c’est l’outil qui transforme « votre configuration est invalide » en « les règles R2 et R3 sont incompatibles ».
Lecture du noyau d’insatisfiabilité — le solveur renvoie UNSATISFIABLE pour x > 5 et x < 3, et le noyau [c2, c1] : les deux contraintes nommées suffisent à provoquer le conflit. L’ordre [c2, c1] reflète l’ordre d’exploration interne du solveur, pas une priorité — le noyau est un ensemble, sa liste n’a pas de sens séquentiel.
Pourquoi ce noyau est la preuve que le solveur a compris le conflit : sur un exemple à deux contraintes, l’insatisfiabilité est évidente à l’œil nu. Mais imaginez 200 contraintes métier où une spécification est invalide — sans noyau, l’utilisateur sait seulement « ça ne marche pas » ; avec le noyau, il sait exactement quelles 2 ou 3 règles se contredisent parmi les 200. C’est la valeur ajoutée qui distingue Z3 d’un solveur ad-hoc : la diagnosticabilité. En pédagogie, cela apprend à l’élève qu’un solveur n’est pas une boîte noire qui dit non — c’est un outil qui explique son verdict, condition indispensable pour débugger une modélisation.
var ctx2 = new Context();
var x2 = ctx2.MkIntConst("x");
var s2 = ctx2.MkSolver();
s2.Add(ctx2.MkGt(x2, ctx2.MkInt(5)));
s2.Add(ctx2.MkLt(x2, ctx2.MkInt(3)));
Console.WriteLine("Contraintes : x > 5 ET x < 3");
Console.WriteLine("Resultat de s.check() : " + s2.Check());
// Noyau d insatisfiabilite via AssertAndTrack.
var s3 = ctx2.MkSolver();
var c1 = ctx2.MkBoolConst("c1");
var c2 = ctx2.MkBoolConst("c2");
s3.AssertAndTrack(ctx2.MkGt(x2, ctx2.MkInt(5)), c1);
s3.AssertAndTrack(ctx2.MkLt(x2, ctx2.MkInt(3)), c2);
Console.WriteLine();
Console.WriteLine("Avec AssertAndTrack :");
Console.WriteLine("Resultat : " + s3.Check());
var core = s3.UnsatCore;
var sb = new System.Text.StringBuilder();
for (int k = 0; k < core.Length; k++) { if (k > 0) sb.Append(", "); sb.Append(core[k]); }
Console.WriteLine("Noyau d insatisfiabilite (contraintes en conflit) : [" + sb + "]");Contraintes : x > 5 ET x < 3
Resultat de s.check() : UNSATISFIABLE
Avec AssertAndTrack :
Resultat : UNSATISFIABLE
Noyau d insatisfiabilite (contraintes en conflit) : [c2, c1]Trois personnes A, B, C. A affirme que B ment, B affirme que C ment, C affirme que A et B mentent tous les deux. Modelise en logique booleenne : A == non B, B == non C, C == (non A et non B). Z3 trouve qui dit la verite.
Pourquoi la logique booléenne est un registre différent de l’arithmétique : ici les variables sont des propositions (vrai/faux), pas des entiers. L’astuce de modélisation est de fusioner deux niveaux — la valeur de vérité de chaque personne (A = « A dit la vérité ») ET le contenu de son affirmation (« B ment » = non B). La contrainte A == non B encode : si A dit la vérité, alors B ment. C’est le pont entre logique propositionnelle et théorie des puzzles (knights and knaves). Z3 résout cela par SAT booléen pur, sans arithmétique — c’est une autre théorie du solveur, et la force d’un SMT est précisément de mélanger les théories (booléen + arithmétique + tableaux) dans un même Context.
var ctx3 = new Context();
var A = ctx3.MkBoolConst("A");
var B = ctx3.MkBoolConst("B");
var C = ctx3.MkBoolConst("C");
var s = ctx3.MkSolver();
s.Add(ctx3.MkEq(A, ctx3.MkNot(B)));
s.Add(ctx3.MkEq(B, ctx3.MkNot(C)));
s.Add(ctx3.MkEq(C, ctx3.MkAnd(ctx3.MkNot(A), ctx3.MkNot(B))));
Console.WriteLine("Resultat : " + s.Check());
var m = s.Model;
bool av = ((BoolExpr)m.Evaluate(A)).BoolValue == Z3_lbool.Z3_L_TRUE;
bool bv = ((BoolExpr)m.Evaluate(B)).BoolValue == Z3_lbool.Z3_L_TRUE;
bool cv = ((BoolExpr)m.Evaluate(C)).BoolValue == Z3_lbool.Z3_L_TRUE;
Console.WriteLine("A dit la verite : " + av);
Console.WriteLine("B dit la verite : " + bv);
Console.WriteLine("C dit la verite : " + cv);
string veridique = av ? "A" : (bv ? "B" : "C");
Console.WriteLine();
Console.WriteLine("Synthese : " + veridique + " dit la verite.");Resultat : SATISFIABLE
A dit la verite : False
B dit la verite : True
C dit la verite : False
Synthese : B dit la verite.RealTrois enfants se partagent 10 euros : l’aine recoit le double du cadet, le benjamin recoit 1 euro de plus que le cadet. Z3 resout en arithmetique rationnelle exacte (fractions, pas de flottants) : cadet = 9/4, aine = 9/2, benjamin = 13/4.
Pourquoi l’arithmétique rationnelle exacte compte : un solveur en flottants (Double en C#) donnerait 2,25, 4,5, 3,25 — des valeurs approchées soumises aux erreurs d’arrondi. Z3 en Real manipule des fractions exactes (9/4), sans aucune perte de précision, parce qu’il résout par simplex sur les rationnels (théorie QF_LRA sous le capot). Pour un problème de partage où la vérification aîné = 2×cadet doit tenir exactement, l’arithmétique exacte garantit que la solution satisfait les contraintes à l’égalité près, pas à un epsilon près. C’est l’écart entre un solveur numérique (approché, rapide) et un solveur formel (exact, certifié) — le SMT est du second type.
var ctx4 = new Context();
var aine = ctx4.MkRealConst("aine");
var cadet = ctx4.MkRealConst("cadet");
var benjamin = ctx4.MkRealConst("benjamin");
var s = ctx4.MkSolver();
s.Add(ctx4.MkEq(ctx4.MkAdd(aine, cadet, benjamin), ctx4.MkReal(10)));
s.Add(ctx4.MkEq(aine, ctx4.MkMul(ctx4.MkReal(2), cadet)));
s.Add(ctx4.MkEq(benjamin, ctx4.MkAdd(cadet, ctx4.MkReal(1))));
Console.WriteLine("Partage de 10 euros : " + s.Check());
var m = s.Model;
Console.WriteLine(" Aine : " + m.Evaluate(aine) + " euros");
Console.WriteLine(" Cadet : " + m.Evaluate(cadet) + " euros");
Console.WriteLine(" Benjamin : " + m.Evaluate(benjamin) + " euros");Partage de 10 euros : SATISFIABLE
Aine : 9/2 euros
Cadet : 9/4 euros
Benjamin : 13/4 eurosTrois objets A (valeur 4, poids 2), B (valeur 5, poids 3), C (valeur 7, poids 5). Capacite maximale 10 kg. On veut maximiser la valeur transportee. Z3 fournit un Optimize qui accepte un objectif MkMaximize.
Pourquoi l’optimisation est l’étape qui justifie le SMT contre un solveur SAT : un SAT solver répond existe-t-il une solution ; un SMT avec Optimize répond quelle est la meilleure solution. Le sac à dos est l’archétype : parmi toutes les allocations satisfaisant la contrainte de poids, on veut maximiser la valeur. Z3 fait cela par optimisation linéaire en entiers (branche OMT — Optimization Modulo Theories) : il explore l’espace des solutions en suivant l’objectif. C’est le pont entre décision (SAT) et optimisation (max/min) — et c’est ce qui rend le SMT pertinent pour des problèmes d’ordonnancement, d’allocation de ressources, de planification sous contraintes, là où un simple solveur SAT s’arrête au premier modèle satisfaisant.
Lecture du résultat d’optimisation — Z3 renvoie la solution optimale : 5 unités d’objet A (valeur 4×5 = 20), 0 unités de B et C, pour un poids total de 10/10 kg (capacité saturée) et une valeur totale de 20. Ce n’est pas une solution quelconque satisfaisant la contrainte de poids — c’est la meilleure selon l’objectif MkMaximize.
Ce que ce résultat enseigne sur la différence décision/optimisation : un solveur SAT pur se serait arrêté à la première allocation valide (par exemple 2 unités de A + 2 de B = valeur 18, poids 10) et aurait déclaré SATISFIABLE. Le Optimize de Z3 a continué l’exploration jusqu’à prouver qu’aucune allocation ne dépasse la valeur 20 — c’est la garantie d’optimalité, pas juste l’existence. Pour un enseignant, c’est le point clé : le SMT ne cherche pas une solution, il caractérise tout l’espace et en extrait l’extrémum. C’est aussi pourquoi l’objet A (meilleur ratio valeur/poids = 2) remplit seul la capacité : le solveur a implicitement appliqué le raisonnement glouton du ratio, sans qu’on le code.
var ctx5 = new Context();
var n_a = ctx5.MkIntConst("n_a");
var n_b = ctx5.MkIntConst("n_b");
var n_c = ctx5.MkIntConst("n_c");
var opt = ctx5.MkOptimize();
opt.Add(ctx5.MkGe(n_a, ctx5.MkInt(0)));
opt.Add(ctx5.MkGe(n_b, ctx5.MkInt(0)));
opt.Add(ctx5.MkGe(n_c, ctx5.MkInt(0)));
opt.Add(ctx5.MkLe(ctx5.MkAdd(ctx5.MkMul(ctx5.MkInt(2), n_a), ctx5.MkMul(ctx5.MkInt(3), n_b), ctx5.MkMul(ctx5.MkInt(5), n_c)), ctx5.MkInt(10)));
var valeur = ctx5.MkAdd(ctx5.MkMul(ctx5.MkInt(4), n_a), ctx5.MkMul(ctx5.MkInt(5), n_b), ctx5.MkMul(ctx5.MkInt(7), n_c));
opt.MkMaximize(valeur);
Console.WriteLine("Optimisation : " + opt.Check());
var m = opt.Model;
long na = ((IntNum)m.Evaluate(n_a)).Int64;
long nb = ((IntNum)m.Evaluate(n_b)).Int64;
long nc = ((IntNum)m.Evaluate(n_c)).Int64;
Console.WriteLine("Solution optimale :");
Console.WriteLine(" Objet A (v=4, p=2) : " + na + " unites");
Console.WriteLine(" Objet B (v=5, p=3) : " + nb + " unites");
Console.WriteLine(" Objet C (v=7, p=5) : " + nc + " unites");
Console.WriteLine(" Poids total : " + (2*na + 3*nb + 5*nc) + " / 10 kg");
Console.WriteLine(" Valeur totale : " + (4*na + 5*nb + 7*nc));Optimisation : SATISFIABLE
Solution optimale :
Objet A (v=4, p=2) : 5 unites
Objet B (v=5, p=3) : 0 unites
Objet C (v=7, p=5) : 0 unites
Poids total : 10 / 10 kg
Valeur totale : 20Trois exercices a completer. Les stubs retournent null : a vous d’implementer la resolution avec Z3. Objectif pedagogique : manipuler Solver, Optimize, Check, Model.
// EXERCICE 1 : Trouver un triplet pythagoricien avec Z3.
// Retourne (a, b, c) tel que a^2 + b^2 = c^2, avec a < b < c <= borneMax.
// Indice : creez un Solver, des variables Int, ajoutez les contraintes, puis Check() et Model.
// Etape 1 : declarer les variables a, b, c
// Etape 2 : ajouter a*a + b*b == c*c et les bornes a < b < c <= borneMax
// Etape 3 : extraire le modele et retourner (a, b, c)
(long A, long B, long C)? TrouverTripletPythagoricien(int borneMax = 20)
{
// TODO etudiant : implementez la resolution avec un Solver Z3
return null; // TODO etudiant : remplacer par le triplet trouve
}
var triplet = TrouverTripletPythagoricien(20);
Console.WriteLine("Triplet pythagoricien : " + (triplet.HasValue ? triplet.ToString() : "(a completer)"));Triplet pythagoricien : (a completer)// EXERCICE 2 : Ordonnancer deux taches sans chevauchement.
// Planifier T1 (3h) et T2 (2h) sans chevauchement, T2 finissant au plus tot.
// Indice : utilisez Optimize avec debut_T1 >= 0, debut_T2 >= 0.
// Etape 1 : declarer debut_T1, debut_T2
// Etape 2 : contrainte debut_T2 >= debut_T1 + 3 (pas de chevauchement, T1 avant)
// Etape 3 : minimiser debut_T2 + 2 (fin de T2)
(long DebutT1, long DebutT2)? OrdonnancerTaches()
{
// TODO etudiant : implementez l ordonnancement optimal avec Optimize
return null; // TODO etudiant : remplacer par (debut_T1, debut_T2)
}
var planning = OrdonnancerTaches();
Console.WriteLine("Planning optimal : " + (planning.HasValue ? planning.ToString() : "(a completer)"));Planning optimal : (a completer)// EXERCICE 3 : Maximiser le profit de production sous contrainte de machine.
// Produits P et Q. p >= 2, q >= 2, 2*p + 4*q <= 20. Maximiser 30*p + 50*q.
// Indice : utilisez Optimize, declarez p et q (Int), ajoutez les contraintes, maximizez.
// Etape 1 : declarer p, q (Int)
// Etape 2 : ajouter les contraintes de production
// Etape 3 : MkMaximize(30*p + 50*q) et extraire le modele
(long P, long Q, long Profit)? AllocationOptimale()
{
// TODO etudiant : implementez l allocation optimale avec Optimize
return null; // TODO etudiant : remplacer par (p, q, profit)
}
var res = AllocationOptimale();
Console.WriteLine("Allocation optimale : " + (res.HasValue ? res.ToString() : "(a completer)"));Allocation optimale : (a completer)Ce twin C# couvre les mêmes concepts que la version Python : Satisfiabilite (Solver, Check, Model), noyau d’insatisfiabilite (AssertAndTrack, UnsatCore), logique booleenne (BoolConst, MkNot, MkAnd), arithmetique rationnelle exacte (Real, fractions), et optimisation (Optimize, MkMaximize).
Le binding Microsoft.Z3 expose exactement le même moteur Z3 que z3-solver (Python) : les résultats sont identiques, seuls l’API et le langage changent. C’est l’illustration qu’un solveur SMT SOTA est utilisable de facon native en .NET.