← 13 — Cryptarithmetic SMT | README Z3

Notebook 14 — De SAT à OPT : optimisation et contraintes molles (MaxSAT)

Navigation : Index Z3 | Index SymbolicAI | Index général

Objectifs d’apprentissage

  • Passer de la satisfiabilité (.Solve() : existe-t-il une solution ?) à l’optimisation (.Optimize() : quelle est la meilleure solution selon un critère ?)
  • Modéliser le problème du sac à dos (0/1 knapsack) comme un théorème Z3.Linq avec un objectif à maximiser
  • Comprendre les contraintes molles (soft constraints) et le paradigme MaxSAT : maximiser le nombre de préférences satisfaites sous contraintes dures
  • Mettre en évidence le gap de la série : jusqu’ici tous les notebooks cherchaient une solution quelconque ; l’optimisation ouvre la porte à des problèmes de décision multicritères

Prérequis

Durée estimée : 40-50 minutes

Les dix premiers notebooks de la série posent des problèmes de satisfiabilité : existe-t-il une affectation des variables qui satisfait toutes les contraintes ? Le solveur répond par une solution quelconque (la première trouvée), via .Solve(). C’est le cadre SAT (ou SMT, avec théories).

Mais de nombreux problèmes réels ne demandent pas une solution, mais la meilleure selon un critère : minimiser un coût, maximiser une valeur, satisfaire un maximum de préférences. C’est le cadre de l’optimisation — et Z3 fournit un solveur d’optimisation dédié, exposé par Z3.Linq via la méthode .Optimize() et la syntaxe LINQ orderby.

Ce notebook comble un gap volontairement laissé ouvert par les notebooks précédents : aucun n’utilisait .Optimize(). On le fait ici sur deux terrains — le sac à dos (optimisation entière simple) puis le roulement d’affectation (MaxSAT : contraintes dures + préférences molles).

#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
Console.WriteLine("Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.Linq");
Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.Linq

De .Solve() à .Optimize()

La classe Theorem<T> expose, au-delà de .Solve(), deux points d’entrée pour l’optimisation :

API Rôle Équivalent LINQ
th.Optimize(Optimization.Minimize, t => t.Cout) minimise l’expression donnée orderby t.Cost
th.Optimize(Optimization.Maximize, t => t.Score) maximise l’expression donnée orderby t.Score descending
th.OrderBy(t => t.Cost).Solve() idiomatique LINQ (minimise) —

Le binding traduit l’expression-objectif en une assertion maximize/minimize Z3 (ctx.MkOptimize() + MkMaximize/MkMinimize), et le solveur explore l’espace de recherche à la recherche de l’optimum global, pas seulement d’une solution faisable.

Concrètement, la différence se voit dans la signature : .Solve() renvoie T? (une solution ou rien si UNSAT), .Optimize() renvoie T (la meilleure solution — s’il existe au moins une solution faisable).

Premier terrain : le sac à dos 0/1 (knapsack)

Le problème du sac à dos est le paradigme canonique de l’optimisation combinatoire : étant donné n objets (chacun avec un poids w_i et une valeur v_i) et une capacité maximale W, choisir le sous-ensemble d’objets qui maximise la valeur totale sans dépasser la capacité.

Modélisation Z3.Linq : une variable entière {0,1} par objet (1 = pris, 0 = laissé), une contrainte linéaire sur le poids total, et un objectif à maximiser (la valeur totale). C’est un problème NP-difficile, mais sur une petite instance le solveur trouve l’optimum instantanément.

// Sac à dos 0/1 : 5 objets, capacité 10
// (poids, valeur) par objet
int[] poids  = { 4, 5, 6, 3, 2 };
int[] valeur = { 10, 15, 16, 7, 5 };
int W = 10;

public class Knapsack
{
    public int x0=0, x1=0, x2=0, x3=0, x4=0;  // 1 si l'objet i est pris
}

using (var ctx = new Z3Context())
{
    var th = ctx.NewTheorem<Knapsack>();

    // Domaine {0,1} pour chaque objet
    th = th.Where(t => t.x0>=0&&t.x0<=1 && t.x1>=0&&t.x1<=1 && t.x2>=0&&t.x2<=1 && t.x3>=0&&t.x3<=1 && t.x4>=0&&t.x4<=1);

    // Contrainte de capacité : poids total <= W
    th = th.Where(t => 4*t.x0 + 5*t.x1 + 6*t.x2 + 3*t.x3 + 2*t.x4 <= W);

    // Objectif : maximiser la valeur totale
    var sol = th.Optimize(Optimization.Maximize, t => 10*t.x0 + 15*t.x1 + 16*t.x2 + 7*t.x3 + 5*t.x4);

    int poidsTotal  = 4*sol.x0 + 5*sol.x1 + 6*sol.x2 + 3*sol.x3 + 2*sol.x4;
    int valeurTotal = 10*sol.x0 + 15*sol.x1 + 16*sol.x2 + 7*sol.x3 + 5*sol.x4;

    Console.WriteLine("Objets pris (1=pris) : " + string.Join(", ", sol.x0, sol.x1, sol.x2, sol.x3, sol.x4));
    Console.WriteLine($"Poids total  : {poidsTotal} / {W}");
    Console.WriteLine($"Valeur totale: {valeurTotal}  (optimum)");
}
Objets pris (1=pris) : 0, 1, 0, 1, 1
Poids total  : 10 / 10
Valeur totale: 27  (optimum)

