Z3-Python 06 — Optimisation avancee

Navigation : Index | Index SMT | Index SymbolicAI | Serie Z3 C# | << Z3-Python-03 Tactiques

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. Enumereer 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 (Introduction) : Solver, Int, Bool, Real, Optimize de base
Z3-Python 03 (Tactiques) : familiarite avec Bool, Or, And, If
Notions d’optimisation combinatoire (maximisation sous contraintes)

Duree estimee : ~40 min

Ce notebook 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 : python3 (conda Python 3 standard). Aucun kernel WSL requis.

# Imports et verification de l'environnement
# Le package pip s'appelle 'z3-solver' (et non 'z3').
# !pip install z3-solver

from z3 import *

print(f"Imports OK : z3-solver version {get_version_string()}")

Imports OK : z3-solver version 4.16.0

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 :

opt = Optimize()
opt.add(contraintes_dures)
opt.maximize(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 `unsat`.
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 Bool) et on ajoute Or(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 Z3, la fonction If(r_i, weight_i, 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)
# et dure 1 unite de temps. Deux taches ne peuvent s'executer au meme instant.

opt = Optimize()

# Variables de decision : creneau de debut de chaque tache (0 a 9)
debut = [Int(f'debut_{i}') for i in range(3)]
for d in debut:
    opt.add(d >= 0, d <= 9)

# --- Contraintes DURES (hard) ---
# Les trois taches doivent occuper des creneaux distincts.
opt.add(debut[0] != debut[1])
opt.add(debut[1] != debut[2])
opt.add(debut[0] != debut[2])

# T0 doit absolument commencer apres le creneau 2 (contrainte externe)
opt.add(debut[0] >= 2)

# --- Contraintes SOUPLES (soft) avec poids ---
# Chaque preference est relaxee par une variable booleenne r_i.
# On minimise la somme ponderee des r_i 'True'.
preferences = [
    # (description, contrainte, poids)
    ("T0 le plus tot possible (debut_0 == 2)", debut[0] == 2, 10),
    ("T1 avant T0 (debut_1 < debut_0)",     debut[1] < debut[0], 7),
    ("T2 en dernier (debut_2 > debut_0)",    debut[2] > debut[0], 5),
    ("T1 au creneau 0 (debut_1 == 0)",       debut[1] == 0, 3),
]

relax_vars = []
cout_total = Int('cout_total')
cout_total_val = IntVal(0)

for idx, (desc, contrainte, poids) in enumerate(preferences):
    r = Bool(f'r_{idx}')
    relax_vars.append((desc, r, poids))
    # Contrainte relachee : c_i OU r_i
    opt.add(Or(contrainte, r))
    cout_total_val = cout_total_val + If(r, poids, 0)

opt.add(cout_total == cout_total_val)
opt.minimize(cout_total)

print("Ordonnancement hierarchique :", opt.check())
if opt.check() == sat:
    m = opt.model()
    print("\nPlanning obtenu :")
    for i in range(3):
        print(f"  T{i} : creneau {m[debut[i]].as_long()}")
    print("\nContraintes souples :")
    cout = 0
    for desc, r, poids in relax_vars:
        violee = bool(m[r])
        penalite = poids if violee else 0
        cout += penalite
        statut = "VIOLEE" if violee else "satisfaite"
        print(f"  [{statut:9s}] (poids {poids:2d}) {desc}")
    print(f"\nCout total des violations : {m[cout_total].as_long()}")

Ordonnancement hierarchique : sat

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

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.

Mécanisme	API Z3	Rôle
Variable de relaxation	`Bool(f'r_{i}')`	Vaut `True` si la contrainte souple est violee
Contrainte relachee	`Or(contrainte, r_i)`	Permet la violation via `r_i`
Penalite	`If(r_i, poids, 0)`	Contribution au cout total si violation
Objectif	`opt.minimize(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.add sans relaxation). 3. Le cout total obtenu est le minimum : aucune autre assignation ne donne une somme ponderee de violations inferieure.

Note technique : Le choix des poids est decisive. Un ecart de 1 entre deux poids peut basculer la solution. En pratique, on utilise souvent une echelle exponentielle (1, 2, 4, 8…) pour garantir une veritable hiérarchie lexicographique approximative.

3. Objectifs multiples — `maximize` vs `minimize` simultanes

Un Optimize peut contenir plusieurs objectifs declares via o.maximize(...) et o.minimize(...). Z3 resout ces objectifs de maniere lexicographique (par ordre de declaration) lorsqu’ils sont declares successivement : 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 o.maximize(expr) ou o.minimize(expr) renvoie un handle (un objet Objective). Après o.check(), on peut interroger :

o.upper(handle) : borne superieure de l’objectif (utile après maximize).
o.lower(handle) : borne inferieure de l’objectif (utile après minimize).

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

opt = Optimize()
q = Int('q')
opt.add(q >= 0, q <= 15)  # capacite de production

revenu = 8 * q
cout = 3 * q

# Declaration des objectifs dans l'ordre de priorite (lexicographique)
h_revenu = opt.maximize(revenu)  # priorite 1 : maximiser le revenu
h_cout = opt.minimize(cout)      # priorite 2 : minimiser le cout

print("Multi-objectif lexicographique :", opt.check())
if opt.check() == sat:
    m = opt.model()
    q_val = m[q].as_long()
    print(f"\nSolution : q = {q_val} unites")
    print(f"  Revenu = 8 x {q_val} = {8 * q_val} EUR (maximise en priorite)")
    print(f"  Cout   = 3 x {q_val} = {3 * q_val} EUR (minimise ensuite)")
    print(f"  Profit net = {8 * q_val - 3 * q_val} EUR")
    print(f"\nBornes : revenu <= {opt.upper(h_revenu)}, cout >= {opt.lower(h_cout)}")

# Demonstration : comparaison avec un seul objectif (profit net = revenu - cout)
# Si on maximisait directement le profit net, le resultat serait different.
opt2 = Optimize()
q2 = Int('q2')
opt2.add(q2 >= 0, q2 <= 15)
profit = 8 * q2 - 3 * q2  # = 5 * q2
opt2.maximize(profit)
print("\n--- Comparaison : maximisation du profit net (5 * q) ---")
print("Resultat :", opt2.check())
if opt2.check() == sat:
    m2 = opt2.model()
    print(f"  q = {m2[q2].as_long()}, profit = {5 * m2[q2].as_long()} EUR")
    print("\nDans cet exemple les deux approches convergent (profit croissant en q),")
    print("mais en general lexicographique != somme ponderee.")

Multi-objectif lexicographique : sat

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 : sat
  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 (maximize puis minimize par ordre de priorite) 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 (q1 + q2 <= 15).
#   - premium (q1) : revenu 8/u, cout 10/u   -> perte de 2/u
#   - standard (q2): revenu 3/u, cout 1/u    -> profit de 2/u
CAPACITE = 15

# --- Strategie 1 : LEXICOGRAPHIQUE (max revenu, puis min cout) ---
opt = Optimize()
q1, q2 = Ints('q1 q2')
opt.add(q1 >= 0, q2 >= 0, q1 + q2 <= CAPACITE)
revenu = 8 * q1 + 3 * q2
cout = 10 * q1 + 1 * q2
opt.maximize(revenu)   # priorite 1 : chiffre d'affaires brut
opt.minimize(cout)     # priorite 2 : cout (secondaire)
assert opt.check() == sat
m = opt.model()
r1, c1 = 8 * m[q1].as_long() + 3 * m[q2].as_long(), 10 * m[q1].as_long() + 1 * m[q2].as_long()
print("Lexicographique (CA brut prioritaire) :")
print(f"  premium={m[q1].as_long()}, standard={m[q2].as_long()} -> CA={r1}, cout={c1}, profit={r1 - c1}")

# --- Strategie 2 : SOMME PONDEREE (max profit net = revenu - cout) ---
opt2 = Optimize()
p1, p2 = Ints('p1 p2')
opt2.add(p1 >= 0, p2 >= 0, p1 + p2 <= CAPACITE)
profit = (8 * p1 + 3 * p2) - (10 * p1 + 1 * p2)   # = -2*p1 + 2*p2
opt2.maximize(profit)
assert opt2.check() == sat
m2 = opt2.model()
r2, c2 = 8 * m2[p1].as_long() + 3 * m2[p2].as_long(), 10 * m2[p1].as_long() + 1 * m2[p2].as_long()
print("Somme ponderee (profit net prioritaire) :")
print(f"  premium={m2[p1].as_long()}, standard={m2[p2].as_long()} -> CA={r2}, cout={c2}, profit={r2 - c2}")

print("\n=> Les deux strategies DIVERGENT : lexicographique sacrifie le profit pour")
print("   le CA brut (premium a perte), la somme ponderee fait l'inverse (standard).")

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

=> Les deux strategies DIVERGENT : lexicographique sacrifie le profit pour
   le CA brut (premium a perte), la somme ponderee fait l'inverse (standard).

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. opt.upper(handle) donne la valeur optimale d’un objectif maximize ; opt.lower(handle) pour minimize. 2. L’ordre de declaration des maximize/minimize 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 unsat.

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.
# Modele : qualite et cout sont des entiers lies par une relation lineaire.
# Une qualite elevee exige un cout minimal, mais le cout peut depasser ce minimum.

def enumerer_front_pareto(max_iter=15):
    """Enumere les points Pareto-optimaux (qualite, cout).

    Strategie lexicographique en deux phases, a chaque iteration :
      1. maximiser la qualite sous cout < cout_precedent (objectif primaire) ;
      2. a qualite ainsi fixee, minimiser le cout (objectif secondaire).
    La phase 2 est indispensable : sans elle, Z3 renvoie un cout quelconque dans
    [2*qualite, cout_precedent-1] et le point est alors DOMINE (le meme niveau de
    qualite existe pour un cout strictement inferieur) -> ce ne serait PAS un
    point Pareto-optimal.
    """
    front = []
    for iteration in range(max_iter):
        # --- Phase 1 : qualite maximale sous cout < cout_precedent ---
        opt = Optimize()
        qualite = Int('qualite')
        cout = Int('cout')
        opt.add(qualite >= 0, qualite <= 10)
        opt.add(cout >= 0, cout <= 20)
        opt.add(cout >= qualite * 2)
        for (_, c_prec) in front:
            opt.add(cout < c_prec)
        opt.maximize(qualite)
        if opt.check() != sat:
            break  # plus de solution : front complet
        q_val = opt.model()[qualite].as_long()

        # --- Phase 2 : a qualite fixee, cout minimal -> point reellement Pareto-optimal ---
        opt2 = Optimize()
        cout2 = Int('cout2')
        opt2.add(cout2 >= q_val * 2)
        opt2.add(cout2 <= 20)
        for (_, c_prec) in front:
            opt2.add(cout2 < c_prec)
        opt2.minimize(cout2)
        if opt2.check() != sat:
            break
        c_val = opt2.model()[cout2].as_long()
        front.append((q_val, c_val))

    return front


front = enumerer_front_pareto()
print("Front de Pareto (qualite max, cout min) :")
print(f"{'Point':>6} | {'Qualite':>7} | {'Cout':>5} | {'Cout min = 2*q':>15}")
print("-" * 45)
for i, (q, c) in enumerate(front):
    cout_min = q * 2
    marque = " <-- cout min" if c == cout_min else ""
    print(f"{i + 1:>6} | {q:>7} | {c:>5} | {cout_min:>15}{marque}")

print(f"\n{len(front)} points Pareto-optimaux trouves (qualites distinctes).")
print("Chaque point est un compromis : pour baisser le cout, il faut")
print("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 |    18 |              18 <-- cout min
     3 |       8 |    16 |              16 <-- cout min
     4 |       7 |    14 |              14 <-- cout min
     5 |       6 |    12 |              12 <-- cout min
     6 |       5 |    10 |              10 <-- cout min
     7 |       4 |     8 |               8 <-- cout min
     8 |       3 |     6 |               6 <-- cout min
     9 |       2 |     4 |               4 <-- cout min
    10 |       1 |     2 |               2 <-- cout min
    11 |       0 |     0 |               0 <-- cout min

11 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 (qualité, coût), le front devient une courbe descendante : chaque pas vers un coût plus bas coûte de la qualité. La droite coût_min = 2 × qualité (la frontière de faisabilité imposée par le modèle) apparaît en pointillés : les points du front se superposent exactement à cette droite. Ce n’est pas un hasard — pour ce modèle, le coût minimal d’une qualité q vaut précisément 2*q (contrainte cout >= 2*qualite), et l’énumération en deux phases (maximiser la qualité, puis minimiser le coût à qualité fixée) garantit que chaque point retombe sur ce plancher. On obtient ainsi la véritable frontière de Pareto : aucun point n’est dominé.

# Visualisation du front de Pareto : qualite (x) vs cout (y).
# On distingue les points Pareto-optimaux de la borne minimale cout = 2 * qualite.

import matplotlib.pyplot as plt

# front est calcule par la cellule precedente (enumerer_front_pareto)
qualites = [q for (q, _) in front]
couts = [c for (_, c) in front]

fig, ax = plt.subplots(figsize=(7, 4.5))

# Borne de faisabilite : cout_min = 2 * qualite (frontiere inferieure du modele)
q_line = range(0, 11)
ax.plot(list(q_line), [2 * q for q in q_line], "k--", alpha=0.5, label="coût_min = 2 × qualité")

# Front de Pareto : les compromis optimaux enumeres par Z3
ax.plot(qualites, couts, "o-", color="#1f77b4", linewidth=2, markersize=8,
        label="front de Pareto (Z3)")

# Annoter chaque point pour rendre le compromis lisible
for q, c in zip(qualites, couts):
    ax.annotate(f"({q},{c})", (q, c), textcoords="offset points", xytext=(6, 6), fontsize=8)

ax.set_xlabel("Qualité (à maximiser)")
ax.set_ylabel("Coût (à minimiser)")
ax.set_title("Front de Pareto : compromis qualité ↔ coût")
ax.legend(loc="upper left")
ax.grid(True, alpha=0.3)
fig.tight_layout()
plt.show()

print(f"Le front comporte {len(front)} compromis Pareto-optimaux.")
print("La pente descendante illustre le trade-off : baisser le coût dégrade la qualité.")

Le front comporte 11 compromis Pareto-optimaux.
La pente descendante illustre le trade-off : baisser le coût dégrade la qualité.

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. Ici, comme le cout minimal d’une qualite q vaut 2*q, chaque point retombe exactement sur le plancher cout = 2*qualite.

Étape	Action	Résultat
1	`opt.maximize(qualite)` sous `cout < cout_precedent`	Qualite maximale encore atteignable
2	`opt2.minimize(cout)` a qualite fixee	Cout minimal pour cette qualite -> point reellement Pareto-optimal
3	Repeter jusqu’a `unsat`	Front complet

Points cles : 1. Le front de Pareto contient les compromis optimaux : aucun point n’est domine par un autre. 2. La phase 2 (minimiser le cout a qualite fixee) est essentielle : sans elle, Z3 renvoie un cout quelconque entre 2*q et le cout precedent, et le point obtenu est alors domine — ce ne serait pas un vrai point Pareto-optimal. 3. Le nombre de points est fini (domains entiers petits), mais peut etre grand si les ranges sont larges. 4. 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 prohibitif.

Exercice 1 : Construire un front de Pareto

Enonce

Ecrivez une fonction construire_front_pareto() 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 = [] et boucler (par exemple for _ in range(15)).
# Étape 2 : dans la boucle, créer opt = Optimize(), 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.maximize(qualite) puis opt.check() ; si unsat, break.
# Étape 5 : extraire les valeurs et les ajouter a front.

# EXERCICE 1 : Enumerer le front de Pareto (qualite vs cout).

def construire_front_pareto(max_iter: int = 15) -> list:
    """Retourne la liste des points Pareto-optimaux (qualite, cout).

    Contraintes du modele :
      - qualite est un entier dans [0, 10]
      - cout est un entier dans [0, 20]
      - cout >= qualite * 2

    Objectif : maximiser qualite a chaque tour, puis forcer cout plus bas.

    # Indice : bouclez, a chaque iteration maximisez qualite, enregistrez
    #           (qualite, cout), puis ajoutez cout < cout_actuel comme contrainte.
    # Etape 1 : initialiser front = []
    # Etape 2 : boucler (for _ in range(max_iter))
    # Etape 3 : creer un Optimize, ajouter les bornes et cout >= qualite * 2
    # Etape 4 : ajouter cout < cout_prec pour chaque point deja trouve
    # Etape 5 : opt.maximize(qualite), si unsat -> break, sinon extraire et ajouter
    """
    print("Exercice 1 - a completer")
    # TODO etudiant : implémentez l'énumération du front de Pareto
    return None  # TODO etudiant : remplacer par la liste des couples (qualite, cout)


front = construire_front_pareto()
print("Front de Pareto :", front)

Exercice 1 - a completer
Front de Pareto : None

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 each). 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.

opt = Optimize()

n = 4
# Variable : salle[i] = numero de salle assignee a l'etudiant i
salle = [Int(f'salle_{i}') for i in range(n)]
for i in range(n):
    opt.add(salle[i] >= 0, salle[i] <= 3)

# Contrainte DURE : assignation bijective (chaque salle a exactement un etudiant)
opt.add(Distinct(salle))

# Preferences (contraintes SOUPLES, toutes de poids 1 = MaxSAT uniforme)
preferences = [
    (0, 0),  # E0 prefere S0
    (1, 0),  # E1 prefere S0 (conflit avec E0)
    (2, 2),  # E2 prefere S2
    (3, 1),  # E3 prefere S1
]

relax_vars = []
somme_violations = IntVal(0)

for etudiant, salle_pref in preferences:
    r = Bool(f'pref_{etudiant}_{salle_pref}')
    relax_vars.append((etudiant, salle_pref, r))
    # Contrainte relachee : etudiant obtient sa salle OU r est vrai
    opt.add(Or(salle[etudiant] == salle_pref, r))
    somme_violations = somme_violations + If(r, 1, 0)

# Objectif : minimiser le nombre de preferences non satisfaites
nb_violations = Int('nb_violations')
opt.add(nb_violations == somme_violations)
opt.minimize(nb_violations)

print("MaxSAT (assignation de salles) :", opt.check())
if opt.check() == sat:
    m = opt.model()
    print("\nAssignation optimale :")
    nb_satisfaites = 0
    for etudiant, salle_pref, r in relax_vars:
        s = m[salle[etudiant]].as_long()
        violee = bool(m[r])
        symbole = "OK" if not violee else "--"
        if not violee:
            nb_satisfaites += 1
        print(f"  E{etudiant} -> S{s}  (preferait S{salle_pref}) [{symbole}]")
    print(f"\nPreferences satisfaites : {nb_satisfaites} / {len(preferences)}")
    print(f"Violations minimales : {m[nb_violations].as_long()}")
    print("\nZ3 ne pouvait pas satisfaire E0 et E1 simultanement (meme preference S0).")
    print("Il a choisit d'en satisfaire un et sacrifie l'autre (1 violation minimum).")

MaxSAT (assignation de salles) : sat

Assignation optimale :
  E0 -> S3  (preferait S0) [--]
  E1 -> S0  (preferait S0) [OK]
  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 choisit 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 prefèrent la même salle S0.

Élément	Implementation	Rôle
Contrainte dure	`Distinct(salle)`	Une salle par etudiant, pas de doublon
Contrainte souple	`Or(salle[i] == pref, r_i)`	Préférence violable si `r_i = True`
Compteur	`If(r_i, 1, 0)`	Contribution unitaire au nombre de violations
Objectif	`opt.minimize(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. Distinct est un sucre syntaxique pour AllDifferent : toutes les valeurs doivent etre distinctes. 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 : 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 satisfaire_preferences(n_items, n_slots, préférences) qui assigne n_items items a n_slots creneaux (assignation injective : au plus un item par creneau) de facon a maximiser le nombre de préférences satisfaites.

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

Retour attendu : un dictionnaire {'assignation': {item: slot, ...}, 'nb_satisfaites': int}.

Indices :

# Indice : pour chaque préférence, créez une variable de relaxation Bool et ajoutez Or(slot[item] == slot_pref, r).
# Étape 1 : declarer slot = [Int(f'slot_{i}') for i in range(n_items)] avec bornes [0, n_slots-1].
# Étape 2 : contrainte dure d’injectivite : Distinct(slot) (ou equivalent si n_items < n_slots).
# Étape 3 : pour chaque (item, pref), créer r = Bool(...), ajouter Or(slot[item] == pref, r).
# Étape 4 : minimiser la somme des If(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.

def satisfaire_preferences(n_items: int, n_slots: int, preferences: list) -> dict:
    """Assigne n_items a n_slots (injectif) en maximisant les preferences.

    Retourne : {'assignation': {item: slot}, 'nb_satisfaites': int}

    # Indice : utilisez des variables Bool de relaxation pour chaque preference.
    # Etape 1 : declarer slot[i] = Int, bornes [0, n_slots-1]
    # Etape 2 : contrainte Distinct(slot) pour l'injectivite
    # Etape 3 : pour chaque (item, pref), Or(slot[item] == pref, r_i)
    # Etape 4 : minimiser la somme des If(r_i, 1, 0)
    # Etape 5 : extraire assignation et compter les preferences satisfaites
    """
    print("Exercice 2 - a completer")
    # TODO etudiant : implémentez la résolution MaxSAT
    return None  # TODO etudiant : remplacer par le résultat


# Test avec 4 items, 4 slots, preferences conflictuelles
prefs_test = [(0, 0), (1, 0), (2, 1), (3, 1)]
resultat = satisfaire_preferences(4, 4, prefs_test)
print("Resultat MaxSAT :", resultat)

Exercice 2 - a completer
Resultat MaxSAT : None

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 80 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 financert 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.

opt = Optimize()

# Donnees : 5 projets (valeur unitaire, financement minimum, priorite)
projets = [
    # (nom, valeur_unitaire, fin_min, priorite)
    ("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
]
budget_total = 80
n_projets = len(projets)

# Variables : allocation[i] = montant investi dans le projet i
alloc = [Int(f'alloc_{projets[i][0]}') for i in range(n_projets)]

# --- Contraintes DURES ---
# Financement minimum et plafond individuel
for i in range(n_projets):
    nom, val, fin_min, prio = projets[i]
    opt.add(alloc[i] >= fin_min)   # minimum viable
    opt.add(alloc[i] <= 50)        # plafond par projet

# Budget total respecte
somme_alloc = Sum(alloc)
opt.add(somme_alloc <= budget_total)

# --- Contraintes SOUPLES (ponderees) ---
# On souhaite que les projets haute priorite (priorite 1) recoivent au moins 20 unites.
# Poids inverse de la priorite : priorite 1 -> poids 10, 2 -> poids 5, 3 -> poids 1.
cout_souple = IntVal(0)
for i in range(n_projets):
    nom, val, fin_min, prio = projets[i]
    poids = {1: 10, 2: 5, 3: 1}[prio]
    r = Bool(f'bonus_{nom}')
    # Contrainte souple : alloc[i] >= 20 OU penalite
    opt.add(Or(alloc[i] >= 20, r))
    cout_souple = cout_souple + If(r, poids, 0)

# Variable de cout souple (pour lisibilite)
cout_violations = Int('cout_violations')
opt.add(cout_violations == cout_souple)

# --- Objectif PRINCIPAL : maximiser la valeur totale ---
valeur_totale = Int('valeur_totale')
valeur_expr = Sum([projets[i][1] * alloc[i] for i in range(n_projets)])
opt.add(valeur_totale == valeur_expr)

# Optimisation lexicographique :
# Priorite 1 : minimiser les violations de contraintes souples (hierarchie)
# Priorite 2 : maximiser la valeur totale
opt.minimize(cout_violations)
opt.maximize(valeur_totale)

print("Allocation de budget :", opt.check())
if opt.check() == sat:
    m = opt.model()
    print(f"\nBudget total disponible : {budget_total}")
    print(f"\n{'Projet':>8} | {'Val/u':>5} | {'Min':>4} | {'Prio':>4} | {'Alloue':>6} | {'Valeur':>7}")
    print("-" * 50)
    total_alloue = 0
    total_valeur = 0
    for i in range(n_projets):
        nom, val, fin_min, prio = projets[i]
        a = m[alloc[i]].as_long()
        v = val * a
        total_alloue += a
        total_valeur += v
        print(f"{nom:>8} | {val:>5} | {fin_min:>4} | {prio:>4} | {a:>6} | {v:>7}")
    print("-" * 50)
    print(f"{'TOTAL':>8} | {'':>5} | {'':>4} | {'':>4} | {total_alloue:>6} | {total_valeur:>7}")
    print(f"\nCout des violations souples : {m[cout_violations].as_long()}")
    print(f"Budget non utilise : {budget_total - total_alloue}")

Allocation de budget : sat

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

Interpretation : allocation multi-objectif complete

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	Effet sur la solution (budget=80)
Budget total	`somme_alloc <= 80`	Contrainte dure absolue
Minimum par projet	`alloc[i] >= fin_min`	Chaque projet viable (Beta=8, Delta=12 à leur minimum)
Bonus priorité	`Or(alloc[i] >= 20, r)` + poids	Hiérarchie ACTIVE : Delta (poids 1) puis Beta (poids 5) sacrifiés
Valeur totale	`maximize(valeur_totale)`	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 minimize(cout) puis maximize(valeur) 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 allouer_budget(budget_total, projets) 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 : - budget_total : entier, budget disponible - projets : liste de tuples (nom, valeur_unitaire, financement_min, priorite) ou priorite 1 = haute, 2 = moyenne, 3 = basse

Retour attendu : {'allocations': {nom: montant}, 'valeur_totale': int}.

Indices :

# Indice : utilisez Optimize avec maximize(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 Sum(allocations) <= budget_total.
# Étape 3 : (optionnel) contraintes souples : Or(alloc[i] >= seuil_priorite, r_i) avec poids selon la priorite.
# Étape 4 : valeur_totale = Sum(valeur_unitaire[i] * alloc[i]), puis opt.maximize(valeur_totale).
# Étape 5 : extraire les allocations et calculer la valeur totale.

# EXERCICE 3 : Allocation de budget avec priorites.

def allouer_budget(budget_total: int, projets: list) -> dict:
    """Aloue budget_total entre les projets pour maximiser la valeur totale.

    Respecte : financement_min par projet, budget total, priorites (optionnel).

    Retourne : {'allocations': {nom: montant}, 'valeur_totale': int}

    # Indice : Optimize + maximize(valeur) + minimum-funding constraints.
    # Etape 1 : declarer Int(f'alloc_{nom}') borne par [fin_min, budget_total]
    # Etape 2 : contrainte Sum(allocs) <= budget_total
    # Etape 3 : (optionnel) contraintes souples selon la priorite
    # Etape 4 : valeur = Sum(val_unit * alloc), opt.maximize(valeur)
    # Etape 5 : extraire allocations et valeur totale
    """
    print("Exercice 3 - a completer")
    # TODO etudiant : implémentez l'allocation optimale
    return None  # TODO etudiant : remplacer par le résultat


# Test : 4 projets, budget 80
projets_test = [
    ("Alpha", 5, 10, 1),
    ("Beta",  3,  8, 2),
    ("Gamma", 7,  5, 1),
    ("Delta", 2, 12, 3),
]
resultat = allouer_budget(80, projets_test)
print("Allocation optimale :", resultat)

Exercice 3 - a completer
Allocation optimale : None

Recapitulatif

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

Technique	API Z3	Quand l’utiliser
Priorites hiérarchiques	`Bool` relaxation + `If(r, poids, 0)` + `minimize`	Contraintes souples avec importance différente
Objectifs multiples lexicographiques	`opt.maximize` puis `opt.minimize` (ordre de declaration)	Priorites strictes entre objectifs (A domine B)
Front de Pareto	Boucle `maximize` + exclusion successive	Explorer tous les compromis optimaux
MaxSAT uniforme	Relaxation `Bool` + `minimize(Sum(If(r,1,0)))`	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 Or(c, r) peut etre violee si r = True, et on penalise cette violation dans l’objectif.
Lexicographique vs pondere : l’optimisation lexicographique (ordre des maximize/minimize) 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.

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 — maximize vs minimize 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

Interpretation : allocation multi-objectif complete

Exercice 3 : Allocation de budget avec priorites

Enonce

Recapitulatif

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

3. Objectifs multiples — `maximize` vs `minimize` simultanes