Navigation : Index SymbolicAI | Série Z3 | >> Sudoku Théorem vs Array
À la fin de ce notebook, vous saurez : 1. Comprendre le concept de programmation déclarative vs impérative 2. Utiliser Z3.Linq pour exprimer des contraintes avec la syntaxe LINQ 3. Résoudre des problèmes de satisfaction de contraintes (CSP) 4. Optimiser des solutions avec Solve() et Optimize()
Ce notebook explore Z3.Linq, une bibliothèque qui combine le solveur SMT Z3 avec la syntaxe LINQ de C# pour exprimer des contraintes de manière déclarative.
Contexte : Z3.Linq est issu du travail de Ricardo Niepel (2015), enrichi par les contributions de jsboige (arrays, objets hiérarchiques, listes imbriquées, 2018-2023), puis modernisé par endjin (2022+). Le fork MyIntelligenceAgency/Z3.Linq maintient la version utilisée dans cette série.
#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.Text; using System.Diagnostics; using System.Linq;
Console.WriteLine("Imports OK : Z3.Linq (.deploy fork), Microsoft.Z3, System.Linq");Imports OK : Z3.Linq (.deploy fork), Microsoft.Z3, System.LinqZ3.Linq est une bibliothèque qui combine deux technologies puissantes:
Avantage principal: Au lieu d’écrire du code impératif pour résoudre un problème, on déclare les contraintes et Z3 trouve une solution (si elle existe).
Cas d’usage typiques: - Résolution de systèmes d’équations - Problèmes de planification et d’ordonnancement - Vérification formelle - Puzzles logiques (Sudoku, n-Queens, etc.)
Le diagramme ci-dessous illustre le chemin complet d’une contrainte LINQ jusqu’à l’objet C# résultat :
flowchart LR
L["Lambda .Where(x => ...)"] --> V["ExpressionVisitor"]
V --> E["BoolExpr Z3"]
E --> S["Solveur SMT"]
S -- SAT --> M["Modèle Z3"]
S -- UNSAT --> N["null"]
M --> T["Objet .NET T"]Point clé : l’ExpressionVisitor traduit chaque nœud de l’arbre AST C# (BinaryExpression, MemberAccess, opérateurs arithmétiques) en son équivalent Z3. C’est cette couche qui rend la déclaration de contraintes déclarative plutôt qu’impérative — on exprime quoi, pas comment.
using Z3.Linq;
using (var ctx = new Z3Context())
{
var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}", solution.X1, solution.X2, solution.X3, solution.X4, solution.X5);
}X1 = 3, X2 = 0, X3 = 1, X4 = 0, X5 = 1Ce que fait le code:
Le code définit un système de 5 contraintes linéaires sur 5 variables entières (X1, X2, X3, X4, X5):
X1 - X2 ∈ [1, 3] (deux contraintes)
X1 = 2·X3 + X5
X3 = X5
X2 = 6·X4Syntaxe LINQ To Z3: - ctx.NewTheorem<Symbols<int, int, int, int, int>>(): Crée un théorème avec 5 variables entières - where t.X1 - t.X2 >= 1: Ajoute une contrainte (traduite en formule SMT) - theorem.Solve(): Demande à Z3 de trouver une affectation satisfaisant toutes les contraintes
Résultat attendu:
Le solveur Z3 trouve une solution (il peut y en avoir plusieurs). L’exécution ci-dessus donne par exemple : - Une affectation valide : X1 = 3, X2 = 0, X3 = 1, X4 = 0, X5 = 1
Note: Z3 est un solveur SMT (Satisfiability Modulo Théories) capable de résoudre des contraintes sur des entiers, des réels, des tableaux, etc. LINQ To Z3 offre une interface C# naturelle pour exprimer ces contraintes. Pour les fondements théoriques de la résolution SMT (DPLL(T)) et la présentation du solveur Z3 lui-même, voir de Moura & Bjørner, Z3: An Efficient SMT Solver (TACAS 2008) et Nieuwenhuis, Oliveras & Tinelli, Solving SAT and SAT Modulo Théories: From an Abstract DPLL Procedure to DPLL(T) (JACM 2006) ; la théorie des tableaux (notebook 4) et le standard SMT-LIB (notebooks 4, 10) sont ancrés dans la section Références du README.
Jusqu’ici, chaque appel à Solve() a renvoyé une solution. Mais la question fondamentale que tranche un solveur SMT n’est pas « quelle est la solution ? » — c’est « une solution existe-t-elle ? ». C’est ce que désigne le S de SMT : Satisfiability.
Solve() renvoie alors une telle affectation.Solve() renvoie alors null (Z3 a prouvé qu’aucune solution n’existe).Cette distinction est centrale : l’une des réponses les plus utiles d’un solveur est « c’est impossible », et cette réponse est une preuve (pas une absence de résultat). Par exemple, prouver qu’un planning est irréalisable sous certaines contraintes, ou qu’un invariant de sécurité ne peut jamais être violé. Le (si elle existe) de la section précédente prend ici tout son sens.
L’exemple ci-dessous force un système UNSAT : la même variable ne peut pas être à la fois > 5 et < 3.
// Exemple : un système UNSAT (insatisfiable)
// La variable X1 doit être à la fois > 5 ET < 3 -- contradiction, aucune solution.
using (var ctx = new Z3Context())
{
var theorem = ctx.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 > 5)
.Where(t => t.X1 < 3);
var solution = theorem.Solve();
Console.WriteLine($"Solve() a renvoyé : {(solution == null ? "null -> le système est UNSAT (aucune affectation possible)" : solution.ToString())}");
}Solve() a renvoyé : null -> le système est UNSAT (aucune affectation possible)Énoncé classique: 3 missionnaires et 3 cannibales doivent traverser une rivière à l’aide d’une barque pouvant transporter au maximum 2 personnes. Si à un moment donné, sur l’une des deux rives, les cannibales sont plus nombreux que les missionnaires, ces derniers se font dévorer.
Objectif: Trouver une séquence de traversées permettant à tous de passer sains et saufs.
Modélisation pour Z3.Linq: - Variables: État de chaque rive à chaque étape (nombre de missionnaires et cannibales) - Contraintes: Capacité de la barque, sécurité des missionnaires, état initial/final - Solution: Séquence d’états satisfaisant toutes les contraintes
La classe suivante encode ce problème de manière déclarative pour être résolu par Z3.
La classe CanibalsAndMissionaries encode le problème en trois parties:
| Variable | Type | Signification |
|---|---|---|
Missionaries[i] |
int[] |
Nombre de missionnaires sur la rive de départ à l’étape i |
Canibals[i] |
int[] |
Nombre de cannibales sur la rive de départ à l’étape i |
Length |
int |
Nombre total d’étapes dans le chemin |
Note: La rive d’arrivée se déduit par soustraction:
MissionnairesArrivée = NbMissionaries - Missionaries[i]
Contraintes globales: - État initial: Tous les missionnaires et cannibales sont sur la rive de départ - État final: Tous sont sur la rive d’arrivée (0 personnes sur la rive de départ)
Contraintes de transition (modèle d’actions): - Étapes paires (i % 2 == 0): La barque traverse de départ vers arrivée → perte de 1 à SizeBoat personnes - Étapes impaires (i % 2 == 1): La barque revient d’arrivée vers départ → gain de 1 à SizeBoat personnes
Contrainte de sécurité (invariant critique):
La méthode Create() construit progressivement le théorème en ajoutant des clauses Where(): - Chaque appel à Where() ajoute une contrainte SMT - La boucle for génère des contraintes pour chaque étape du chemin - Z3.Linq traduit automatiquement les expressions lambda en formules logiques
Cette approche déclarative contraste avec la programmation impérative classique: on décrit quoi trouver, pas comment le trouver.
L’affirmation des contraintes des arbres d’expression LINQ sur la classe d’état et l’étape suivante. On se base pour ça sur la classe Theorem de LINQ To Z3 :
public class CanibalsAndMissionaries
{
// Le nombre de canibales et missionaires (3 dans le problème original)
public int NbMissionaries { get; set; } = 3;
// La taille de la barque (2 dans le projet original)
public int SizeBoat { get; set; } = 2;
// La longueur du chemin calculé
private int _length;
//La propriété qui permet d'accéder à la taille du chemin dans Z3
public int Length
{
get => _length;
set
{
_length = value;
// Quand la longueur est déterminée par Z3, on initialise les tableaux pour pouvoir récupérer les valeurs
Canibals = new int[value];
Missionaries = new int[value];
}
}
// Un tableau contenant à chaque étape le nombre de canibales sur la berge de départ
public int[] Canibals { get; set; }
// Un tableau contenant à chaque étape le nombre de missionaires sur la berge de départ
public int[] Missionaries { get; set; }
/// <summary>
/// Une représentation lisible de la solution proposée
/// </summary>
/// <returns>une chaine de caractère ou chaque ligne est une étape du chemin</returns>
public override string ToString()
{
var sb = new StringBuilder();
for (int i = 0; i < Canibals.Length; i++)
{
sb.AppendLine($"{i + 1} - (({Missionaries[i]}M, {Canibals[i]}C, {1 - i % 2}), ({(i % 2)}, {NbMissionaries - Missionaries[i]}M, {NbMissionaries - Canibals[i]}C))");
}
return sb.ToString();
}
/// <summary>
/// La méthode qui permet la création du théorème associé au problème
/// </summary>
/// <param name="context">Le contexte Z3 qui devra interpréter les contraintes</param>
/// <param name="entity">Une valeur du problème servant de modèle pour définir les paramètres principaux</param>
/// <returns>Un théorème de notre environnement qui peut être filtré et résolu</returns>
public static Theorem<CanibalsAndMissionaries> Create(Z3Context context, CanibalsAndMissionaries entity)
{
// On créée une instance du théorème, sans contraintes, puis on va rajouter les contraintes une à une
var theorem = context.NewTheorem<CanibalsAndMissionaries>();
// Contraintes globales
// On récupère les contraintes globales qui seront injectées sous forme de constante dans la lambda expression
var sizeBoat = entity.SizeBoat;
int nbMissionaries = entity.NbMissionaries;
int maxlength = entity.Length;
theorem = theorem.Where(caM => caM.NbMissionaries == nbMissionaries);
theorem = theorem.Where(caM => caM.SizeBoat == sizeBoat);
// Etat initial
theorem = theorem.Where(caM => caM.Missionaries[0] == caM.NbMissionaries && caM.Canibals[0] == caM.NbMissionaries);
//Modèle de transition
// On filtre à chaque étape selon les actions possible
for (int iclosure = 0; iclosure < maxlength; iclosure++)
{
var i = iclosure;
//Les deux rives contiennent entre 0 et 3 personnes
theorem = theorem.Where(caM => caM.Canibals[i] >= 0
&& caM.Canibals[i] <= caM.NbMissionaries
&& caM.Missionaries[i] >= 0
&& caM.Missionaries[i] <= caM.NbMissionaries);
if (i % 2 == 0)
{
// Aux itérations paires, la rive de départ perd entre 1 et SizeBoat personnes
theorem = theorem.Where(caM => caM.Canibals[i + 1] <= caM.Canibals[i]
&& caM.Missionaries[i + 1] <= caM.Missionaries[i]
&& caM.Canibals[i + 1] + caM.Missionaries[i + 1] - caM.Canibals[i] - caM.Missionaries[i] < 0
&& caM.Canibals[i + 1] + caM.Missionaries[i + 1] - caM.Canibals[i] - caM.Missionaries[i] >= -caM.SizeBoat);
}
else
{
// Aux itérations impaires, la rive de départ gagne entre 1 et SizeBoat personnes
theorem = theorem.Where(caM =>
caM.Canibals[i + 1] >= caM.Canibals[i]
&& caM.Missionaries[i + 1] >= caM.Missionaries[i]
&& caM.Canibals[i + 1] + caM.Missionaries[i + 1] - caM.Canibals[i] - caM.Missionaries[i] > 0
&& caM.Canibals[i + 1] + caM.Missionaries[i + 1] - caM.Canibals[i] - caM.Missionaries[i] <= caM.SizeBoat);
}
//Jamais moins de missionnaire que de cannibal sur chacune des rives
theorem = theorem.Where(caM => (caM.Missionaries[i] == 0 || (caM.Missionaries[i] >= caM.Canibals[i]))
&& (caM.Missionaries[i] == caM.NbMissionaries || ((caM.NbMissionaries - caM.Missionaries[i]) >= (caM.NbMissionaries - caM.Canibals[i]))));
}
// Test de but
// A l'arrivée, plus personne sur la rive de départ
theorem = theorem.Where(
caM => caM.Length > 0
&& caM.Length < maxlength
&& caM.Missionaries[caM.Length - 1] == 0
&& caM.Canibals[caM.Length - 1] == 0
);
return theorem;
}
}LINQ To Z3 nous donne la solution sous forme d’ un objet POCO (Plain Old CLR Object) du type de paramètre générique T du théorème.
using System.Diagnostics;
var stopWatch = new Stopwatch();
stopWatch.Start();
TimeSpan debutChrono;
// Solving Canibals & Missionaires
var can = new CanibalsAndMissionaries(){NbMissionaries = 3, SizeBoat = 2, Length = 30};
using (var ctx = new Z3Context())
{
var theorem = CanibalsAndMissionaries.Create(ctx, can);
debutChrono = stopWatch.Elapsed;
//Print(theorem);
var result = theorem.Solve();
// affichage du résultat
display($"Durée Cannibales et Missionaires {stopWatch.Elapsed - debutChrono}");
display(result);
}Durée Cannibales et Missionaires 00:00:00.32187331 - ((3M, 3C, 1), (0, 0M, 0C))\r\n2 - ((2M, 2C, 0), (1, 1M, 1C))\r\n3 - ((3M, 3C, 1), (0, 0M, 0C))\r\n4 - ((2M, 2C, 0), (1, 1M, 1C))\r\n5 - ((3M, 3C, 1), (0, 0M, 0C))\r\n6 - ((2M, 2C, 0), (1, 1M, 1C))\r\n7 - ((3M, 2C, 1), (0, 0M, 1C))\r\n8 - ((2M, 2C, 0), (1, 1M, 1C))\r\n9 - ((3M, 2C, 1), (0, 0M, 1C...| NbMissionaries | |
| SizeBoat | |
| Length | |
| Canibals | |
| Missionaries | |
Le code ci-dessus résout le problème classique des 3 missionnaires et 3 cannibales avec une barque de capacité 2.
Paramètres du problème: - NbMissionaries = 3: 3 missionnaires et 3 cannibales - SizeBoat = 2: La barque peut transporter au maximum 2 personnes - Length = 30: Limite supérieure du nombre d’étapes à explorer
Sortie attendue: - Un chemin solution avec le nombre d’étapes nécessaires - Chaque ligne au format: (MissionnairesDépart, CannibalsDépart, Barque), (Barque, MissionnairesArrivée, CannibalesArrivée) - La durée d’exécution du solveur Z3
Note: La méthode
Solve()trouve une solution satisfaisant les contraintes, mais pas nécessairement la plus courte. Pour obtenir la solution optimale, il faut utiliserOptimize()(voir section suivante).
Il s’agit de placer N reines sur un echiquier NxN de sorte qu’aucune ne soit sur la même ligne, colonne ou diagonale qu’une autre.
Objectif : Modelisez un echiquier 4x4 avec Z3.Linq. Chaque variable represente la colonne de la reine sur la ligne correspondante.
Indices : - Utilisez Symbols<int, int, int, int> pour un echiquier 4x4 - Contrainte 1 : toutes les colonnes différentes (Q1 != Q2 != Q3 != Q4) - Contrainte 2 : pas de diagonale => |Qi - Qj| != |i - j| - Utilisez Math.Abs pour la valeur absolue des différences
// Exercice 2 : n-Queens 4x4 avec Z3.Linq
// TODO etudiant : placez 4 reines sur un echiquier 4x4
// Etape 1 : definissez un theoreme avec 4 variables (Q1, Q2, Q3, Q4)
// Etape 2 : ajoutez les contraintes de colonnes distinctes
// Etape 3 : ajoutez les contraintes anti-diagonales
// Indice : Math.Abs(Qi - Qj) != Math.Abs(i - j) pour i != j
// using (var ctx = new Z3Context())
// {
// var theorem = from q in ctx.NewTheorem<Symbols<int, int, int, int>>()
// where ... // Vos contraintes de colonnes distinctes
// where ... // Vos contraintes anti-diagonales
// select q;
// var solution = theorem.Solve();
// Console.WriteLine($"Q1={solution.X1}, Q2={solution.X2}, Q3={solution.X3}, Q4={solution.X4}");
// }
Console.WriteLine("Exercice a completer : n-Queens 4x4 avec Z3.Linq");Exercice a completer : n-Queens 4x4 avec Z3.Linqusing System.Diagnostics;
var stopWatch = new Stopwatch();
stopWatch.Start();
TimeSpan debutChrono;
// Solving Canibals & Missionaires
var can = new CanibalsAndMissionaries(){NbMissionaries = 3, SizeBoat = 2, Length = 30};
using (var ctx = new Z3Context())
{
var theorem = CanibalsAndMissionaries.Create(ctx, can);
debutChrono = stopWatch.Elapsed;
//Print(theorem);
var result = theorem.Optimize(Optimization.Minimize, objMnC => objMnC.Length);
// affichage du résultat
display($"Durée Cannibales et Missionaires {stopWatch.Elapsed - debutChrono}");
display(result);
}
Durée Cannibales et Missionaires 00:00:00.13765391 - ((3M, 3C, 1), (0, 0M, 0C))\r\n2 - ((2M, 2C, 0), (1, 1M, 1C))\r\n3 - ((3M, 2C, 1), (0, 0M, 1C))\r\n4 - ((3M, 0C, 0), (1, 0M, 3C))\r\n5 - ((3M, 1C, 1), (0, 0M, 2C))\r\n6 - ((1M, 1C, 0), (1, 2M, 2C))\r\n7 - ((2M, 2C, 1), (0, 1M, 1C))\r\n8 - ((0M, 2C, 0), (1, 3M, 1C))\r\n9 - ((0M, 3C, 1), (0, 3M, 0C...| NbMissionaries | |
| SizeBoat | |
| Length | |
| Canibals | |
| Missionaries | |
Différence entre Solve() et Optimize():
Solve(): Trouve une solution satisfaisant toutes les contraintes, sans garantie d’optimalitéOptimize(Optimization.Minimize, objMnC => objMnC.Length): Trouve la solution avec la plus petite valeur de LengthDans le cas des missionnaires et cannibales, cela signifie: - Solve() peut retourner un chemin de 15 étapes alors qu’il existe un chemin de 11 étapes - Optimize() garantit de trouver le chemin le plus court possible
Performance: L’optimisation est plus coûteuse en temps de calcul, car le solveur doit explorer l’espace de recherche pour prouver qu’aucune solution plus courte n’existe.
Résultat attendu: Le chemin optimal pour 3 missionnaires et 3 cannibales avec une barque de capacité 2 est de 11 étapes.
using System.Diagnostics;
var stopWatch = new Stopwatch();
stopWatch.Start();
TimeSpan debutChrono;
// Solving Canibals & Missionaires
var can = new CanibalsAndMissionaries(){NbMissionaries = 30, SizeBoat = 7, Length = 100};
using (var ctx = new Z3Context())
{
var theorem = CanibalsAndMissionaries.Create(ctx, can);
debutChrono = stopWatch.Elapsed;
//Print(theorem);
var result = theorem.Optimize(Optimization.Minimize, objMnC => objMnC.Length);
// affichage du résultat
display($"Durée Cannibales et Missionaires {stopWatch.Elapsed - debutChrono}");
display(result);
}
Durée Cannibales et Missionaires 00:01:20.17862191 - ((30M, 30C, 1), (0, 0M, 0C))\r\n2 - ((30M, 23C, 0), (1, 0M, 7C))\r\n3 - ((30M, 25C, 1), (0, 0M, 5C))\r\n4 - ((24M, 24C, 0), (1, 6M, 6C))\r\n5 - ((25M, 25C, 1), (0, 5M, 5C))\r\n6 - ((22M, 22C, 0), (1, 8M, 8C))\r\n7 - ((23M, 23C, 1), (0, 7M, 7C))\r\n8 - ((20M, 20C, 0), (1, 10M, 10C))\r\n9 - ((21M,...| NbMissionaries | |
| SizeBoat | |
| Length | |
| Canibals | |
| Missionaries | |
Generalisez le modèle des missionnaires-cannibales pour resoudre un problème voisin : un fermier doit traverser une riviere avec un loup, une chevre et un chou. La barque ne peut transporter que le fermier plus un seul item. Le loup mange la chevre et la chevre mange le chou s’ils restent seuls ensemble.
Objectif : Adaptez la classe CanibalsAndMissionaries ou créez un nouveau modèle Z3.Linq pour ce problème.
Indices : - Le fermier est toujours dans la barque (pas besoin de variable separree, il est implicite) - 3 items a transporter : L (loup), C (chevre), X (chou) - Invariant : le fermier ne peut pas laisser (L+C) ou (C+X) seuls sur une rive - Utilisez un codage similaire avec des tableaux pour les positions a chaque étape
// Exercice 3 : Loups, Chevres et Choux avec Z3.Linq
// TODO etudiant : modelisez le probleme du fermier, loup, chevre et chou
// Etape 1 : definissez les variables d'etat (positions de chaque item par etape)
// Etape 2 : ajoutez les contraintes de transition (1 seul item par traverse)
// Etape 3 : ajoutez les invariants de securite (pas L+C ni C+X seuls)
// Etape 4 : resolvez avec Optimize pour trouver le chemin le plus court
// Indice : vous pouvez utiliser Symbols<int, int, int> pour 3 positions
// ou creer une classe adaptee avec un tableau de positions
// public class FarmerProblem { ... }
// using (var ctx = new Z3Context()) { ... }
Console.WriteLine("Exercice a completer : loups, chevres et choux avec Z3.Linq");Exercice a completer : loups, chevres et choux avec Z3.Linqrecord positionnels (DSL NewTheorem<PositionalRecord>)L’environnement d’un théorème (le type T passe a NewTheorem<T>) peut etre un record positionnel C# – par exemple record Point(int X, int Y) – et non une class mutable. La reconstruction de la solution passe alors par une branche dediee du solveur (Theorem.cs:993-1099) qui selectionne le primary constructor du record, evalue chaque paramètre depuis le modèle Z3, puis invoque Activator.CreateInstance(t, args) avec les valeurs positionnelles – l’ancienne branche Activator.CreateInstance(t) throw sur un record sans constructeur sans paramètre (un positional record n’expose que des init-only setters).
Le mini-problème : sur un point (X, Y) dans le plan, trouver le point satisfaisant X + Y = 12 et X = 2·Y (solution unique attendue : X = 8, Y = 4).
Stack : A+B – le raw doit gerer manuellement la reconstruction via
Model.Evalsur chaqueIntExpr, tandis que le DSLNewTheorem<Point>().Where(...)invoque la brancheConstructFromModelautomatiquement ; l’objet rendu (Point { X = 8, Y = 4 }) est type C#, pas une paire deIntNum.
Ancre fork : Theorem.cs:993-1099 (branche ConstructFromModel), tests Z3.Linq.Tests/RecordEnvTheoryTests.cs:18-91 (4 cas : positional standard, scalaires mixtes int+bool, trois paramètres, UNSAT). La feature etait listee dans le backlog B9 d’#4688 avec une ancre « a confirmer » – le grep la trouve dans la branche reconstruction, pas dans la declaration de type (qui est du C# standard).
// B9 - Record positionnel "deux stacks" sur le meme probleme (X+Y=12, X=2Y).
// Un point (X, Y) dans le plan, soumis a 2 contraintes lineaires.
// Solution unique attendue : X=8, Y=4.
// Un record positionnel declare au niveau de la cellule (requis par NewTheorem<T>).
public record PointRecord(int X, int Y) { }
// =====================================================================
// BLOC DSL (Z3.Linq) : la reconstruction d'un record via primary ctor
// =====================================================================
{
using var thCtx = new Z3Context();
var pt = thCtx.NewTheorem<PointRecord>()
.Where(p => p.X + p.Y == 12)
.Where(p => p.X == 2 * p.Y)
.Solve();
Console.WriteLine($"[DSL] NewTheorem<PointRecord>(X+Y=12, X=2Y) : {(pt == null ? "UNSAT" : $"SAT -> {pt} (X={pt.X}, Y={pt.Y})")}");
// Variante discriminante : reorder les Where -> la solution NE change PAS
// (le matching des params se fait par nom via l'environnement, pas par l'ordre des Where)
var pt2 = thCtx.NewTheorem<PointRecord>()
.Where(p => p.X == 2 * p.Y)
.Where(p => p.X + p.Y == 12)
.Solve();
Console.WriteLine($"[DSL] (memo) Where inverse : {(pt2 == null ? "UNSAT" : $"SAT -> {pt2} (meme X, Y)")}");
// Variante UNSAT : X >= 0 et X < 0 -> le binding doit rendre null, pas throw
var unsat = thCtx.NewTheorem<PointRecord>()
.Where(p => p.X >= 0)
.Where(p => p.X < 0)
.Solve();
Console.WriteLine($"[DSL] cas UNSAT (X>=0 et X<0) : {(unsat == null ? "null (UNSAT, pas d'exception)" : "??")}");
}
// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : meme probleme, reconstruction manuelle
// =====================================================================
{
using var z3 = new Microsoft.Z3.Context();
var x = z3.MkIntConst("X");
var y = z3.MkIntConst("Y");
var solver = z3.MkSolver();
solver.Assert(z3.MkEq(z3.MkAdd(x, y), z3.MkInt(12)));
solver.Assert(z3.MkEq(x, z3.MkMul(z3.MkInt(2), y)));
Status st = solver.Check();
Console.WriteLine($"[RAW] X+Y=12, X=2Y : {st}");
if (st == Status.SATISFIABLE)
{
var m = solver.Model;
// Reconstruction manuelle : 2 Eval + parse IntNum + construction (x, y)
var xv = ((IntNum)m.Eval(x, true)).Int;
var yv = ((IntNum)m.Eval(y, true)).Int;
Console.WriteLine($"[RAW] temoin : (X={xv}, Y={yv}) (construction manuelle a partir du Model)");
}
// Cas UNSAT symetrique
var sUn = z3.MkSolver();
sUn.Assert(z3.MkGe(x, z3.MkInt(0)));
sUn.Assert(z3.MkLt(x, z3.MkInt(0)));
Console.WriteLine($"[RAW] X>=0 et X<0 : {sUn.Check()} (aucune affectation)");
}[DSL] NewTheorem<PointRecord>(X+Y=12, X=2Y) : SAT -> PointRecord { X = 8, Y = 4 } (X=8, Y=4)
[DSL] (memo) Where inverse : SAT -> PointRecord { X = 8, Y = 4 } (meme X, Y)
[DSL] cas UNSAT (X>=0 et X<0) : null (UNSAT, pas d'exception)
[RAW] X+Y=12, X=2Y : SATISFIABLE
[RAW] temoin : (X=8, Y=4) (construction manuelle a partir du Model)
[RAW] X>=0 et X<0 : UNSATISFIABLE (aucune affectation)Les deux ecritures resolvent le même système (X + Y = 12, X = 2·Y) et produisent le même temoin (X = 8, Y = 4), mais leur cout d’ecriture est asymetrique :
| Aspect | Stack B (raw Microsoft.Z3) | Stack A (DSL Z3.Linq) |
|---|---|---|
| Variables | MkIntConst("X"), MkIntConst("Y") declaratives une a une |
implicites via les proprietes X/Y du type Point |
| Contraintes | MkEq(MkAdd(x, y), MkInt(12)), MkEq(x, MkMul(MkInt(2), y)) |
p => p.X + p.Y == 12, p => p.X == 2*p.Y en LINQ naturel |
| Verification | MkSolver().Assert(...).Check() + cast IntNum/parse dans le Model |
.Solve() typé C# |
| Reconstruction | model.Eval(x, true).ToString() + cast manuel + reconstruction (x, y) a la main |
un simple Point { X = 8, Y = 4 } – le binding a fait le reste |
| Surface code | plusieurs lignes significatives + risque d’erreur de typage des IntNum |
quelques lignes de contraintes |
| Constructeur sans paramètre | non requis (le raw n’instancie jamais d’objet C#) | necessaire dans le cas d’une class mutable, interdit dans le cas d’un record (l’ancienne branche Activator.CreateInstance(t) throw) |
Ligne de contraste : la valeur ajoutee du DSL ici n’est pas une fecondation d’expression (comme
Sumqui replie N termes en un seulMkAdd), mais le routage de reconstruction – la detection du type d’environnement (classmutable avec setter vsrecordpositionnel vs type anonyme) et l’invocation de la bonne branche deTheorem.cs:993-1099. Cote raw, c’est au chercheur de coder la reconstruction – cote DSL, elle est incluse par defaut dansNewTheorem<T>(). Les tests unitairesRecordEnvTheoryTests(4 cas) verifient que la branche positionnelle couvre records a 2-3 params, scalaires mixtes (int + bool), et le retournullsur UNSAT.
Reproduisez la demarche ci-dessus avec un record a trois paramètres – par exemple record Triple(int A, int B, int C) – et trois contraintes scalaires (par exemple A == 1, B == 2, C == 3). Le solveur doit rendre un Triple { A = 1, B = 2, C = 3 }.
Variante discriminante : declarez les contraintes dans un ordre différent (par exemple B == 2, C == 3, A == 1). La solution reste-t-elle la même ? Le matching des arguments du constructeur se fait-il par nom ou par position dans le .Where ?
Indice : voir Theorem.cs:1076 – la reconstruction selectionne le constructeur dont tous les paramètres sont dans l’environnement, puis passe les args positionnellement.
// Exercice 4 : record positionnel a 3 parametres avec Z3.Linq
// TODO etudiant : modelisez un record Triple(int A, int B, int C) puis :
// Etape 1 : declarez record Triple(int A, int B, int C) au niveau de la cellule
// Etape 2 : 3 contraintes scalaires : A == 1, B == 2, C == 3
// Etape 3 : lancez .Solve() et verifiez que vous obtenez Triple { A=1, B=2, C=3 }
// Etape 4 (variante discriminante) : changez l'ordre des contraintes en B==2, C==3, A==1
// et verifiez que la solution reste la meme (le matching des params se fait par NOM, pas par ordre du Where)
// Indice : la reconstruction du record (Theorem.cs:1076) selectionne le constructeur
// dont TOUS les parametres sont satisfiables par l'environnement ; le passage des args
// est positionnel. L'ordre de declaration des Where ne change donc pas la solution,
// seul l'ordre des parametres du constructeur compte.
Console.WriteLine("Exercice a completer : record Triple positionnel a 3 parametres avec Z3.Linq");Exercice a completer : record Triple positionnel a 3 parametres avec Z3.LinqCe notebook a illustré l’utilisation de Z3.Linq pour résoudre des problèmes de satisfaction de contraintes en combinant la puissance du solveur SMT Z3 avec la syntaxe LINQ de C#.
| Approche | Cas simple (3M, 3C) | Cas complexe (30M, 30C) | Avantages | Limitations |
|---|---|---|---|---|
| Solve() | Rapide | Rapide | Trouve une solution | Pas forcément optimale |
| Optimize() | Très rapide | Plus lent | Solution optimale | Coût de calcul plus élevé |
Optimize() permet de minimiser/maximiser des objectifsNote pratique: Pour des problèmes de grande taille, il est recommandé de fournir une borne supérieure réaliste pour
Lengthafin d’éviter l’explosion combinatoire.
Modélisez et résolvez un problème de planification avec Z3.Linq.
Créez un solveur pour planifier des tâches sur plusieurs machines.
Solve() et Optimize() pour ce problème ?// TODO: Définissez le problème de planification
// - 5 tâches avec des durées différentes
// - 3 machines avec des capacités différentes
// - Contrainte : chaque tâche sur une seule machine
// - Contrainte : capacité machine non dépassée
// - Objectif : minimiser le temps total de complétion
public class PlanningProblem
{
// TODO: Propriétés du problème
// public int[] TaskDurations { get; set; }
// public int[] MachineCapacities { get; set; }
// public int[,] Assignment { get; set; } // tâche -> machine
}
// TODO: Créez le théorème LINQ pour le problème
// var theorem = from t in ctx.NewTheorem<PlanningProblem>()
// where ... // Vos contraintes
// select t;
// TODO: Résolvez et affichez la solution
// var solution = theorem.Optimize(...);
Console.WriteLine("Exercice a completer : modeliser un probleme de planification avec Z3.Linq");Exercice a completer : modeliser un probleme de planification avec Z3.Linq