Lecture du sac à dos

Z3 trouve l’optimum en explorant l’espace des \(2^5 = 32\) sous-ensembles d’objets. La solution maximise la valeur sans dépasser la capacité — c’est exactement ce que ferait une programmation dynamique, mais sans écrire l’algorithme : on décrit le problème (variables, domaine, contrainte, objectif), le solveur trouve l’optimum.

Verdict honnête (Prong-B) : sur cette instance jouet, le sac à dos est trivial — une énumération exhaustive ou une DP le résout aussi vite. L’intérêt ici est pédagogique : introduire l’API .Optimize() sur un problème dont l’énoncé est familier. Le terrain où l’optimisation SMT discrimine vraiment apparaît dans la section suivante, avec les contraintes molles (MaxSAT) — là où il faut arbitrer entre des préférences conflictuelles.

Second terrain : contraintes molles et MaxSAT (roulement d’infirmières)

Le sac à dos optimise un objectif quantitatif (une valeur). Beaucoup de problèmes réels sont multicritères : on a des contraintes dures (qui doivent être satisfaites) et des préférences (qu’on aimerait satisfaire, mais qu’on peut violer au prix d’une pénalité). C’est le cadre du MaxSAT (satisfiabilité maximale) :

  • Contraintes dures (hard) : modélisées par .Where(...) — impératives.
  • Préférences molles (soft) : encodées dans l’objectif — on maximise le nombre de préférences satisfaites.

Le terrain canonique est le roulement d’affectation (nurse rostering) : on doit staffier des gardes (contraintes dures : couverture, pas de double-garde) tout en respectant au mieux les préférences des employés (soft). Quand deux employés veulent le même créneau, le solveur arbitre pour maximiser globalement la satisfaction.

Considérons 3 infirmières (A, B, C) à affecter à 3 gardes (G1, G2, G3), une infirmière par garde. Préférences : A veut G1, B veut G1 aussi, C veut G2. Le conflit (A et B veulent G1) rend impossible de satisfaire tout le monde — c’est précisément là que MaxSAT prouve sa valeur.

// Nurse rostering (MaxSAT) : 3 infirmieres x 3 gardes, 1 infirmiere/garde.
// Variables {0,1} : A_Gi = 1 si l'infirmiere A prend la garde Gi.
public class NurseRoster
{
    public int A_G1=0, A_G2=0, A_G3=0;
    public int B_G1=0, B_G2=0, B_G3=0;
    public int C_G1=0, C_G2=0, C_G3=0;
}

using (var ctx = new Z3Context())
{
    var th = ctx.NewTheorem<NurseRoster>();

    // Domaine {0,1} pour les 9 variables d'affectation
    th = th.Where(t => t.A_G1>=0&&t.A_G1<=1 && t.A_G2>=0&&t.A_G2<=1 && t.A_G3>=0&&t.A_G3<=1
                    && t.B_G1>=0&&t.B_G1<=1 && t.B_G2>=0&&t.B_G2<=1 && t.B_G3>=0&&t.B_G3<=1
                    && t.C_G1>=0&&t.C_G1<=1 && t.C_G2>=0&&t.C_G2<=1 && t.C_G3>=0&&t.C_G3<=1);

    // HARD — couverture : exactement 1 infirmiere par garde
    th = th.Where(t => t.A_G1 + t.B_G1 + t.C_G1 == 1);  // garde G1
    th = th.Where(t => t.A_G2 + t.B_G2 + t.C_G2 == 1);  // garde G2
    th = th.Where(t => t.A_G3 + t.B_G3 + t.C_G3 == 1);  // garde G3

    // HARD — capacite : au plus 1 garde par infirmiere (pas de double-garde)
    th = th.Where(t => t.A_G1 + t.A_G2 + t.A_G3 <= 1);
    th = th.Where(t => t.B_G1 + t.B_G2 + t.B_G3 <= 1);
    th = th.Where(t => t.C_G1 + t.C_G2 + t.C_G3 <= 1);

    // SOFT — maximiser les preferences satisfaites :
    //   A veut G1, B veut G1, C veut G2
    var sol = th.Optimize(Optimization.Maximize,
        t => t.A_G1 + t.B_G1 + t.C_G2);

    // Infirmiere affectee a chaque garde (la premiere a 1 dans la colonne)
    string nG1 = sol.A_G1==1?"A":(sol.B_G1==1?"B":"C");
    string nG2 = sol.A_G2==1?"A":(sol.B_G2==1?"B":"C");
    string nG3 = sol.A_G3==1?"A":(sol.B_G3==1?"B":"C");
    int prefsSatisfaites = sol.A_G1 + sol.B_G1 + sol.C_G2;

    Console.WriteLine("Affectation optimale :");
    Console.WriteLine($"  Garde G1 -> infirmiere {nG1}");
    Console.WriteLine($"  Garde G2 -> infirmiere {nG2}");
    Console.WriteLine($"  Garde G3 -> infirmiere {nG3}");
    Console.WriteLine($"Preferences satisfaites : {prefsSatisfaites} / 3  (A voulait G1, B voulait G1, C voulait G2)");
    Console.WriteLine("Conflit A/B sur G1 : impossible de satisfaire les 3 -> le solveur arbitre (optimum = 2).");
}
Affectation optimale :
  Garde G1 -> infirmiere A
  Garde G2 -> infirmiere C
  Garde G3 -> infirmiere B
