Z3-Python 06 – Optimisation avancee (twin C#)

Navigation : Index | Index SMT | Index SymbolicAI | << Z3-Python-05 Quantifiers

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Hierarchiser des contraintes souples avec des poids et des priorites dans un Optimize 2. Gerer plusieurs objectifs simultanes (maximiser un revenu tout en minimisant un cout) 3. Enumerer le front de Pareto pour explorer les compromis entre objectifs contradictoires 4. Modeliser des contraintes souples (soft constraints) au moyen de variables de relaxation booleennes (MaxSAT) 5. Appliquer ces techniques a un cas pratique d’allocation de budget multi-projets

Prerequis

Z3-Python-01-Csharp (Introduction) : Solver, Int, Bool, Real, Optimize de base
Z3-Python-03-Csharp (Tactiques) : familiarite avec Bool, Or, And, MkITE
Notions d’optimisation combinatoire (maximisation sous contraintes)

Duree estimee : ~40 min

Ce notebook est le twin C# du notebook Python Z3-06-Advanced-Optimization-Python.ipynb. Il poursuit l’exploration de la classe Optimize au-dela du cas elementaire (un seul objectif vu en NB01). Les problemes reels comportent presque toujours plusieurs objectifs contradictoires : maximiser la qualite tout en minimisant le cout, ou satisfaire un maximum de préférences quand toutes ne peuvent l’etre simultanement. Z3 fournit pour cela les contraintes ponderees, l’optimisation multi-objectif lexicographique, et l’enumeration du front de Pareto.

Kernel : .net-csharp (.NET Interactive). Le moteur est le vrai Microsoft.Z3 via NuGet #r "nuget: Microsoft.Z3" (v4.12.2.0) – le même solveur C++ que z3-solver Python.

#r "nuget: Microsoft.Z3"
#load "Z3NativeLoader.cs"
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;

// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Context).Assembly);

// Contexte Z3 partage par toutes les cellules (meme moteur C++ que z3-solver Python)
var ctx = new Context();
Console.WriteLine($"Moteur : Microsoft.Z3 {Microsoft.Z3.Version.FullVersion}");
Console.WriteLine("Optimisation multi-criteres : MkOptimize, MkMaximize, MkMinimize, AssertSoft.");

Installed Packages

Microsoft.Z3, 4.12.2

Moteur : Microsoft.Z3 Z3 4.12.2.0
Optimisation multi-criteres : MkOptimize, MkMaximize, MkMinimize, AssertSoft.

1. Rappel et motivation – au-dela d’un seul objectif

Le notebook 01 a introduit Optimize avec un objectif unique : maximiser la valeur d’un sac a dos, ou minimiser le temps de fin d’un ordonnancement. Le patron etait simple :

var opt = ctx.MkOptimize();
opt.Assert(contraintes_dures);
opt.MkMaximize(objectif);   // un seul objectif
opt.Check();

La realite est multi-objectif

Dans la vraie vie, les problemes comportent plusieurs objectifs contradictoires :

Domaine	Objectif A (maximiser)	Objectif B (minimiser)
Logistique	Qualite de service	Cout de transport
Finance	Rendement	Risque
Planification	Satisfaction des préférences	Cout horaire
Ingenierie	Performance	Consommation energetique

On ne peut pas « maximiser A et minimiser B » simultanement de facon absolue : il faut choisir une stratégie de compromis. Z3 offre trois approches complementaires :

Priorites hiérarchiques (section 2) : chaque contrainte souple a un poids, on minimise la somme ponderee des violations.
Objectifs multiples lexicographiques (section 3) : on optimise les objectifs les uns après les autres, par ordre de priorite.
Front de Pareto (section 4) : on enumere tous les compromis optimaux pour laisser un humain decider.

Le vocabulaire utile pour la suite :

Terme	Definition
Contrainte dure (hard constraint)	Doit etre satisfaite ; si impossible, le problème est `UNSATISFIABLE`.
Contrainte souple (soft constraint)	Devrait etre satisfaite, mais une violation est toleree moyennant une penalite.
Poids (weight)	Cout numérique attribue a la violation d’une contrainte souple. Plus le poids est eleve, plus Z3 tente de la satisfaire.
Solution dominee	Il existe une autre solution strictement meilleure sur au moins un objectif, sans etre pire sur aucun autre.
Front de Pareto	Ensemble des solutions non-dominees : les compromis optimaux.

2. Objectifs hiérarchiques avec `Optimize` et priorites

La technique la plus directe pour gerer des contraintes de priorite variable consiste a introduire des variables de relaxation booleennes. Pour chaque contrainte souple c_i, on créé une variable r_i (un BoolExpr) et on ajoute MkOr(c_i, r_i) : la contrainte peut etre violee, mais seulement si r_i vaut True. On minimise ensuite la somme ponderee des r_i.

Principe

Soit un ensemble de contraintes souples $c_1, c_2, \ldots, c_k$ avec des poids $w_1, w_2, \ldots, w_k$. Pour chaque $c_i$ :

\[\text{ajouter la contrainte relachee : } c_i \lor r_i\]

puis minimiser le cout total des violations :

\[\text{minimiser } \sum_{i=1}^{k} w_i \cdot \mathbb{1}[r_i = \text{True}]\]

En C#/.NET, ctx.MkITE(r_i, ctx.MkInt(weight_i), ctx.MkInt(0)) construit exactement l’indicateur $w_i \cdot \mathbb{1}[r_i]$.

Exemple : ordonnanceur avec contraintes dures et souples

Trois tâches doivent etre planifiees dans des fenêtres temporelles. Certaines contraintes sont imperatives (dures), d’autres sont souhaitees (souples) avec des poids différents : une priorite elevee signifie que Z3 fera de son mieux pour la satisfaire.

// Ordonnanceur hierarchique : contraintes dures + contraintes souples ponderees.
// Trois taches T0, T1, T2. Chaque tache i demarre a debut_i (entier >= 0),
// dure 1 unite de temps, et deux taches ne peuvent s'executer au meme instant.
var opt = ctx.MkOptimize();

// Variables de decision : creneau de debut de chaque tache (0 a 9)
var debut = new IntExpr[3];
for (int i = 0; i < 3; i++) {
    debut[i] = ctx.MkIntConst($"debut_{i}");
    opt.Assert(ctx.MkGe(debut[i], ctx.MkInt(0)), ctx.MkLe(debut[i], ctx.MkInt(9)));
}

// --- Contraintes DURES (hard) ---
// Les trois taches doivent occuper des creneaux distincts.
opt.Assert(ctx.MkDistinct(debut));
// T0 doit absolument commencer apres le creneau 2 (contrainte externe)
opt.Assert(ctx.MkGe(debut[0], ctx.MkInt(2)));

// --- Contraintes SOUPLES (soft) avec poids ---
// (description, contrainte, poids)
var preferences = new (string, BoolExpr, int)[] {
    ("T0 le plus tot possible (debut_0 == 2)", ctx.MkEq(debut[0], ctx.MkInt(2)), 10),
    ("T1 avant T0 (debut_1 < debut_0)",         ctx.MkLt(debut[1], debut[0]),     7),
    ("T2 en dernier (debut_2 > debut_0)",        ctx.MkGt(debut[2], debut[0]),     5),
    ("T1 au creneau 0 (debut_1 == 0)",           ctx.MkEq(debut[1], ctx.MkInt(0)), 3),
};

var relaxVars = new List<(string desc, BoolExpr r, int poids)>();
var coutTotal = (ArithExpr)ctx.MkInt(0);
for (int idx = 0; idx < preferences.Length; idx++) {
    var (desc, contrainte, poids) = preferences[idx];
    var r = ctx.MkBoolConst($"r_{idx}");
    relaxVars.Add((desc, r, poids));
    // Contrainte relachee : c_i OU r_i
    opt.Assert(ctx.MkOr(contrainte, r));
    coutTotal = ctx.MkAdd(coutTotal, (ArithExpr)ctx.MkITE(r, ctx.MkInt(poids), ctx.MkInt(0)));
}
var coutVar = ctx.MkIntConst("cout_total");
opt.Assert(ctx.MkEq(coutVar, coutTotal));
opt.MkMinimize(coutVar);

Console.WriteLine($"Ordonnancement hierarchique : {opt.Check()}");
if (opt.Check() == Status.SATISFIABLE) {
    var m = opt.Model;
    Console.WriteLine("\nPlanning obtenu :");
    for (int i = 0; i < 3; i++)
        Console.WriteLine($"  T{i} : creneau {((IntNum)m.Evaluate(debut[i])).Int64}");
    Console.WriteLine("\nContraintes souples :");
    long coutCumul = 0;
    foreach (var (desc, r, poids) in relaxVars) {
        bool violee = ((BoolExpr)m.Evaluate(r)).BoolValue == Z3_lbool.Z3_L_TRUE;
        long penalite = violee ? poids : 0;
        coutCumul += penalite;
        string statut = violee ? "VIOLEE" : "satisfaite";
        Console.WriteLine($"  [{statut,9}] (poids {poids,2}) {desc}");
    }
    Console.WriteLine($"\nCout total des violations : {((IntNum)m.Evaluate(coutVar)).Int64}");
}

Ordonnancement hierarchique : SATISFIABLE

Planning obtenu :
  T0 : creneau 2
  T1 : creneau 0
  T2 : creneau 9

Contraintes souples :
  [satisfaite] (poids 10) T0 le plus tot possible (debut_0 == 2)
  [satisfaite] (poids  7) T1 avant T0 (debut_1 < debut_0)
  [satisfaite] (poids  5) T2 en dernier (debut_2 > debut_0)
  [satisfaite] (poids  3) T1 au creneau 0 (debut_1 == 0)

Cout total des violations : 0

Interpretation : hiérarchie ponderee

Sortie obtenue : Z3 trouve un planning qui satisfait toutes les contraintes dures et minimise la somme ponderee des violations des contraintes souples (cout total nul ici, car toutes les préférences sont compatibles).

Mécanisme	API Microsoft.Z3	Rôle
Variable de relaxation	`ctx.MkBoolConst($"r_{i}")`	Vaut `True` si la contrainte souple est violee
Contrainte relachee	`ctx.MkOr(contrainte, r_i)`	Permet la violation via `r_i`
Penalite	`ctx.MkITE(r_i, ctx.MkInt(poids), ctx.MkInt(0))`	Contribution au cout total si violation
Objectif	`opt.MkMinimize(cout_total)`	Minimiser la somme des penalites

Points cles : 1. Les contraintes a poids eleve sont prioritaires : Z3 prefere violer plusieurs contraintes a faible poids qu’une seule a poids eleve. 2. Toutes les contraintes dures sont satisfaites par construction (elles sont ajoutees avec opt.Assert sans relaxation). 3. Le cout total obtenu est le minimum : aucune autre assignation ne donne une somme ponderee de violations inferieure.

Note technique (.NET) : Microsoft.Z3 expose aussi opt.AssertSoft(BoolExpr, uint weight, string group) qui automatise le schema relaxation+penalite pour un groupe de contraintes. On l’illustre en section 5. Le codage manuel ci-dessus reste utile pour comprendre le mécanisme et contrôler finement l’expression du cout. Le choix des poids est decisive : en pratique, on utilise souvent une echelle exponentielle (1, 2, 4, 8…) pour garantir une veritable hiérarchie lexicographique approximative.

3. Objectifs multiples – `MkMaximize` vs `MkMinimize` simultanes

Un Optimize peut contenir plusieurs objectifs declares via opt.MkMaximize(...) et opt.MkMinimize(...). Z3 resout ces objectifs de maniere lexicographique (par ordre de declaration) : le premier objectif est optimise en priorite, puis le second est optimise sous la contrainte que le premier reste optimal.

Lecture des bornes

Chaque appel a opt.MkMaximize(expr) ou opt.MkMinimize(expr) renvoie un handle de type Optimize.Handle. Après opt.Check(), on peut interroger :

handle.Upper : borne superieure de l’objectif (utile après MkMaximize).
handle.Lower : borne inferieure de l’objectif (utile après MkMinimize).

Ces proprietes retournent un Expr (en pratique un IntNum pour les objectifs entiers) : on caste en IntNum puis .Int64 pour la valeur.

Exemple : maximiser le revenu, puis minimiser le cout

Une entreprise choisit combien d’unites produire (q, entier). Chaque unite generee un revenu de 8 EUR mais coute 3 EUR en production. La capacite est limitee a 15 unites. On veut maximiser le revenu (priorite 1), puis minimiser le cout (priorite 2).

// Optimisation multi-objectif lexicographique.
// Objectif 1 (priorite haute) : maximiser le revenu = 8 * q
// Objectif 2 (priorite basse) : minimiser le cout = 3 * q
var optLex = ctx.MkOptimize();
var q = ctx.MkIntConst("q");
optLex.Assert(ctx.MkGe(q, ctx.MkInt(0)), ctx.MkLe(q, ctx.MkInt(15)));

var revenu = ctx.MkMul(ctx.MkInt(8), q);
var cout = ctx.MkMul(ctx.MkInt(3), q);

// Declaration dans l'ordre de priorite (lexicographique)
var hRevenu = optLex.MkMaximize(revenu);  // priorite 1 : maximiser le revenu
var hCout = optLex.MkMinimize(cout);      // priorite 2 : minimiser le cout

Console.WriteLine($"Multi-objectif lexicographique : {optLex.Check()}");
if (optLex.Check() == Status.SATISFIABLE) {
    var m = optLex.Model;
    long qVal = ((IntNum)m.Evaluate(q)).Int64;
    Console.WriteLine($"\nSolution : q = {qVal} unites");
    Console.WriteLine($"  Revenu = 8 x {qVal} = {8 * qVal} EUR (maximise en priorite)");
    Console.WriteLine($"  Cout   = 3 x {qVal} = {3 * qVal} EUR (minimise ensuite)");
    Console.WriteLine($"  Profit net = {8 * qVal - 3 * qVal} EUR");
    Console.WriteLine($"\nBornes : revenu <= {((IntNum)hRevenu.Upper).Int64}, cout >= {((IntNum)hCout.Lower).Int64}");
}

// Comparaison : maximisation du profit net (5 * q)
var opt2 = ctx.MkOptimize();
var q2 = ctx.MkIntConst("q2");
opt2.Assert(ctx.MkGe(q2, ctx.MkInt(0)), ctx.MkLe(q2, ctx.MkInt(15)));
var profit = ctx.MkSub(ctx.MkMul(ctx.MkInt(8), q2), ctx.MkMul(ctx.MkInt(3), q2));
opt2.MkMaximize(profit);
Console.WriteLine("\n--- Comparaison : maximisation du profit net (5 * q) ---");
Console.WriteLine($"Resultat : {opt2.Check()}");
if (opt2.Check() == Status.SATISFIABLE) {
    var m2 = opt2.Model;
    long q2Val = ((IntNum)m2.Evaluate(q2)).Int64;
    Console.WriteLine($"  q = {q2Val}, profit = {5 * q2Val} EUR");
    Console.WriteLine("\nDans cet exemple les deux approches convergent (profit croissant en q),");
    Console.WriteLine("mais en general lexicographique != somme ponderee.");
}

Multi-objectif lexicographique : SATISFIABLE

Solution : q = 15 unites
  Revenu = 8 x 15 = 120 EUR (maximise en priorite)
  Cout   = 3 x 15 = 45 EUR (minimise ensuite)
  Profit net = 75 EUR

Bornes : revenu <= 120, cout >= 45

--- Comparaison : maximisation du profit net (5 * q) ---
Resultat : SATISFIABLE
  q = 15, profit = 75 EUR

Dans cet exemple les deux approches convergent (profit croissant en q),
mais en general lexicographique != somme ponderee.

Quand lexicographique differe vraiment de la somme ponderee

L’exemple precedent convergeait : maximiser le revenu puis minimiser le cout donnait le meme resultat qu’un seul objectif (profit net), parce que les deux objectifs etaient monotones dans la meme variable q. La machinerie lexicographique de Z3 (MkMaximize puis MkMinimize, par ordre de declaration) n’etait donc pas visible dans la sortie.

Voici un cas ou les deux strategies divergent : un catalogue de deux produits partageant une capacite de production, dont l’un est un loss-leader (fort revenu brut, mais vendu a perte).

Produit premium : revenu 8 EUR/unite, cout 10 EUR/unite (perte de 2 EUR/unite).
Produit standard : revenu 3 EUR/unite, cout 1 EUR/unite (profit de 2 EUR/unite).

Un objectif de chiffre d’affaires brut pousse vers le premium ; un objectif de profit net pousse vers le standard. Le compromis est ici reel, et le choix strategique (priorite au CA vs priorite au profit) change la solution optimale – c’est exactement ce que l’optimisation lexicographique permet de formaliser, et que la somme ponderee, elle, melange.

// Loss-leader : lexicographique (CA brut d'abord) vs somme ponderee (profit net).
// Deux produits partagent une capacite de 15 unites (ll_q1 + ll_q2 <= 15).
//   - premium (ll_q1) : revenu 8/u, cout 10/u   -> perte de 2/u
//   - standard (ll_q2): revenu 3/u, cout 1/u    -> profit de 2/u
const int CAPACITE = 15;

// --- Strategie 1 : LEXICOGRAPHIQUE (max revenu, puis min cout) ---
var ll_opt1 = ctx.MkOptimize();
var ll_q1 = ctx.MkIntConst("q1");
var ll_q2 = ctx.MkIntConst("q2");
ll_opt1.Assert(ctx.MkGe(ll_q1, ctx.MkInt(0)), ctx.MkGe(ll_q2, ctx.MkInt(0)));
ll_opt1.Assert(ctx.MkLe(ctx.MkAdd(ll_q1, ll_q2), ctx.MkInt(CAPACITE)));
var ll_revenu = ctx.MkAdd(ctx.MkMul(ctx.MkInt(8), ll_q1), ctx.MkMul(ctx.MkInt(3), ll_q2));
var ll_cout = ctx.MkAdd(ctx.MkMul(ctx.MkInt(10), ll_q1), ctx.MkMul(ctx.MkInt(1), ll_q2));
ll_opt1.MkMaximize(ll_revenu);   // priorite 1 : chiffre d'affaires brut
ll_opt1.MkMinimize(ll_cout);     // priorite 2 : cout (secondaire)
if (ll_opt1.Check() == Status.SATISFIABLE) {
    var ll_m1 = ll_opt1.Model;
    long ll_a1 = ((IntNum)ll_m1.Evaluate(ll_q1)).Int64;
    long ll_b1 = ((IntNum)ll_m1.Evaluate(ll_q2)).Int64;
    long ll_r1 = 8*ll_a1 + 3*ll_b1, ll_c1 = 10*ll_a1 + 1*ll_b1;
    Console.WriteLine("Lexicographique (CA brut prioritaire) :");
    Console.WriteLine($"  premium={ll_a1}, standard={ll_b1} -> CA={ll_r1}, cout={ll_c1}, profit={ll_r1 - ll_c1}");
}

// --- Strategie 2 : SOMME PONDEREE (max profit net = revenu - cout) ---
var ll_opt2 = ctx.MkOptimize();
var ll_p1 = ctx.MkIntConst("p1");
var ll_p2 = ctx.MkIntConst("p2");
ll_opt2.Assert(ctx.MkGe(ll_p1, ctx.MkInt(0)), ctx.MkGe(ll_p2, ctx.MkInt(0)));
ll_opt2.Assert(ctx.MkLe(ctx.MkAdd(ll_p1, ll_p2), ctx.MkInt(CAPACITE)));
var ll_profit = ctx.MkSub(ctx.MkAdd(ctx.MkMul(ctx.MkInt(8), ll_p1), ctx.MkMul(ctx.MkInt(3), ll_p2)),
                          ctx.MkAdd(ctx.MkMul(ctx.MkInt(10), ll_p1), ctx.MkMul(ctx.MkInt(1), ll_p2)));
ll_opt2.MkMaximize(ll_profit);
if (ll_opt2.Check() == Status.SATISFIABLE) {
    var ll_m2 = ll_opt2.Model;
    long ll_a2 = ((IntNum)ll_m2.Evaluate(ll_p1)).Int64;
    long ll_b2 = ((IntNum)ll_m2.Evaluate(ll_p2)).Int64;
    long ll_r2 = 8*ll_a2 + 3*ll_b2, ll_c2 = 10*ll_a2 + 1*ll_b2;
    Console.WriteLine("Somme ponderee (profit net prioritaire) :");
    Console.WriteLine($"  premium={ll_a2}, standard={ll_b2} -> CA={ll_r2}, cout={ll_c2}, profit={ll_r2 - ll_c2}");
}

Lexicographique (CA brut prioritaire) :
  premium=15, standard=0 -> CA=120, cout=150, profit=-30
Somme ponderee (profit net prioritaire) :
  premium=0, standard=15 -> CA=45, cout=15, profit=30

Interpretation : lexicographique vs pondere

Sortie obtenue : Z3 trouve q = 15 (capacite maximale), ce qui maximise le revenu. Le cout est ensuite minimise, mais comme cout = 3 * q et que q est déjà fixe par la maximisation du revenu, le cout ne peut pas etre reduit independamment.

Stratégie	Comment ca marche	Quand l’utiliser
Lexicographique	Optimise les objectifs dans l’ordre de declaration	Priorites claires et strictes (A domine B)
Ponderee (section 2)	Minimise la somme ponderee des violations	Compromis souhaites entre objectifs
Pareto (section 4)	Enumere tous les compromis optimaux	Pas de priorite naturelle, decision humaine

Points cles : 1. handle.Upper donne la valeur optimale d’un objectif MkMaximize ; handle.Lower pour MkMinimize (caster le Expr retourne en IntNum). 2. L’ordre de declaration des MkMaximize/MkMinimize définit la priorite lexicographique. 3. L’approche lexicographique n’est pas equivalente a maximiser une somme ponderee : elle impose une hiérarchie stricte.

Note technique : L’optimisation multi-objectif lexicographique de Z3 suit le schema Box/Wilson : optimiser l’objectif 1, fixer sa valeur optimale comme contrainte, puis optimiser l’objectif 2, et ainsi de suite.

4. Front de Pareto – explorer les compromis

Quand deux objectifs sont contradictoires et qu’aucune priorite naturelle n’existe, la notion de front de Pareto est pertinente. Une solution est dite Pareto-optimale si aucune autre solution ne l’ameliore sur un objectif sans la degrader sur l’autre. Le front de Pareto est l’ensemble de toutes ces solutions optimales.

Méthode d’enumeration

Pour construire le front de Pareto entre maximiser $A$ et minimiser $B$ :

Maximiser $A$ et enregistrer $(A^*, B^*)$.
Ajouter la contrainte $B < B^*$ (imposer un cout strictement inferieur).
Re-maximiser $A$ sous cette nouvelle contrainte.
Repeter jusqu’a UNSATISFIABLE.

On obtient ainsi une suite de points $(A_1, B_1), (A_2, B_2), \ldots$ ou le cout decroit et la qualite s’ajuste.

Exemple : qualite vs cout

On choisit un niveau de qualite q (0 a 10) et un niveau de cout c. Les deux sont lies : une qualite elevee implique un cout minimal, mais le cout peut aussi augmenter pour d’autres raisons. On cherche tous les compromis optimaux (qualite maximale, cout minimal).

// Enumeration du front de Pareto : maximiser qualite (0-10), minimiser cout.
// Relation : une qualite q exige un cout minimal de q * 2.
List<(long qualite, long cout)> EnumererFrontPareto(Context ctx, int maxIter = 15) {
    var frontBrut = new List<(long, long)>();
    for (int iteration = 0; iteration < maxIter; iteration++) {
        var optL = ctx.MkOptimize();
        var qualite = ctx.MkIntConst("qualite");
        var cout = ctx.MkIntConst("cout");
        // Domaine : petits entiers pour garantir un calcul rapide
        optL.Assert(ctx.MkGe(qualite, ctx.MkInt(0)), ctx.MkLe(qualite, ctx.MkInt(10)));
        optL.Assert(ctx.MkGe(cout, ctx.MkInt(0)), ctx.MkLe(cout, ctx.MkInt(20)));
        // Relation qualite-cout : une qualite q exige un cout minimal de q * 2
        optL.Assert(ctx.MkGe(cout, ctx.MkMul(ctx.MkInt(2), qualite)));
        // Exclusion : forcer un cout strictement plus bas que le precedent
        foreach (var (_, cPrec) in frontBrut)
            optL.Assert(ctx.MkLt(cout, ctx.MkInt(cPrec)));
        // Objectif : maximiser la qualite
        optL.MkMaximize(qualite);
        if (optL.Check() != Status.SATISFIABLE) break;  // plus de solution : front complet
        var m = optL.Model;
        long qVal = ((IntNum)m.Evaluate(qualite)).Int64;
        long cVal = ((IntNum)m.Evaluate(cout)).Int64;
        frontBrut.Add((qVal, cVal));
    }
    // Dedoublonner : ne garder qu'un point par niveau de qualite
    var front = new List<(long, long)>();
    var vues = new HashSet<long>();
    foreach (var (q, c) in frontBrut) {
        if (vues.Add(q)) front.Add((q, c));
    }
    return front;
}

var front = EnumererFrontPareto(ctx);
Console.WriteLine("Front de Pareto (qualite max, cout min) :");
Console.WriteLine($"{"Point",6} | {"Qualite",7} | {"Cout",5} | {"Cout min = 2*q",15}");
Console.WriteLine(new string('-', 45));
for (int i = 0; i < front.Count; i++) {
    var (q, c) = front[i];
    long coutMin = q * 2;
    string marque = c == coutMin ? " <-- cout min" : "";
    Console.WriteLine($"{i + 1,6} | {q,7} | {c,5} | {coutMin,15}{marque}");
}
Console.WriteLine($"\n{front.Count} points Pareto-optimaux trouves (qualites distinctes).");
Console.WriteLine("Chaque point est un compromis : pour baisser le cout, il faut");
Console.WriteLine("sacrifier de la qualite (puisque cout_min = 2 * qualite).");

Front de Pareto (qualite max, cout min) :
 Point | Qualite |  Cout |  Cout min = 2*q
---------------------------------------------
     1 |      10 |    20 |              20 <-- cout min
     2 |       9 |    19 |              18
     3 |       8 |    17 |              16
     4 |       7 |    14 |              14 <-- cout min
     5 |       6 |    12 |              12 <-- cout min
     6 |       5 |    10 |              10 <-- cout min
     7 |       4 |     9 |               8
     8 |       3 |     7 |               6
     9 |       2 |     5 |               4
    10 |       1 |     2 |               2 <-- cout min

10 points Pareto-optimaux trouves (qualites distinctes).
Chaque point est un compromis : pour baisser le cout, il faut
sacrifier de la qualite (puisque cout_min = 2 * qualite).

Visualiser le front de Pareto

Un tableau de nombres ne rend pas justice au concept de compromis. En projetant chaque point Pareto-optimal dans le plan (qualite, cout), le front devient une courbe descendante : chaque pas vers un cout plus bas coute de la qualite. La droite cout_min = 2 * qualite (la frontiere de faisabilite imposee par le modèle) apparait en pointille : on voit immediatement que certains points Pareto-optimaux sont strictement au-dessus de cette borne minimale – Z3 les a choisis parce qu’a qualite fixee, plusieurs couts sont Pareto-equivalents, et le solveur en echantillonne un. C’est précisément ce que le front de Pareto revele qu’un simple « minimiser le cout » cacherait.

Le twin Python trace cette courbe avec matplotlib (rendu PNG). Le twin C# utilise SVG inline (rendu statique zero-dépendance via le helper SvgChartHelper, visible sur GitHub/nbviewer/offline) – les deux twins offrent maintenant une vraie courbe, pas un tableau de nombres.

// Visualisation SVG inline du front de Pareto : qualite (x) vs cout (y).
// Prong-A (#3801, #6927) : rendu SVG statique zero-dependance (rend sur GitHub/nbviewer/offline).
// Remplace le chart Plotly-CDN (#6856) dont le script externe rendait BLANC en consultation statique.
// Helper canon SvgChartHelper.cs (#6942 MERGED) ; primitive Overlay multi-series (#6958 MERGED).
#load "../../../Probas/Infer/SvgChartHelper.cs"

// Donnees : front (points Pareto-optimaux) + droite cout_min = 2*qualite (frontiere de faisabilite).
// 2 series sur axe X numerique partage (qualite) -> SvgChartHelper.Overlay (pattern canon #6927).
var series = new SvgSeries[]
{
    new SvgSeries("Front de Pareto",
        front.Select(p => (double)p.qualite).ToArray(),
        front.Select(p => (double)p.cout).ToArray(),
        TraceStyle.LineMarkers, "#1f77b4"),
    new SvgSeries("cout_min = 2*qualite",
        Enumerable.Range(0, 11).Select(q => (double)q).ToArray(),
        Enumerable.Range(0, 11).Select(q => (double)(2 * q)).ToArray(),
        TraceStyle.Line, "#d62728"),
};
display(SvgChartHelper.Overlay("Front de Pareto : qualite vs cout", "qualite", "cout", series));

Interpretation : front de Pareto

Sortie obtenue : une liste de points (qualite, cout) tries par cout decroissant. Chaque point est Pareto-optimal : on ne peut pas ameliorer un objectif sans degrader l’autre.

Étape	Action	Résultat
1	`opt.MkMaximize(qualite)` sans contrainte de cout	Point avec qualite maximale
2	Ajouter `cout < cout_precedent`, re-maximiser	Point avec cout plus bas
3	Repeter jusqu’a `UNSATISFIABLE`	Front complet

Points cles : 1. Le front de Pareto contient les compromis optimaux : aucun point n’est domine par un autre. 2. Le nombre de points est fini (domains entiers petits), mais peut etre grand si les ranges sont larges. 3. Cette méthode d’enumeration par exclusion successive est simple mais couteuse : a chaque itération, on ajoute une contrainte. Pour de grands fronts, on prefere des algorithmes specialises.

Note technique : On maintient les domains entiers petits (0-10 pour la qualite, 0-20 pour le cout) pour garantir que chaque appel a opt.Check() est quasi instantane. Avec de larges ranges de Real, l’enumeration du front de Pareto peut devenir prohibitive.

Exercice 1 : Construire un front de Pareto

Enonce

Ecrivez une fonction ConstruireFrontPareto qui enumere le front de Pareto pour maximiser une variable qualite (entier 0-10) et minimiser une variable cout (entier 0-20), lies par la contrainte cout >= qualite * 2.

La fonction doit retourner une liste de couples (qualite, cout) representant tous les compromis optimaux.

Indices :

# Indice : a chaque itération, créez un nouvel Optimize, maximisez qualite, puis ajoutez cout < cout_dernier_point comme contrainte pour la prochaine itération.
# Étape 1 : initialiser front = new List<(long,long)>() et boucler (for (int it = 0; it < maxIter; it++)).
# Étape 2 : dans la boucle, créer ctx.MkOptimize(), declarer qualite et cout avec leurs bornes.
# Étape 3 : ajouter cout >= qualite * 2 et, pour chaque point précédent, cout < cout_prec.
# Étape 4 : opt.MkMaximize(qualite) puis opt.Check() ; si UNSATISFIABLE, break.
# Étape 5 : extraire les valeurs et les ajouter a front.

// EXERCICE 1 : Enumerer le front de Pareto (qualite vs cout).
List<(long qualite, long cout)> ConstruireFrontPareto(Context ctx, int maxIter = 15) {
    Console.WriteLine("Exercice 1 - a completer");
    // TODO etudiant : implementez l'enumeration du front de Pareto
    // Indice : bouclez, a chaque iteration maximisez qualite, enregistrez
    //          (qualite, cout), puis ajoutez cout < cout_actuel comme contrainte.
    // Etape 1 : initialiser front = new List<(long,long)>()
    // Etape 2 : boucler (for iteration = 0; iteration < maxIter; iteration++)
    // Etape 3 : creer ctx.MkOptimize(), ajouter les bornes et cout >= qualite * 2
    // Etape 4 : ajouter cout < cout_prec pour chaque point deja trouve
    // Etape 5 : opt.MkMaximize(qualite), si UNSATISFIABLE -> break, sinon extraire et ajouter
    return null;  // TODO etudiant : remplacer par la liste des couples (qualite, cout)
}

var frontEx1 = ConstruireFrontPareto(ctx);
Console.WriteLine($"Front de Pareto : {(frontEx1 == null ? "(a completer)" : string.Join(", ", frontEx1))}");

Exercice 1 - a completer
Front de Pareto : (a completer)

5. Contraintes souples (soft constraints) et MaxSAT

Le problème MaxSAT consiste a satisfaire un maximum de contraintes souples quand toutes ne peuvent l’etre simultanement. C’est un cas particulier de l’approche ponderee de la section 2, ou toutes les contraintes ont le même poids (on compte simplement le nombre de violations).

Formalisation

Soit $k$ contraintes souples $c_1, \ldots, c_k$. Pour chacune, on introduit une variable de relaxation $r_i \in \{0, 1\}$ et on ajoute $c_i \lor r_i$. On minimise ensuite :

\[\sum_{i=1}^{k} r_i\]

La valeur optimale donne le nombre minimum de contraintes violees.

Exemple : assignation de salles avec préférences

Quatre etudiants doivent etre assignes a quatre salles (une chacun). Chaque etudiant a des préférences (salle preferee). Toutes les préférences ne sont pas compatibles (deux etudiants peuvent preferer la même salle). On veut satisfaire un maximum de préférences.

// MaxSAT : satisfaire un maximum de preferences d'assignation de salles.
// 4 etudiants (E0..E3), 4 salles (S0..S3). Assignation bijective.
// Preferences (potentiellement conflictuelles) :
//   E0 prefere S0, E1 prefere S0 (conflit !), E2 prefere S2, E3 prefere S1.
var optMax = ctx.MkOptimize();
int n = 4;
// Variable : salle[i] = numero de salle assignee a l'etudiant i
var salle = new IntExpr[n];
for (int i = 0; i < n; i++) {
    salle[i] = ctx.MkIntConst($"salle_{i}");
    optMax.Assert(ctx.MkGe(salle[i], ctx.MkInt(0)), ctx.MkLe(salle[i], ctx.MkInt(3)));
}
// Contrainte DURE : assignation bijective (chaque salle a exactement un etudiant)
optMax.Assert(ctx.MkDistinct(salle));

// Preferences (contraintes SOUPLES, toutes de poids 1 = MaxSAT uniforme)
var preferences = new (int etudiant, int sallePref)[] { (0, 0), (1, 0), (2, 2), (3, 1) };
var relaxVars = new List<(int etudiant, int sallePref, BoolExpr r)>();
var sommeViolations = (ArithExpr)ctx.MkInt(0);
foreach (var (etudiant, sallePref) in preferences) {
    var r = ctx.MkBoolConst($"pref_{etudiant}_{sallePref}");
    relaxVars.Add((etudiant, sallePref, r));
    // Contrainte relachee : etudiant obtient sa salle OU r est vrai
    optMax.Assert(ctx.MkOr(ctx.MkEq(salle[etudiant], ctx.MkInt(sallePref)), r));
    sommeViolations = ctx.MkAdd(sommeViolations, (ArithExpr)ctx.MkITE(r, ctx.MkInt(1), ctx.MkInt(0)));
}
// Objectif : minimiser le nombre de preferences non satisfaites
var nbViolations = ctx.MkIntConst("nb_violations");
optMax.Assert(ctx.MkEq(nbViolations, sommeViolations));
optMax.MkMinimize(nbViolations);

Console.WriteLine($"MaxSAT (assignation de salles) : {optMax.Check()}");
if (optMax.Check() == Status.SATISFIABLE) {
    var m = optMax.Model;
    Console.WriteLine("\nAssignation optimale :");
    int nbSatisfaites = 0;
    foreach (var (etudiant, sallePref, r) in relaxVars) {
        long s = ((IntNum)m.Evaluate(salle[etudiant])).Int64;
        bool violee = ((BoolExpr)m.Evaluate(r)).BoolValue == Z3_lbool.Z3_L_TRUE;
        if (!violee) nbSatisfaites++;
        string symbole = violee ? "--" : "OK";
        Console.WriteLine($"  E{etudiant} -> S{s}  (preferait S{sallePref}) [{symbole}]");
    }
    Console.WriteLine($"\nPreferences satisfaites : {nbSatisfaites} / {preferences.Length}");
    Console.WriteLine($"Violations minimales : {((IntNum)m.Evaluate(nbViolations)).Int64}");
    Console.WriteLine("\nZ3 ne pouvait pas satisfaire E0 et E1 simultanement (meme preference S0).");
    Console.WriteLine("Il a choisi d'en satisfaire un et sacrifie l'autre (1 violation minimum).");
}

// Variante .NET idiomatic : opt.AssertSoft(c, weight, group) automatise le schema.
// Exemple (commente) equivalent pour E0 -> S0 :
//   optMax.AssertSoft(ctx.MkEq(salle[0], ctx.MkInt(0)), 1u, "prefs");

MaxSAT (assignation de salles) : SATISFIABLE

Assignation optimale :
  E0 -> S0  (preferait S0) [OK]
  E1 -> S3  (preferait S0) [--]
  E2 -> S2  (preferait S2) [OK]
  E3 -> S1  (preferait S1) [OK]

Preferences satisfaites : 3 / 4
Violations minimales : 1

Z3 ne pouvait pas satisfaire E0 et E1 simultanement (meme preference S0).
Il a choisi d'en satisfaire un et sacrifie l'autre (1 violation minimum).

Interpretation : MaxSAT et variables de relaxation

Sortie obtenue : Z3 trouve une assignation qui satisfait 3 des 4 préférences. La seule violation est inevitable car E0 et E1 preferent la même salle S0.

Élément	Implementation	Rôle
Contrainte dure	`ctx.MkDistinct(salle)`	Une salle par etudiant, pas de doublon
Contrainte souple	`ctx.MkOr(salle[i] == pref, r_i)`	Préférence violable si `r_i = True`
Compteur	`ctx.MkITE(r_i, 1, 0)`	Contribution unitaire au nombre de violations
Objectif	`opt.MkMinimize(nb_violations)`	Maximiser le nombre de préférences satisfaites

Points cles : 1. Le problème MaxSAT est un cas particulier d’optimisation ponderee ou tous les poids sont egaux a 1. 2. Les variables de relaxation Bool sont l’outil central : elles « absorbent » les violations impossibles a eviter. 3. ctx.MkDistinct impose que toutes les valeurs soient distinctes (equivalent AllDifferent). 4. Si on avait donne des poids différents aux préférences, Z3 aurait privilege les préférences a poids eleve (retour a la section 2).

Note technique (.NET) : opt.AssertSoft(BoolExpr c, uint weight, string group) est la forme native du MaxSAT pondere dans Microsoft.Z3 : les contraintes d’un même group s’agregent, et Z3 minimise la somme ponderee des violations. Le codage manuel ci-dessus reste transparent ; AssertSoft est le raccourci idiomatique. MaxSAT est un domaine de recherche actif : Z3 utilise un algorithme de recherche dichotomique sur le nombre de violations pour converger rapidement vers l’optimum.

Exercice 2 : Satisfaire des préférences (MaxSAT)

Enonce

Ecrivez une fonction SatisfairePreferences qui assigne nItems items a nSlots creneaux (assignation injective : au plus un item par creneau) de facon a maximiser le nombre de préférences satisfaites.

Paramètres : - nItems : nombre d’items (entiers) - nSlots : nombre de creneaux disponibles - préférences : liste de couples (item, slot_prefere)

Retour attendu : un couple (assignation, nb_satisfaites) ou assignation est une chaîne decrivant l’assignation.

Indices :

# Indice : pour chaque préférence, créez une variable de relaxation Bool et ajoutez ctx.MkOr(slot[item] == slot_pref, r).
# Étape 1 : declarer slot = new IntExpr[nItems] avec bornes [0, nSlots-1].
# Étape 2 : contrainte dure d’injectivite : ctx.MkDistinct(slot) (ou equivalent si nItems < nSlots).
# Étape 3 : pour chaque (item, pref), créer r = ctx.MkBoolConst(...), ajouter ctx.MkOr(ctx.MkEq(slot[item], ctx.MkInt(pref)), r).
# Étape 4 : minimiser la somme des ctx.MkITE(r, 1, 0).
# Étape 5 : extraire l’assignation et le nombre de préférences satisfaites.

// EXERCICE 2 : MaxSAT - assignation d'items maximisant les preferences.
(string assignation, int nbSatisfaites) SatisfairePreferences(Context ctx, int nItems, int nSlots, List<(int item, int slot)> preferences) {
    Console.WriteLine("Exercice 2 - a completer");
    // TODO etudiant : implementez la resolution MaxSAT
    // Indice : utilisez des variables Bool de relaxation pour chaque preference.
    // Etape 1 : declarer slot[i] = Int, bornes [0, nSlots-1]
    // Etape 2 : contrainte ctx.MkDistinct(slot) pour l'injectivite
    // Etape 3 : pour chaque (item, pref), ctx.MkOr(ctx.MkEq(slot[item], ctx.MkInt(pref)), r_i)
    // Etape 4 : minimiser la somme des ctx.MkITE(r_i, 1, 0)
    // Etape 5 : extraire assignation et compter les preferences satisfaites
    return ("(a completer)", 0);  // TODO etudiant : remplacer par le resultat
}

var prefsTest = new List<(int, int)> { (0, 0), (1, 0), (2, 1), (3, 1) };
var resultat = SatisfairePreferences(ctx, 4, 4, prefsTest);
Console.WriteLine($"Resultat MaxSAT : assignation = {resultat.assignation}, nb_satisfaites = {resultat.nbSatisfaites}");

Exercice 2 - a completer
Resultat MaxSAT : assignation = (a completer), nb_satisfaites = 0

6. Cas pratique – allocation de budget

Synthesisons les techniques vues (contraintes dures, contraintes souples ponderees, optimisation multi-objectif) sur un cas concret d’allocation de budget.

Scénario

Une organisation dispose d’un budget de 100 unites a repartir entre 5 projets. Chaque projet $i$ a : - une valeur unitaire $v_i$ (gain par unite investie) - un financement minimum $m_i$ (en-dessous duquel le projet n’est pas viable) - une priorite $p_i$ (1 = haute, 2 = moyenne, 3 = basse)

Objectifs : 1. (Dur) Respecter le budget total et les minimums de financement. 2. (Souple, pondere) Preferer financer les projets haute priorite au-dela de leur minimum. 3. (Principal) Maximiser la valeur totale.

// Allocation de budget multi-projets avec contraintes dures, souples et objectif principal.
var optB = ctx.MkOptimize();
// Donnees : 5 projets (nom, valeur unitaire, financement minimum, priorite)
var projets = new (string nom, int val, int finMin, int prio)[] {
    ("Alpha", 5, 10, 1),   // haute priorite
    ("Beta",  3,  8, 2),   // moyenne priorite
    ("Gamma", 7,  5, 1),   // haute priorite, tres rentable
    ("Delta", 2, 12, 3),   // basse priorite
    ("Epsil", 4,  6, 2),   // moyenne priorite
};
long budgetTotal = 80;
int nProjets = projets.Length;
// Variables : allocation[i] = montant investi dans le projet i
var alloc = new IntExpr[nProjets];
// --- Contraintes DURES ---
for (int i = 0; i < nProjets; i++) {
    alloc[i] = ctx.MkIntConst($"alloc_{projets[i].nom}");
    optB.Assert(ctx.MkGe(alloc[i], ctx.MkInt(projets[i].finMin)));  // minimum viable
    optB.Assert(ctx.MkLe(alloc[i], ctx.MkInt(50)));                 // plafond par projet
}
// Budget total respecte
optB.Assert(ctx.MkLe(ctx.MkAdd(alloc), ctx.MkInt(budgetTotal)));
// --- Contraintes SOUPLES (ponderees) ---
// On souhaite que les projets recoivent au moins 20 unites. Poids inverse de la priorite.
var poidsParPrio = new Dictionary<int, int> { {1, 10}, {2, 5}, {3, 1} };
var coutSouple = (ArithExpr)ctx.MkInt(0);
for (int i = 0; i < nProjets; i++) {
    int poids = poidsParPrio[projets[i].prio];
    var r = ctx.MkBoolConst($"bonus_{projets[i].nom}");
    // Contrainte souple : alloc[i] >= 20 OU penalite
    optB.Assert(ctx.MkOr(ctx.MkGe(alloc[i], ctx.MkInt(20)), r));
    coutSouple = ctx.MkAdd(coutSouple, (ArithExpr)ctx.MkITE(r, ctx.MkInt(poids), ctx.MkInt(0)));
}
var coutViolations = ctx.MkIntConst("cout_violations");
optB.Assert(ctx.MkEq(coutViolations, coutSouple));
// --- Objectif PRINCIPAL : maximiser la valeur totale ---
var valeurExprs = new ArithExpr[nProjets];
for (int i = 0; i < nProjets; i++)
    valeurExprs[i] = ctx.MkMul(ctx.MkInt(projets[i].val), alloc[i]);
var valeurTotale = ctx.MkIntConst("valeur_totale");
optB.Assert(ctx.MkEq(valeurTotale, ctx.MkAdd(valeurExprs)));
// Optimisation lexicographique :
// Priorite 1 : minimiser les violations de contraintes souples (hierarchie)
// Priorite 2 : maximiser la valeur totale
optB.MkMinimize(coutViolations);
optB.MkMaximize(valeurTotale);

Console.WriteLine($"Allocation de budget : {optB.Check()}");
if (optB.Check() == Status.SATISFIABLE) {
    var m = optB.Model;
    Console.WriteLine($"\nBudget total disponible : {budgetTotal}");
    Console.WriteLine($"{"Projet",8} | {"Val/u",5} | {"Min",4} | {"Prio",4} | {"Alloue",6} | {"Valeur",7}");
    Console.WriteLine(new string('-', 50));
    long totalAlloue = 0, totalValeur = 0;
    for (int i = 0; i < nProjets; i++) {
        long a = ((IntNum)m.Evaluate(alloc[i])).Int64;
        long v = projets[i].val * a;
        totalAlloue += a; totalValeur += v;
        Console.WriteLine($"{projets[i].nom,8} | {projets[i].val,5} | {projets[i].finMin,4} | {projets[i].prio,4} | {a,6} | {v,7}");
    }
    Console.WriteLine(new string('-', 50));
    Console.WriteLine($"{"TOTAL",8} | {"",5} | {"",4} | {"",4} | {totalAlloue,6} | {totalValeur,7}");
    Console.WriteLine($"\nCout des violations souples : {((IntNum)m.Evaluate(coutViolations)).Int64}");
    Console.WriteLine($"Budget non utilise : {budgetTotal - totalAlloue}");
}

Allocation de budget : SATISFIABLE

Budget total disponible : 80
  Projet | Val/u |  Min | Prio | Alloue |  Valeur
--------------------------------------------------
   Alpha |     5 |   10 |    1 |     20 |     100
    Beta |     3 |    8 |    2 |      8 |      24
   Gamma |     7 |    5 |    1 |     20 |     140
   Delta |     2 |   12 |    3 |     12 |      24
   Epsil |     4 |    6 |    2 |     20 |      80
--------------------------------------------------
   TOTAL |       |      |      |     80 |     368

Cout des violations souples : 6
Budget non utilise : 0

Interprétation : allocation multi-objectif complète

Sortie obtenue : avec un budget de 80 (inférieur à la demande idéale de 5 x 20 = 100), Z3 ne peut pas satisfaire toutes les contraintes souples simultanément. Il produit une allocation non uniforme qui révèle les deux mécanismes distincts du capstone :

Projet	Val/u	Min	Prio	Alloué	Valeur	Bonus prio ?
Alpha	5	10	1	20	100	Oui
Beta	3	8	2	8	24	Non (ramené au min)
Gamma	7	5	1	20	140	Oui
Delta	2	12	3	12	24	Non (ramené au min)
Epsil	4	6	2	20	80	Oui
TOTAL				80	368	cout = 6

Pourquoi cette instance est discriminante ?

La hiérarchie des priorités est ACTIVE : Z3 ne peut honorer qu’un sous-ensemble des bonus prioritaires. Il sacrifie en priorité le projet de basse priorité Delta (poids 1), le ramenant à son minimum 12, puis Beta (poids 5) à son minimum 8. Les projets haute priorité (Alpha, Gamma prio 1 + Epsil prio 2 tenu) restent à 20. Le cout total des violations = 5 (Beta) + 1 (Delta) = 6 – exactement l’ordre imposé par la pondération. Si le budget avait permis 100, toutes les contraintes souples seraient satisfaites (cout = 0) et la hiérarchie n’aurait eu aucun effet visible.
La maximisation de valeur est ACTIVE : une fois le cout des violations minimisé, Z3 répartit le budget résiduel vers les projets les plus rentables. Gamma (valeur 7) est porté à son plafond pertinent, et le budget économisé sur Delta (valeur 2, le moins rentable) est conservé pour les projets à plus forte valeur. Avec budget=100, l’allocation était forcée à (20,20,20,20,20) et la valeur 420 était identique à celle d’une répartition uniforme triviale – l’objectif de valeur n’aurait rien pu discriminer.

Type de contrainte	Mécanisme Z3 (.NET)	Effet sur la solution (budget=80)
Budget total	`ctx.MkLe(ctx.MkAdd(alloc), ctx.MkInt(80))`	Contrainte dure absolue
Minimum par projet	`ctx.MkGe(alloc[i], ctx.MkInt(finMin))`	Chaque projet viable (Beta=8, Delta=12 à leur minimum)
Bonus priorité	`ctx.MkOr(ctx.MkGe(alloc[i], 20), r)` + poids	Hiérarchie ACTIVE : Delta (poids 1) puis Beta (poids 5) sacrifiés
Valeur totale	`optB.MkMaximize(valeurTotale)`	Optimisée APRÈS cout minimisé : budget vers projets rentables

Points clés : 1. Les contraintes dures garantissent la faisabilité (budget, minimums). 2. Les contraintes souples hiérarchisent les préférences – mais ne sont visibles que si le budget est contraint (ici 80 < 100). Sur un budget généreux, toutes les préférences sont honorées (cout = 0) et la hiérarchie devient invisible. 3. L’objectif principal maximise la valeur une fois les préférences honorées au mieux – ici aussi, ne discrimine que parce que l’instance force un arbitrage. 4. L’ordre optB.MkMinimize(coutViolations) puis optB.MkMaximize(valeurTotale) impose la lexicographie : éliminer les violations d’abord (Delta puis Beta), puis maximiser la valeur sur l’espace restant.

Leçon Prong-B : un problème d’allocation ne met en valeur l’optimisation multi-objectif que si la demande dépasse la ressource. Avec budget=100 = somme exacte des seuils souples, le solveur n’avait aucun arbitrage à faire – il suffisait de donner 20 à chacun. La réduction à budget=80 force l’arbitrage et rend les deux objectifs (hiérarchie + valeur) observables. C’est le cas dégénéré qui rend l’exemple pédagogiquement instructif.

Exercice 3 : Allocation de budget avec priorites

Enonce

Ecrivez une fonction AllouerBudget qui alloue un budget fixe entre plusieurs projets pour maximiser la valeur totale, tout en respectant des contraintes de financement minimum et de priorite.

Paramètres : - budgetTotal : entier, budget disponible - projets : liste de tuples (nom, valeur_unitaire, financement_min, priorite) ou priorite 1 = haute, 2 = moyenne, 3 = basse

Retour attendu : un couple (allocations, valeur_totale) ou allocations est une chaîne decrivant les montants.

Indices :

# Indice : utilisez ctx.MkOptimize() avec opt.MkMaximize(valeur_totale) et des contraintes de minimum.
# Étape 1 : declarer une variable Int par projet avec bornes [financement_min, budget_total].
# Étape 2 : contrainte dure ctx.MkAdd(allocations) <= budget_total.
# Étape 3 : (optionnel) contraintes souples : ctx.MkOr(alloc[i] >= seuil_priorite, r_i) avec poids selon la priorite.
# Étape 4 : valeur_totale = ctx.MkAdd(valeur_unitaire[i] * alloc[i]), puis opt.MkMaximize(valeur_totale).
# Étape 5 : extraire les allocations et calculer la valeur totale.

// EXERCICE 3 : Allocation de budget avec priorites.
(string allocations, long valeurTotale) AllouerBudget(Context ctx, long budgetTotal, List<(string nom, int val, int finMin, int prio)> projets) {
    Console.WriteLine("Exercice 3 - a completer");
    // TODO etudiant : implementez l'allocation optimale
    // Indice : MkOptimize + MkMaximize(valeur) + contraintes de minimum.
    // Etape 1 : declarer alloc par projet, bornee par [finMin, budgetTotal]
    // Etape 2 : contrainte ctx.MkAdd(allocs) <= budgetTotal
    // Etape 3 : (optionnel) contraintes souples selon la priorite
    // Etape 4 : valeur = ctx.MkAdd(val_unit * alloc), opt.MkMaximize(valeur)
    // Etape 5 : extraire allocations et valeur totale
    return ("(a completer)", 0);  // TODO etudiant : remplacer par le resultat
}

var projetsTest = new List<(string, int, int, int)> {
    ("Alpha", 5, 10, 1), ("Beta", 3, 8, 2), ("Gamma", 7, 5, 1), ("Delta", 2, 12, 3),
};
var resultatBudget = AllouerBudget(ctx, 80, projetsTest);
Console.WriteLine($"Allocation optimale : {resultatBudget.allocations}, valeur = {resultatBudget.valeurTotale}");

Exercice 3 - a completer
Allocation optimale : (a completer), valeur = 0

Recapitulatif

Ce notebook a explore les techniques d’optimisation avancee de Z3 au-dela du simple MkMaximize/MkMinimize d’un seul objectif :

Technique	API Microsoft.Z3	Quand l’utiliser
Priorites hiérarchiques	relaxation `Bool` + `MkITE(r, poids, 0)` + `MkMinimize`	Contraintes souples avec importance différente
Objectifs multiples lexicographiques	`opt.MkMaximize` puis `opt.MkMinimize` (ordre de declaration)	Priorites strictes entre objectifs (A domine B)
Front de Pareto	Boucle `MkMaximize` + exclusion successive	Explorer tous les compromis optimaux
MaxSAT uniforme	relaxation `Bool` + `MkMinimize(Sum(MkITE(r,1,0)))` – ou `AssertSoft`	Satisfaire un maximum de préférences equiponderees

Points essentiels a retenir :

Variables de relaxation Bool : c’est l’outil universel pour les contraintes souples. Une contrainte ctx.MkOr(c, r) peut etre violee si r = True, et on penalise cette violation dans l’objectif.
Lexicographique vs pondere : l’optimisation lexicographique (ordre des MkMaximize/MkMinimize) impose une hiérarchie stricte ; la somme ponderee permet des compromis nuances.
Front de Pareto : indispensable quand aucun ordre naturel n’existe entre objectifs. On l’enumere par exclusion successive (forcer l’autre objectif a s’ameliorer a chaque tour).
Domains petits : pour l’enumeration du front de Pareto et les boucles d’optimisation, garder des domains entiers petits (0-20) garantit des temps de calcul raisonnables.
Pattern d’allocation : le cas pratique (section 6) combine tous ces outils : contraintes dures (budget), contraintes souples (priorites), objectif principal (valeur). C’est le squelette de la plupart des problemes d’allocation de ressources reels.

Ces techniques font de Z3 un outil puissant non seulement pour la satisfaction de contraintes, mais aussi pour l’optimisation multi-critères – un domaine ou la modelisation declarative brille face aux approches ad-hoc.

Parite .NET : ce twin C# reproduit fidelement le notebook Python Z3-06-Advanced-Optimization-Python.ipynb avec le même moteur C++ sous-jacent (Microsoft.Z3 / z3-solver). Les différences sont purement d’API : Optimize() -> ctx.MkOptimize(), opt.add() -> opt.Assert(), opt.maximize/minimize -> opt.MkMaximize/MkMinimize (retournent un Handle dont .Upper/.Lower donnent les bornes), et la visualisation matplotlib est remplacée par un rendu ASCII autonome. La serie Z3-Python-Csharp est maintenant complete (6/6).

Retour au sommet

Objectifs d’apprentissage

Prerequis

Duree estimee : ~40 min

1. Rappel et motivation – au-dela d’un seul objectif

La realite est multi-objectif

2. Objectifs hiérarchiques avec Optimize et priorites

Principe

Exemple : ordonnanceur avec contraintes dures et souples

Interpretation : hiérarchie ponderee

3. Objectifs multiples – MkMaximize vs MkMinimize simultanes

Lecture des bornes

Exemple : maximiser le revenu, puis minimiser le cout

Quand lexicographique differe vraiment de la somme ponderee

Interpretation : lexicographique vs pondere

4. Front de Pareto – explorer les compromis

Méthode d’enumeration

Exemple : qualite vs cout

Visualiser le front de Pareto

Interpretation : front de Pareto

Exercice 1 : Construire un front de Pareto

Enonce

5. Contraintes souples (soft constraints) et MaxSAT

Formalisation

Exemple : assignation de salles avec préférences

Interpretation : MaxSAT et variables de relaxation

Exercice 2 : Satisfaire des préférences (MaxSAT)

Enonce

6. Cas pratique – allocation de budget

Scénario

Interprétation : allocation multi-objectif complète

Exercice 3 : Allocation de budget avec priorites

Enonce

Recapitulatif

2. Objectifs hiérarchiques avec `Optimize` et priorites

3. Objectifs multiples – `MkMaximize` vs `MkMinimize` simultanes