Preferences satisfaites : 2 / 3  (A voulait G1, B voulait G1, C voulait G2)
Conflit A/B sur G1 : impossible de satisfaire les 3 -> le solveur arbitre (optimum = 2).

Lecture : pourquoi MaxSAT fait la différence (Prong-B)

L’optimum trouvé est 2 préférences sur 3 — et c’est le mieux possible. Pourquoi ? A et B veulent toutes deux la garde G1, or une seule infirmière peut la prendre (contrainte dure de couverture). Le solveur en donne une à A (ou B), satisfait la préférence de C sur G2, et affecte la garde restante G3 à l’infirmière dont la préférence n’a pas pu être honorée. Aucune affectation ne peut dépasser 2 préférences satisfaites — le solveur le prouve par optimisation globale.

C’est exactement le terrain où l’optimisation SMT discrimine face à une approche naïve :

  • Un glouton « donner à chacun sa préférence » échoue dès la première étape (A et B en conflit sur G1) et doit reculer — sans stratégie globale, il peut aboutir à une affectation sous-optimale (1 préférence) au lieu de l’optimum (2).
  • Le solveur d’optimisation explore l’espace des affectations en tenant compte simultanément de toutes les contraintes dures et de l’objectif, et garantit l’optimum.

Sur cette instance (3×3 = 9 variables), c’est petit. Mais le même patron passe à l’échelle : 30 infirmières × 30 gardes avec disponibilités, compétences et préférences pondérées devient un weighted partial MaxSAT que le solveur traite en secondes — là où un backtracking manuel explose.

Points clés : - Les contraintes dures vont dans .Where(...) ; les préférences molles dans l’objectif .Optimize(...) — la distinction structurelle est explicite dans le code. - L’optimum est garanti global (le solveur explore tout l’espace, il ne s’arrête pas à la première solution faisable). - Quand les préférences sont pondérées (certaines comptent plus que d’autres), il suffit de pondérer l’objectif : t => 3*t.A_G1 + 1*t.B_G1 + 2*t.C_G2 — weighted MaxSAT, sans changer la structure.

B1 — Weighted MaxSAT explicite (DSL SoftWhere)

Le pattern .Optimize(Maximize, lambda_ponderee) cache la pondération dans une expression-objectif : on construit un lambda t => 3*t.A_G1 + 1*t.B_G1 + 2*t.C_G2 qui combine linéairement des contributions booléennes. C’est pratique, mais ça mélange deux choses — la nature pondérée de la contrainte (chaque préférence est un jugement indépendant) et la stratégie d’agrégation (ici une somme linéaire). Le binding Z3.Linq expose un cran plus bas via SoftWhere (Theorem{T}.cs:121) : on déclare chaque préférence comme une contrainte molle indépendante avec son poids et un groupe optionnel (les softs d’un même groupe sont agrégés en un seul objectif par Z3), et le routage vers MkOptimize + AssertSoft est automatique (cf Theorem.cs:141-149). Z3 minimise alors la somme des poids des contraintes molles violées — exactement la sémantique MaxRes du weighted MaxSAT canonique.

Stack : A + B — pourquoi. Ce bloc ouvre un deuxième volet “deux stacks” : pas pour exposer une théorie Z3 cachée (BitVectors, réels, UNSAT cores), mais pour révéler l’architecture de routage entre Solver (qui ignore les softs) et Optimize (qui les porte via AssertSoft). Le DSL SoftWhere est l’entrée qui déclenche ce routage ; le raw AssertSoft est l’appel Z3 qui le matérialise.

// B1 — Weighted MaxSAT "deux stacks" sur le meme probleme (3 infirmieres x 3 gardes)
// Preferences : A veut G1 (poids 3), B veut G1 (poids 1), C veut G2 (poids 2)
// Meme instance que la cellule 7 (unweighted), mais avec poids distincts.
// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : on manipule l'Optimize object directement
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    var opt = z3.MkOptimize();

    // Variables entieres {0,1} : A_Gi, B_Gi, C_Gi (alignement avec le pattern de NB-09)
    var A_G1 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("A_G1");
    var A_G2 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("A_G2");
    var A_G3 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("A_G3");
    var B_G1 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("B_G1");
    var B_G2 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("B_G2");
    var B_G3 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("B_G3");
    var C_G1 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("C_G1");
    var C_G2 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("C_G2");
    var C_G3 = (Microsoft.Z3.ArithExpr)z3.MkIntConst("C_G3");

    // Helper : assert (v >= 0) && (v <= 1)
    void Dom(Microsoft.Z3.ArithExpr v)
    {
        opt.Assert(z3.MkAnd(z3.MkGe(v, z3.MkInt(0)), z3.MkLe(v, z3.MkInt(1))));
    }
    Dom(A_G1); Dom(A_G2); Dom(A_G3); Dom(B_G1); Dom(B_G2); Dom(B_G3); Dom(C_G1); Dom(C_G2); Dom(C_G3);

    // HARD — couverture : exactement 1 infirmiere par garde
    opt.Assert(z3.MkEq(z3.MkAdd(A_G1, B_G1, C_G1), z3.MkInt(1)));
    opt.Assert(z3.MkEq(z3.MkAdd(A_G2, B_G2, C_G2), z3.MkInt(1)));
    opt.Assert(z3.MkEq(z3.MkAdd(A_G3, B_G3, C_G3), z3.MkInt(1)));

    // SOFT — preferences ponderees (AssertSoft : poids = penalite si violee)
    // La garde molle s'exprime comme "A_Gi == 1" — equivalente a (A_Gi != 0)
    opt.AssertSoft(z3.MkEq(A_G1, z3.MkInt(1)), 3, "preferences");  // A veut G1, poids 3 (le plus fort)
    opt.AssertSoft(z3.MkEq(B_G1, z3.MkInt(1)), 1, "preferences");  // B veut G1, poids 1
    opt.AssertSoft(z3.MkEq(C_G2, z3.MkInt(1)), 2, "preferences");  // C veut G2, poids 2

    var status = opt.Check();
    Console.WriteLine($"[RAW] Status : {status}");

    if (status == Microsoft.Z3.Status.SATISFIABLE)
    {
        var m = opt.Model;
        int vA_G1 = ((Microsoft.Z3.IntNum)m.Eval(A_G1, true)).Int;
        int vA_G2 = ((Microsoft.Z3.IntNum)m.Eval(A_G2, true)).Int;
        int vA_G3 = ((Microsoft.Z3.IntNum)m.Eval(A_G3, true)).Int;
        int vB_G1 = ((Microsoft.Z3.IntNum)m.Eval(B_G1, true)).Int;
        int vB_G2 = ((Microsoft.Z3.IntNum)m.Eval(B_G2, true)).Int;
        int vB_G3 = ((Microsoft.Z3.IntNum)m.Eval(B_G3, true)).Int;
        int vC_G1 = ((Microsoft.Z3.IntNum)m.Eval(C_G1, true)).Int;
        int vC_G2 = ((Microsoft.Z3.IntNum)m.Eval(C_G2, true)).Int;
        int vC_G3 = ((Microsoft.Z3.IntNum)m.Eval(C_G3, true)).Int;
        var gardeG1 = vA_G1==1 ? "A" : (vB_G1==1 ? "B" : "C");
        var gardeG2 = vA_G2==1 ? "A" : (vB_G2==1 ? "B" : "C");
        var gardeG3 = vA_G3==1 ? "A" : (vB_G3==1 ? "B" : "C");
        Console.WriteLine($"[RAW] Garde G1 -> {gardeG1}");
        Console.WriteLine($"[RAW] Garde G2 -> {gardeG2}");
        Console.WriteLine($"[RAW] Garde G3 -> {gardeG3}");
        Console.WriteLine("[RAW] A obtient G1 (poids 3 satisfait) — B perd G1 (poids 1 sacrifie)");
    }
}
Console.WriteLine();

public class NurseRosterB1
{
    public int A_G1=0, A_G2=0, A_G3=0;
    public int B_G1=0, B_G2=0, B_G3=0;
    public int C_G1=0, C_G2=0, C_G3=0;
}

// ============================================================
// BLOC DSL (Z3.Linq) : SoftWhere + Solve — meme semantique
// ============================================================
using (var ctx = new Z3Context())
{
    var th = ctx.NewTheorem<NurseRosterB1>();

    // Domaine {0,1} pour les 9 variables d'affectation
    th = th.Where(t => t.A_G1>=0&&t.A_G1<=1 && t.A_G2>=0&&t.A_G2<=1 && t.A_G3>=0&&t.A_G3<=1
                    && t.B_G1>=0&&t.B_G1<=1 && t.B_G2>=0&&t.B_G2<=1 && t.B_G3>=0&&t.B_G3<=1
                    && t.C_G1>=0&&t.C_G1<=1 && t.C_G2>=0&&t.C_G2<=1 && t.C_G3>=0&&t.C_G3<=1);

    // HARD — couverture (memes contraintes qu'au-dessus)
    th = th.Where(t => t.A_G1 + t.B_G1 + t.C_G1 == 1);
    th = th.Where(t => t.A_G2 + t.B_G2 + t.C_G2 == 1);
    th = th.Where(t => t.A_G3 + t.B_G3 + t.C_G3 == 1);

    // SOFT — chaque preference declaree separement avec son poids
    // Pas besoin de .Optimize() — le routage vers MkOptimize est AUTOMATIQUE
    // des qu'une soft constraint est presente (Theorem.cs:144).
    th = th.SoftWhere(t => t.A_G1 == 1, weight: 3);
    th = th.SoftWhere(t => t.B_G1 == 1, weight: 1);
    th = th.SoftWhere(t => t.C_G2 == 1, weight: 2);

    var sol = th.Solve();

    string nG1 = sol.A_G1==1?"A":(sol.B_G1==1?"B":"C");
    string nG2 = sol.A_G2==1?"A":(sol.B_G2==1?"B":"C");
    string nG3 = sol.A_G3==1?"A":(sol.B_G3==1?"B":"C");

    Console.WriteLine($"[DSL] Garde G1 -> {nG1}");
    Console.WriteLine($"[DSL] Garde G2 -> {nG2}");
    Console.WriteLine($"[DSL] Garde G3 -> {nG3}");
    Console.WriteLine("[DSL] Meme verdict que le raw : A obtient G1 (poids 3) > B (poids 1)");
}
Console.WriteLine();
Console.WriteLine("B1 OK : raw et DSL produisent la meme affectation (A sur G1), demontrant que");
Console.WriteLine("SoftWhere est bien l'equivalent DSL de AssertSoft (meme routage vers MkOptimize).");
[RAW] Status : SATISFIABLE
[RAW] Garde G1 -> A
[RAW] Garde G2 -> C
[RAW] Garde G3 -> A
[RAW] A obtient G1 (poids 3 satisfait) — B perd G1 (poids 1 sacrifie)

[DSL] Garde G1 -> A
[DSL] Garde G2 -> C
[DSL] Garde G3 -> A
[DSL] Meme verdict que le raw : A obtient G1 (poids 3) > B (poids 1)

B1 OK : raw et DSL produisent la meme affectation (A sur G1), demontrant que
SoftWhere est bien l'equivalent DSL de AssertSoft (meme routage vers MkOptimize).

Lecture B1 — pourquoi deux écritures du même problème

Les deux blocs résolvent exactement la même instance (3 infirmières × 3 gardes, mêmes contraintes dures, mêmes préférences pondérées) et arrivent au même verdict : A obtient G1 (poids 3) — son poids bat B (poids 1). La différence n’est pas sémantique, elle est architecturale :

Aspect RAW (MkOptimize + AssertSoft) DSL (th.SoftWhere + Solve)
Qui instancie l’Optimize L’utilisateur (var solver = z3.MkOptimize()) Le binding automatiquement (Theorem.cs:144)
Qui traduit la lambda t => ... Pas de lambda : on construit le BoolExpr à la main Le ExpressionVisitor du binding
Visibilité des poids Explicite : AssertSoft(expr, weight: 3, group: "...") Explicite aussi : SoftWhere(constraint, weight: 3)
Granularité de modification On peut ajouter/retirer des AssertSoft à la volée entre Check() Idem (chaque SoftWhere retourne un nouveau Theorem<T>)
Verbosity de nombreuses lignes de boilerplate quelques lignes

Ligne de contraste (à retenir) : le DSL cache l’objet Optimize et déclenche le routage automatique (cf Theorem.cs:144 if (softConstraints.Any())) — le raw expose l’objet pour un contrôle direct (groupes, vérifications incrémentales). Même sémantique Z3 (AssertSoft apparaît dans les deux), deux niveaux d’abstraction différents.

Cas d’usage : on préfère le DSL SoftWhere par défaut (lisibilité, chaînable avec .Where); on bascule en raw quand on doit inspecter le modèle entre deux assertions, partager un Optimize entre sous-problèmes, ou désactiver temporairement certaines contraintes molles (le DSL SoftWhere ajoute toujours, jamais ne retire).

B3 — Somme variadique (DSL Z3Methods.Sum)

Le sac à dos de la cellule 4 déroule à la main sa contrainte de capacité et son objectif : 4*t.x0 + 5*t.x1 + 6*t.x2 + 3*t.x3 + 2*t.x4. Ça passe pour 5 objets ; à 20 ou 50 objets ce déroulage devient illisible et fragile (une faute de copier-coller par terme). Le visiteur Z3.Linq ne connaît nativement que le + binaire (repli pairwise a + b) — il n’a aucun moyen de replier une liste de longueur arbitraire. C’est le trou que comble Z3Methods.Sum (Z3Methods.cs:37) : une méthode magique variadique qui prend un params T[] (littéral new[]{...} ou collection matérialisée via Select(...).ToArray()) et se traduit en un unique MkAdd sur tous les termes (cf ExpressionVisitor.cs:482).

Stack : A + B — pourquoi. Ce bloc « deux stacks » ne révèle pas une théorie Z3 cachée : MkAdd est déjà variadique côté API brute. Ce que B3 révèle, c’est le pont d’agrégation entre une collection C# et un terme SMT unique — le DSL Sum est l’entrée LINQ qui déclenche le repli, le raw MkAdd(ArithExpr[]) est l’appel Z3 qui le matérialise. Sans Sum, la lambda du DSL est condamnée au déroulage terme-à-terme.

// B3 — Somme variadique "deux stacks" sur le meme sac a dos (5 objets, capacite 10)
// poids {4,5,6,3,2}, valeur {10,15,16,7,5} — meme instance que la cellule 4.
// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : MkAdd variadique construit A LA MAIN
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    var opt = z3.MkOptimize();

    int[] poidsR  = { 4, 5, 6, 3, 2 };
    int[] valeurR = { 10, 15, 16, 7, 5 };
    int WR = 10;

    // Une variable entiere {0,1} par objet
    var x = new Microsoft.Z3.ArithExpr[5];
    for (int i = 0; i < 5; i++)
    {
        x[i] = (Microsoft.Z3.ArithExpr)z3.MkIntConst("x" + i);
        opt.Assert(z3.MkAnd(z3.MkGe(x[i], z3.MkInt(0)), z3.MkLe(x[i], z3.MkInt(1))));
    }

    // Capacite : on replie A LA MAIN les 5 termes ponderes dans un tableau, puis MkAdd
    var termesPoids = new Microsoft.Z3.ArithExpr[5];
    for (int i = 0; i < 5; i++) termesPoids[i] = (Microsoft.Z3.ArithExpr)z3.MkMul(z3.MkInt(poidsR[i]), x[i]);
    opt.Assert(z3.MkLe(z3.MkAdd(termesPoids), z3.MkInt(WR)));

    // Objectif : maximiser la somme ponderee des valeurs (meme repli manuel)
    var termesValeur = new Microsoft.Z3.ArithExpr[5];
    for (int i = 0; i < 5; i++) termesValeur[i] = (Microsoft.Z3.ArithExpr)z3.MkMul(z3.MkInt(valeurR[i]), x[i]);
    opt.MkMaximize(z3.MkAdd(termesValeur));

    var status = opt.Check();
    Console.WriteLine($"[RAW] Status : {status}");
    if (status == Microsoft.Z3.Status.SATISFIABLE)
    {
        var m = opt.Model;
        var pris = new int[5];
        for (int i = 0; i < 5; i++) pris[i] = ((Microsoft.Z3.IntNum)m.Eval(x[i], true)).Int;
        int poidsTot = 0, valeurTot = 0;
        for (int i = 0; i < 5; i++) { poidsTot += poidsR[i] * pris[i]; valeurTot += valeurR[i] * pris[i]; }
        Console.WriteLine("[RAW] Objets pris (1=pris) : " + string.Join(", ", pris));
        Console.WriteLine($"[RAW] Poids {poidsTot} / {WR} — Valeur optimale {valeurTot}");
    }
}
Console.WriteLine();

public class KnapsackB3
{
    public int x0 = 0, x1 = 0, x2 = 0, x3 = 0, x4 = 0;  // 1 si l'objet i est pris
}

// ============================================================
// BLOC DSL (Z3.Linq) : Z3Methods.Sum remplace le deroulage manuel
// ============================================================
using (var ctx = new Z3Context())
{
    var th = ctx.NewTheorem<KnapsackB3>();

    th = th.Where(t => t.x0>=0&&t.x0<=1 && t.x1>=0&&t.x1<=1 && t.x2>=0&&t.x2<=1 && t.x3>=0&&t.x3<=1 && t.x4>=0&&t.x4<=1);

    // Capacite : UNE ligne — Sum replie les 5 termes ponderes en un seul MkAdd
    th = th.Where(t => Z3Methods.Sum(new[]{ 4*t.x0, 5*t.x1, 6*t.x2, 3*t.x3, 2*t.x4 }) <= 10);

    // Objectif : idem, Sum sur les valeurs
    var sol = th.Optimize(Optimization.Maximize, t => Z3Methods.Sum(new[]{ 10*t.x0, 15*t.x1, 16*t.x2, 7*t.x3, 5*t.x4 }));

    int[] prisD = { sol.x0, sol.x1, sol.x2, sol.x3, sol.x4 };
    int poidsD  = 4*sol.x0 + 5*sol.x1 + 6*sol.x2 + 3*sol.x3 + 2*sol.x4;
    int valeurD = 10*sol.x0 + 15*sol.x1 + 16*sol.x2 + 7*sol.x3 + 5*sol.x4;
    Console.WriteLine("[DSL] Objets pris (1=pris) : " + string.Join(", ", prisD));
    Console.WriteLine($"[DSL] Poids {poidsD} / 10 — Valeur optimale {valeurD}");
}
Console.WriteLine();
Console.WriteLine("B3 OK : raw (MkAdd manuel sur tableau) et DSL (Z3Methods.Sum) trouvent le meme optimum.");
Console.WriteLine("Le DSL supprime le deroulage terme-a-terme que le + binaire du visiteur imposerait.");
[RAW] Status : SATISFIABLE
[RAW] Objets pris (1=pris) : 0, 1, 0, 1, 1
[RAW] Poids 10 / 10 — Valeur optimale 27

[DSL] Objets pris (1=pris) : 0, 1, 0, 1, 1
[DSL] Poids 10 / 10 — Valeur optimale 27

B3 OK : raw (MkAdd manuel sur tableau) et DSL (Z3Methods.Sum) trouvent le meme optimum.
Le DSL supprime le deroulage terme-a-terme que le + binaire du visiteur imposerait.

Lecture B3 — pourquoi deux écritures de la même somme

Les deux blocs résolvent le même sac à dos (5 objets, capacité 10) et trouvent le même optimum. La différence tient à l’expression de la somme pondérée :

Aspect RAW (z3.MkAdd(ArithExpr[])) DSL (Z3Methods.Sum(new[]{...}))
Construction des termes Boucle explicite MkMul(poids[i], x[i]) dans un tableau Directement dans la lambda t => ...
Repli en somme z3.MkAdd(termes) (API brute déjà variadique) Z3Methods.Sum(...) → visiteur → MkAdd
Longueur variable Naturelle (on remplit le tableau) Naturelle (new[]{...} littéral ou Select(...).ToArray())
Sans B3 côté DSL — Déroulage manuel 4*x0 + 5*x1 + ... (le + du visiteur ne replie que deux opérandes)
Lisibilité à N objets Boilerplate MkIntConst/MkMul/Eval lisible même à 50 termes

Ligne de contraste (à retenir) : le + du visiteur ne replie que deux opérandes ; Z3Methods.Sum replie une liste entière en un seul MkAdd — c’est le pont manquant entre une collection C# et un terme SMT. Même sémantique Z3 (MkAdd dans les deux blocs), mais le DSL supprime le déroulage manuel que le + binaire imposerait.

Cas d’usage : dès qu’une contrainte agrège un nombre variable de contributions (somme d’indicateurs sum_i Sel[i]*coût[i], charge d’un bin, total d’une ligne Sudoku), Sum évite le déroulage. Sur la forme Select(...).ToArray(), la collection source est évaluée dans l’hôte (host-evaluable) puis chaque élément substitué — on peut donc sommer sur Enumerable.Range(0, n) sans écrire les n termes à la main.

Exercices

Les trois exercices vous font réutiliser l’API .Optimize() sur de nouvelles instances d’optimisation. Chaque exercice suit le squelette : définir la classe de variables, ajouter domaine + contraintes dures (.Where), puis appeler .Optimize avec un objectif.

Rappel C.1 : les stubs ne lèvent jamais d’erreur — Console.WriteLine("Exercice à compléter"). Le notebook s’exécute de bout en bout même exercices non résolus.

Exercice 1 — Sac à dos avec 6 objets

Reprenez le sac à dos de la cellule 4 mais avec 6 objets : poids [6, 3, 4, 2, 5, 7], valeurs [12, 5, 8, 3, 10, 14], capacité W = 15. Définissez la classe Knapsack6 (6 variables {0,1}), ajoutez la contrainte de capacité, et maximisez la valeur. Quel est l’optimum ?

Indice : il y a \(2^6 = 64\) sous-ensembles — énumérable à la main, mais le solveur le trouve sans énumération explicite.

// Exercice 1 : sac a dos 6 objets
// TODO etudiant :
// 1. Classe Knapsack6 { x0..x5 } (int), domaine {0,1}
// 2. Contrainte : 6*x0 + 3*x1 + 4*x2 + 2*x3 + 5*x4 + 7*x5 <= 15
// 3. Objectif : Optimize(Maximize, t => 12*x0 + 5*x1 + 8*x2 + 3*x3 + 10*x4 + 14*x5)
Console.WriteLine("Exercice 1 a completer : sac a dos 6 objets, maximiser la valeur sous capacite 15");
Exercice 1 a completer : sac a dos 6 objets, maximiser la valeur sous capacite 15

Exercice 2 — Minimisation (coût de transport)

Trois entrepôts approvisionnent un client. Chaque entrepôt a un coût unitaire de livraison et une capacité : entropôt 1 (coût 4, capacité 50), entropôt 2 (coût 6, capacité 80), entropôt 3 (coût 3, capacité 30). Le client demande 100 unités. Minimisez le coût total de livraison.

Étapes : 3 variables entières (quantités, domaines 0..capacité), contrainte q1+q2+q3 == 100, objectif Optimize(Minimize, t => 4*t.q1 + 6*t.q2 + 3*t.q3).

// Exercice 2 : minimisation cout de transport (LP entier)
// TODO etudiant :
// 1. Classe Transport { q1, q2, q3 } (int), domaines 0..50, 0..80, 0..30
// 2. Contrainte : t.q1 + t.q2 + t.q3 == 100
// 3. Objectif : Optimize(Minimize, t => 4*t.q1 + 6*t.q2 + 3*t.q3)
Console.WriteLine("Exercice 2 a completer : minimiser le cout de transport (4/6/3 par entropot, demande 100)");
Exercice 2 a completer : minimiser le cout de transport (4/6/3 par entropot, demande 100)

Exercice 3 — Weighted MaxSAT (préférences pondérées)

Reprenez le roulement d’infirmières de la cellule 7, mais avec des préférences pondérées : A veut G1 avec un poids 3, B veut G1 avec un poids 1, C veut G2 avec un poids 2. Maximisez la somme pondérée. L’affectation optimale change-t-elle par rapport à la cellule 7 (où toutes les préférences comptaient equally) ?

Question subsidiaire : avec ces poids, quel est l’optimum pondéré, et quelle infirmière obtient G1 ?

// Exercice 3 : weighted MaxSAT (preferences ponderees)
// TODO etudiant :
// 1. Reprendre NurseRoster (9 vars {0,1}, memes contraintes dures)
// 2. Objectif pondere : Optimize(Maximize, t => 3*t.A_G1 + 1*t.B_G1 + 2*t.C_G2)
Console.WriteLine("Exercice 3 a completer : weighted MaxSAT, ponderer les preferences (A=3, B=1, C=2)");
Exercice 3 a completer : weighted MaxSAT, ponderer les preferences (A=3, B=1, C=2)

Conclusion

Ce notebook comble le gap d’optimisation de la série Z3.Linq : là où les dix premiers notebooks posaient des problèmes de satisfiabilité (.Solve()), on introduit ici l’optimisation (.Optimize()) sur deux terrains complémentaires :

  • Sac à dos (knapsack) : un objectif quantitatif à maximiser sous contrainte de capacité — l’optimisation entière la plus canonique.
  • Roulement d’infirmières (nurse rostering) : le paradigme MaxSAT — des contraintes dures (couverture, capacité) dans .Where(...), des préférences molles dans l’objectif, avec conflits arbitrés globalement par le solveur.

Points clés : - .Optimize(Optimization.Maximize/Minimize, lambda) ou la syntaxe LINQ orderby/orderby descending — le binding traduit l’objectif en assertions maximize/minimize Z3. - L’optimum est garanti global : le solveur explore l’espace complet, il ne renvoie pas la première solution faisable. - La distinction dur vs mou est explicite dans le code : .Where(...) pour l’impératif, l’objectif pour le souhaitable — c’est ce qui rend la modélisation MaxSAT lisible et maintenable. - Le weighted MaxSAT (préférences pondérées) s’obtient gratuitement en pondérant l’objectif, sans changer la structure du modèle.

Référence : le MaxSAT est le cadre standard pour l’optimisation sous contraintes booléennes ; Z3 implémente les algorithmes state-of-the-art (MaxRes, OLL) pour le résoudre. Le nurse rostering en est l’application canonique en recherche opérationnelle.

Retour au sommet