Notebook 06 — Meal-Planner declaratif : du modèle Z3 au plan hebdomadaire visualise

Navigation : Index Z3 | Index SymbolicAI | Index general | Notebook précédent (Nested Arrays)

Ce notebook consolide en une seule histoire coherente la modelisation declarative d’un planificateur de repas avec Z3.Linq et l’API Microsoft.Z3, du menu d’un jour au plan hebdomadaire visualise. Il est organise en trois parties :

Le corpus nutritionnel detaille (RecipeML x Ciqual, quantites en grammes) est prepare dans le notebook de données 07 ; ici on se concentre sur la modelisation et sa restitution.

flowchart LR
    A["Partie A\nModele declaratif\n(index / bool / int[][])"] --> B["Partie B\nCouplage hebdomadaire\n(fenêtre kcal/jour, variete)"]
    B --> C["Partie C\nVisualisation HTML\n(cartes, grille, Pareto)"]
    %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
    style A fill:#cfe3ff,color:#004085
    style B fill:#ffe9c7,color:#856404
    style C fill:#c8f7c5,color:#1b5e20
#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 Microsoft.DotNet.Interactive;
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Text;
using System.Xml.Linq;
Console.WriteLine("Imports OK : Z3.Linq (.deploy, CollectionHandling cable), Microsoft.Z3, Microsoft.DotNet.Interactive (display/HTML), System.Linq/Text/Xml.Linq/Diagnostics");
Imports OK : Z3.Linq (.deploy, CollectionHandling cable), Microsoft.Z3, Microsoft.DotNet.Interactive (display/HTML), System.Linq/Text/Xml.Linq/Diagnostics

Partie A — Modelisation declarative

Cette partie construit le modele Z3 pas a pas : de la selection simple (sections 1-6) au plan hebdomadaire en tableau imbrique (section 7). Les approfondissements techniques — interpretation approfondie du plan int[][], forensic CollectionHandling, tableau synthetique — sont regroupes en Annexes A-C en fin de carnet, pour garder ici le fil de la demonstration.

1. Contexte : Le théorème hiérarchique

Dans les notebooks précédents, nous avons utilisé Symbols<T1, T2, ...> pour créer des variables Z3 plates. Le théorème hiérarchique generalise cette approche :

  • Un objet parent (ex: Meal) contient des references vers des objets enfants (ex: Course)
  • Chaque niveau de la hiérarchie possède ses propres contraintes
  • Le solveur Z3 résout le système complet de manière cohérente

Analogie

Meal (contraintes globales : calories totales, budget)
  |-- Entree (contraintes : type, taille)
  |-- Plat principal (contraintes : proteines minimales)
  |-- Dessert (contraintes : sucre maximal)

La fusion de données consiste a injecter des données externes (table nutritionnelle) dans les contraintes du solveur.

2. Base de données nutritionnelle (data fusion)

Nous definissons une base de données d’aliments avec leurs propriétés nutritionnelles. Ces données seront utilisees par le solveur pour sélectionner des combinaisons valides.

// Base de données nutritionnelle : fusion de données statiques avec le solveur
public class FoodItem
{
    public string Name { get; set; }
    public int Calories { get; set; }      // kcal par portion
    public int Protein { get; set; }       // grammes
    public int Carbs { get; set; }         // grammes
    public int Fat { get; set; }           // grammes
    public int Cost { get; set; }          // prix en centimes
    public string Category { get; set; }   // entree, plat, dessert
}

var foodDatabase = new List<FoodItem>
{
    // Entrees
    new FoodItem { Name = "Salade verte",    Calories = 80,  Protein = 2,  Carbs = 8,   Fat = 4,  Cost = 300, Category = "entree" },
    new FoodItem { Name = "Soupe de legumes", Calories = 120, Protein = 4,  Carbs = 18,  Fat = 3,  Cost = 250, Category = "entree" },
    new FoodItem { Name = "Carpaccio",        Calories = 150, Protein = 15, Carbs = 2,   Fat = 8,  Cost = 600, Category = "entree" },
    // Plats principaux
    new FoodItem { Name = "Poulet roti",      Calories = 350, Protein = 30, Carbs = 5,   Fat = 20, Cost = 500, Category = "plat" },
    new FoodItem { Name = "Saumon grille",    Calories = 300, Protein = 28, Carbs = 0,   Fat = 18, Cost = 800, Category = "plat" },
    new FoodItem { Name = "Pates bolognaise", Calories = 450, Protein = 18, Carbs = 55,  Fat = 14, Cost = 350, Category = "plat" },
    new FoodItem { Name = "Risotto",          Calories = 400, Protein = 10, Carbs = 60,  Fat = 12, Cost = 400, Category = "plat" },
    // Desserts
    new FoodItem { Name = "Fruit frais",      Calories = 70,  Protein = 1,  Carbs = 15,  Fat = 0,  Cost = 200, Category = "dessert" },
    new FoodItem { Name = "Mousse au chocolat",Calories = 250, Protein = 4,  Carbs = 28,  Fat = 14, Cost = 350, Category = "dessert" },
    new FoodItem { Name = "Yaourt nature",    Calories = 60,  Protein = 5,  Carbs = 6,   Fat = 2,  Cost = 150, Category = "dessert" },
};

Console.WriteLine($"Base de données chargée : {foodDatabase.Count} aliments");
Console.WriteLine(string.Join("\n", foodDatabase.GroupBy(f => f.Category)
    .Select(g => $"  {g.Key} : {g.Count()} items")));
Base de données chargée : 10 aliments
  entree : 3 items
  plat : 4 items
  dessert : 3 items

Interpretation

La base contient 10 aliments répartis en 3 catégories (entree, plat, dessert). Chaque aliment a des propriétés nutritionnelles et un cout. Le solveur devra sélectionner exactement 1 entree + 1 plat + 1 dessert qui satisfont les contraintes globales.

3. Approche 1 : Sélection par index avec contraintes lineaires

La première approche utilisé des variables entieres pour sélectionner un aliment dans chaque catégorie. Les contraintes sont exprimees lineairement en fonction de l’index.

// Approche index-based : chaque variable represente l'index d'un aliment
// Les contraintes Z3.Linq doivent utiliser des expressions lineaires sur les variables

var entrees = foodDatabase.Where(f => f.Category == "entree").ToList();
var plats = foodDatabase.Where(f => f.Category == "plat").ToList();
var desserts = foodDatabase.Where(f => f.Category == "dessert").ToList();

using (var ctx = new Z3Context())
{
    // Variables : index de l'aliment choisi dans chaque catégorie
    // Contraintes de bornes avec expressions lineaires (pattern Z3.Linq)
    var theorem = from meal in ctx.NewTheorem<Symbols<int, int, int>>()
        where meal.X1 >= 0 && meal.X1 - 3 <= 0   // 0 <= X1 <= 2 (3 entrees)
        where meal.X2 >= 0 && meal.X2 - 4 <= 0   // 0 <= X2 <= 3 (4 plats)
        where meal.X3 >= 0 && meal.X3 - 3 <= 0   // 0 <= X3 <= 2 (3 desserts)
        select meal;

    var solution = theorem.Solve();
    
    if (solution != null)
    {
        var e = entrees[solution.X1];
        var p = plats[solution.X2];
        var d = desserts[solution.X3];
        int totalCal = e.Calories + p.Calories + d.Calories;
        int totalCost = e.Cost + p.Cost + d.Cost;
        
        Console.WriteLine("Menu trouve (sans contraintes nutritionnelles) :");
        Console.WriteLine($"  Entree  : {e.Name} ({e.Calories} kcal)");
        Console.WriteLine($"  Plat    : {p.Name} ({p.Calories} kcal)");
        Console.WriteLine($"  Dessert : {d.Name} ({d.Calories} kcal)");
        Console.WriteLine($"  Total   : {totalCal} kcal, {totalCost/100.0:F2} euros");
    }
    else
    {
        Console.WriteLine("Aucune solution trouvee");
    }
}
Menu trouve (sans contraintes nutritionnelles) :
  Entree  : Salade verte (80 kcal)
  Plat    : Poulet roti (350 kcal)
  Dessert : Fruit frais (70 kcal)
  Total   : 500 kcal, 10,00 euros

Interpretation

Sans contraintes nutritionnelles, le solveur trouve la première combinaison valide (index 0, 0, 0). Le résultat est trivialement la première entree, le premier plat et le premier dessert de la base. Nous devons ajouter des contraintes pour obtenir un menu équilibré.

4. Approche 2 : Contraintes nutritionnelles avec énumération

La contrainte Z3.Linq fonctionne avec des expressions lineaires. Pour injecter les données nutritionnelles, nous énumérons les combinaisons possibles et posons des contraintes sur les totaux.

Stratégie : generer toutes les combinaisons possibles, puis filtrer avec Z3 sur les contraintes globales (calories, proteines, budget).

// Approche par énumération + filtrage Z3
// Objectif : trouver un menu avec 600-900 kcal, >= 25g proteines, cout <= 12 euros

int minCalories = 600, maxCalories = 900;
int minProtein = 25;
int maxCostCents = 1200; // 12 euros

var validMenus = new List<string>();

// Énumération des combinaisons + vérification des contraintes
foreach (var e in entrees)
    foreach (var p in plats)
        foreach (var d in desserts)
        {
            int cal = e.Calories + p.Calories + d.Calories;
            int prot = e.Protein + p.Protein + d.Protein;
            int cost = e.Cost + p.Cost + d.Cost;
            
            if (cal >= minCalories && cal <= maxCalories 
                && prot >= minProtein && cost <= maxCostCents)
            {
                validMenus.Add($"{e.Name} + {p.Name} + {d.Name} = {cal} kcal, {prot}g prot, {cost/100.0:F2} EUR");
            }
        }

Console.WriteLine($"Menus valides (600-900 kcal, >= 25g prot, <= 12 EUR) : {validMenus.Count}/{entrees.Count * plats.Count * desserts.Count} combinaisons");
Console.WriteLine();
foreach (var menu in validMenus.Take(8))
    Console.WriteLine($"  {menu}");
if (validMenus.Count > 8)
    Console.WriteLine($"  ... et {validMenus.Count - 8} autres");
Menus valides (600-900 kcal, >= 25g prot, <= 12 EUR) : 8/36 combinaisons

  Salade verte + Poulet roti + Mousse au chocolat = 680 kcal, 36g prot, 11,50 EUR
  Soupe de legumes + Poulet roti + Mousse au chocolat = 720 kcal, 38g prot, 11,00 EUR
  Soupe de legumes + Pates bolognaise + Mousse au chocolat = 820 kcal, 26g prot, 9,50 EUR
  Soupe de legumes + Pates bolognaise + Yaourt nature = 630 kcal, 27g prot, 7,50 EUR
  Carpaccio + Pates bolognaise + Fruit frais = 670 kcal, 34g prot, 11,50 EUR
  Carpaccio + Pates bolognaise + Yaourt nature = 660 kcal, 38g prot, 11,00 EUR
  Carpaccio + Risotto + Fruit frais = 620 kcal, 26g prot, 12,00 EUR
  Carpaccio + Risotto + Yaourt nature = 610 kcal, 30g prot, 11,50 EUR

Interpretation

L’énumération exhaustive fonctionne car l’espace est petit (3 x 4 x 3 = 36 combinaisons). Pour de grands catalogues, le solveur Z3 est préférable car il explore intelligemment l’espace de recherche plutôt que de tout énumérer.

5. Approche 3 : Modèle Z3 avec variables booléennes (sélection)

Pour modéliser la sélection d’aliments directement dans Z3, nous utilisons des variables booléennes : chaque aliment est soit sélectionné (true) soit non sélectionné (false).

Principe

  • Une variable booléenne par aliment
  • Exactement 1 entree + 1 plat + 1 dessert sélectionnés
  • Contraintes nutritionnelles sur la somme ponderee
// Approche booléenne Z3 : chaque aliment est une variable bool
// Avantage : le solveur explore l'espace, pas d'énumération

using (var z3ctx = new Context())
{
    var solver = z3ctx.MkSolver();
    
    // Variables booléennes : une par aliment
    var selections = foodDatabase
        .Select((food, i) => new { Food = food, Var = (BoolExpr)z3ctx.MkConst($"sel_{i}_{food.Name}", z3ctx.BoolSort) })
        .ToList();
    
    // Contrainte 1 : exactement 1 entree sélectionnée
    var entreeVars = selections.Where(s => s.Food.Category == "entree").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(entreeVars));           // au moins 1
    foreach (var v1 in entreeVars)                 // au plus 1 (pairwise exclusion)
        foreach (var v2 in entreeVars)
            if (v1 != v2)
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    // Contrainte 2 : exactement 1 plat sélectionné
    var platVars = selections.Where(s => s.Food.Category == "plat").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(platVars));
    foreach (var v1 in platVars)
        foreach (var v2 in platVars)
            if (v1 != v2)
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    // Contrainte 3 : exactement 1 dessert sélectionné
    var dessertVars = selections.Where(s => s.Food.Category == "dessert").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(dessertVars));
    foreach (var v1 in dessertVars)
        foreach (var v2 in dessertVars)
            if (v1 != v2)
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    // Contraintes nutritionnelles lineaires (implication conditionnelle)
    IntExpr totalCal = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Calories), z3ctx.MkInt(0))));
    
    IntExpr totalProt = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Protein), z3ctx.MkInt(0))));
    
    IntExpr totalCost = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Cost), z3ctx.MkInt(0))));
    
    solver.Add(z3ctx.MkGe(totalCal, z3ctx.MkInt(600)));
    solver.Add(z3ctx.MkLe(totalCal, z3ctx.MkInt(900)));
    solver.Add(z3ctx.MkGe(totalProt, z3ctx.MkInt(25)));
    solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(1200)));
    
    Console.WriteLine($"Contraintes : {solver.NumAssertions} assertions");
    
    var result = solver.Check();
    Console.WriteLine($"Résultat solve : {result}");
    
    if (result == Status.SATISFIABLE)
    {
        var model = solver.Model;
        Console.WriteLine("\nMenu équilibré trouve :");
        int cal = 0, prot = 0, cost = 0;
        foreach (var s in selections)
        {
            var val = model.Eval(s.Var, true);
            if (val.BoolValue == Z3_lbool.Z3_L_TRUE)
            {
                Console.WriteLine($"  [{s.Food.Category}] {s.Food.Name} : {s.Food.Calories} kcal, {s.Food.Protein}g prot, {s.Food.Cost/100.0:F2} EUR");
                cal += s.Food.Calories;
                prot += s.Food.Protein;
                cost += s.Food.Cost;
            }
        }
        Console.WriteLine($"  --- Total : {cal} kcal, {prot}g proteines, {cost/100.0:F2} EUR ---");
    }
    else
    {
        Console.WriteLine("Aucun menu ne satisfait les contraintes.");
    }
}
Contraintes : 31 assertions
Résultat solve : SATISFIABLE

Menu équilibré trouve :
  [entree] Soupe de legumes : 120 kcal, 4g prot, 2,50 EUR
  [plat] Pates bolognaise : 450 kcal, 18g prot, 3,50 EUR
  [dessert] Mousse au chocolat : 250 kcal, 4g prot, 3,50 EUR
  --- Total : 820 kcal, 26g proteines, 9,50 EUR ---

Interpretation

L’approche booléenne utilisé MkITE (If-Then-Else) pour conditionnellement ajouter la contribution nutritionnelle de chaque aliment. C’est la clé technique de la data fusion : les données statiques (calories, proteines, cout) sont injectees dans les expressions Z3 via MkITE.

Technique Rôle
BoolExpr par aliment Sélection binaire
MkOr + exclusion mutuelle Exactement 1 par catégorie
MkITE(sel, valeur, 0) Contribution conditionnelle
Somme des MkITE Total nutritionnel global

6. Optimisation : menu le moins cher (dichotomie)

Le solveur Z3 (MkSolver) trouve une solution satisfaisante, mais pas forcement optimale. Pour trouver le menu le moins cher, nous utilisons une recherche par dichotomie :

  1. On fixe une borne superieure sur le cout
  2. On demande au solveur s’il existe un menu dans ce budget
  3. Si oui, on essaie un budget plus faible ; si non, on augmente
  4. On répète jusqu’a trouver le minimum exact

Cette technique (binary search on objective) est un pattern classique en optimisation par solveur SAT/SMT.

// Optimisation : trouver le menu équilibré le MOINS CHER
// On utilisé le solver avec exploration itérative : on ajoute une contrainte
// de cout de plus en plus strict jusqu'a ce que le probleme devienne UNSAT

using (var z3ctx = new Context())
{
    var solver = z3ctx.MkSolver();
    
    // Variables booléennes
    var selections = foodDatabase
        .Select((food, i) => new { Food = food, Var = (BoolExpr)z3ctx.MkConst($"sel_{i}_{food.Name}", z3ctx.BoolSort) })
        .ToList();
    
    // Exactement 1 par catégorie
    var entreeVars = selections.Where(s => s.Food.Category == "entree").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(entreeVars));
    foreach (var v1 in entreeVars)
        foreach (var v2 in entreeVars)
            if (!v1.Equals(v2))
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    var platVars = selections.Where(s => s.Food.Category == "plat").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(platVars));
    foreach (var v1 in platVars)
        foreach (var v2 in platVars)
            if (!v1.Equals(v2))
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    var dessertVars = selections.Where(s => s.Food.Category == "dessert").Select(s => (BoolExpr)s.Var).ToArray();
    solver.Add(z3ctx.MkOr(dessertVars));
    foreach (var v1 in dessertVars)
        foreach (var v2 in dessertVars)
            if (!v1.Equals(v2))
                solver.Add(z3ctx.MkImplies(v1, z3ctx.MkNot(v2)));
    
    // Contraintes nutritionnelles
    IntExpr totalCal = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Calories), z3ctx.MkInt(0))));
    IntExpr totalProt = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Protein), z3ctx.MkInt(0))));
    IntExpr totalCost = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0), 
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Food.Cost), z3ctx.MkInt(0))));
    
    solver.Add(z3ctx.MkGe(totalCal, z3ctx.MkInt(600)));
    solver.Add(z3ctx.MkLe(totalCal, z3ctx.MkInt(900)));
    solver.Add(z3ctx.MkGe(totalProt, z3ctx.MkInt(25)));
    solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(1200)));
    
    // Recherche du cout minimum par dichotomie
    int lo = 0, hi = 1200, bestCost = -1;
    Status bestResult = Status.UNSATISFIABLE;
    
    while (lo <= hi)
    {
        solver.Push();
        int mid = (lo + hi) / 2;
        solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(mid)));
        var r = solver.Check();
        solver.Pop();
        
        if (r == Status.SATISFIABLE)
        {
            bestCost = mid;
            bestResult = r;
            hi = mid - 1;  // essayer moins cher
        }
        else
        {
            lo = mid + 1;  // besoin de plus de budget
        }
    }
    
    // Résoudre avec le meilleur cout trouve
    solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(bestCost)));
    var result = solver.Check();
    Console.WriteLine($"Optimisation (dichotomie) : cout minimum = {bestCost/100.0:F2} EUR, résultat = {result}");
    
    if (result == Status.SATISFIABLE)
    {
        var model = solver.Model;
        Console.WriteLine("\nMenu optimal (cout minimum) :");
        int cal = 0, prot = 0, cost = 0;
        foreach (var s in selections)
        {
            var val = model.Eval(s.Var, true);
            if (val.BoolValue == Z3_lbool.Z3_L_TRUE)
            {
                Console.WriteLine($"  [{s.Food.Category}] {s.Food.Name} : {s.Food.Calories} kcal, {s.Food.Protein}g prot, {s.Food.Cost/100.0:F2} EUR");
                cal += s.Food.Calories;
                prot += s.Food.Protein;
                cost += s.Food.Cost;
            }
        }
        Console.WriteLine($"  === Total : {cal} kcal, {prot}g proteines, {cost/100.0:F2} EUR ===");
    }
    else
    {
        Console.WriteLine("Aucun menu optimal trouve.");
    }
}
Optimisation (dichotomie) : cout minimum = 7,50 EUR, résultat = SATISFIABLE

Menu optimal (cout minimum) :
  [entree] Soupe de legumes : 120 kcal, 4g prot, 2,50 EUR
  [plat] Pates bolognaise : 450 kcal, 18g prot, 3,50 EUR
  [dessert] Yaourt nature : 60 kcal, 5g prot, 1,50 EUR
  === Total : 630 kcal, 27g proteines, 7,50 EUR ===

Interpretation

La dichotomie sur le cout est un pattern classique en optimisation SAT/SMT. Plutôt que d’utiliser MkOptimizer (qui peut etre instable dans certains bindings), on utilisé solver.Push()/solver.Pop() pour tester différentes bornes de cout sans reconstruire le solver a chaque fois.

Aspect Solve simple Dichotomie
Objectif Première solution Solution optimale
Cout Arbitraire Minimum garanti
Appels solver 1 O(log(budget_max))
Stabilite Toujours Toujours

7. Théorème hiérarchique : plan hebdomadaire en int[][]

Jusqu’ici, nous avons manipulé des variables plates. Pour planifier plusieurs repas simultanément — un plan sur N jours —, l’abstraction naturelle est un tableau imbriqué : une ligne par jour, une colonne par créneau (entrée, plat, dessert). C’est précisément ce que le fork Z3.Linq résout via le théorème hiérarchique sur int[][].

Chaque cellule est un entier = index d’un aliment. Les aliments étant groupés par catégorie dans foodDatabase (entrées, puis plats, puis desserts), on impose des bornes d’index par créneau pour forcer la bonne catégorie.

La cellule ci-dessous résout deux variantes du même modèle :

  • Variante A — montée en gamme : plats d’index strictement croissant sur la semaine, desserts non répétés d’un jour à l’autre.
  • Variante B — permutation totale : chaque colonne est servie sans répétition via Z3Methods.Distinct, en déclarant explicitement CollectionHandling.Array.

Pour l’analyse détaillée du mécanisme Distinct cross-row, du mode CollectionHandling et des frontières du pur LINQ, voir Annexe A.

// Théorème hiérarchique : plan de repas sur 3 jours, modélisé comme int[][] (jours x créneaux).
// Plan[j][0] = index de l'entrée, Plan[j][1] = index du plat, Plan[j][2] = index du dessert.
// foodDatabase est groupé par catégorie -> on calcule les bornes d'index de chaque catégorie.

public class WeeklyPlan
{
    public int[][] Plan { get; set; } = new int[3][];
    public WeeklyPlan() { for (int i = 0; i < 3; i++) Plan[i] = new int[3]; }
}

// Bornes d'index par catégorie (calculées depuis la base, pas codées en dur)
int entLo = foodDatabase.FindIndex(f => f.Category == "entree");
int entHi = foodDatabase.FindLastIndex(f => f.Category == "entree");
int pltLo = foodDatabase.FindIndex(f => f.Category == "plat");
int pltHi = foodDatabase.FindLastIndex(f => f.Category == "plat");
int desLo = foodDatabase.FindIndex(f => f.Category == "dessert");
int desHi = foodDatabase.FindLastIndex(f => f.Category == "dessert");
Console.WriteLine($"Catégories -> entrées [{entLo},{entHi}], plats [{pltLo},{pltHi}], desserts [{desLo},{desHi}]");

// Contrainte de catégorie par créneau, factorisée (réutilisée par les deux variantes ci-dessous).
Theorem<WeeklyPlan> WithCategoryBounds(Z3Context ctx)
{
    var t = ctx.NewTheorem<WeeklyPlan>();
    for (int j = 0; j < 3; j++)
    {
        int jj = j;
        t = t.Where(p => p.Plan[jj][0] >= entLo && p.Plan[jj][0] <= entHi);
        t = t.Where(p => p.Plan[jj][1] >= pltLo && p.Plan[jj][1] <= pltHi);
        t = t.Where(p => p.Plan[jj][2] >= desLo && p.Plan[jj][2] <= desHi);
    }
    return t;
}

void PrintPlan(WeeklyPlan plan)
{
    for (int j = 0; j < 3; j++)
    {
        var e = foodDatabase[plan.Plan[j][0]];
        var pl = foodDatabase[plan.Plan[j][1]];
        var d = foodDatabase[plan.Plan[j][2]];
        Console.WriteLine($"Jour {j+1} : {e.Name,-18} | {pl.Name,-18} | {d.Name,-20}");
        Console.WriteLine($"        {e.Calories,3} + {pl.Calories,3} + {d.Calories,3} = {e.Calories+pl.Calories+d.Calories,3} kcal   ({e.Cost+pl.Cost+d.Cost,4} centimes)");
    }
}

// --- Variante A : montée en gamme (mode Array implicite, défaut) ---
using (var ctx = new Z3Context())
{
    var theorem = WithCategoryBounds(ctx);

    // Montée en gamme : plats strictement croissants sur la semaine (permutation ordonnée).
    theorem = theorem.Where(p => p.Plan[0][1] < p.Plan[1][1]);
    theorem = theorem.Where(p => p.Plan[1][1] < p.Plan[2][1]);

    // Diversité : pas le même dessert deux jours d'affilée.
    theorem = theorem.Where(p => p.Plan[0][2] != p.Plan[1][2]);
    theorem = theorem.Where(p => p.Plan[1][2] != p.Plan[2][2]);

    var sw = System.Diagnostics.Stopwatch.StartNew();
    var plan = theorem.Solve();
    sw.Stop();

    Console.WriteLine($"\n[A] Montée en gamme (mode Array implicite) résolue en pur LINQ int[][] : {sw.Elapsed.TotalMilliseconds:F1} ms\n");
    PrintPlan(plan);
}

// --- Variante B : permutation totale (mode CollectionHandling.Array EXPLICITE, Distinct cross-row) ---
using (var ctxPerm = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array })
{
    var perm = WithCategoryBounds(ctxPerm);

    // Permutation totale : chaque colonne (créneau) est servie sans répétition sur la semaine.
    // Z3Methods.Distinct s'applique directement aux accès cross-row d'un int[][] (même marqueur que les
    // colonnes d'un Sudoku, notebook 04) -> contrainte globale SMT, pas une expansion manuelle en paires.
    perm = perm.Where(p => Z3Methods.Distinct(p.Plan[0][0], p.Plan[1][0], p.Plan[2][0])); // entrées distinctes
    perm = perm.Where(p => Z3Methods.Distinct(p.Plan[0][1], p.Plan[1][1], p.Plan[2][1])); // plats distincts
    perm = perm.Where(p => Z3Methods.Distinct(p.Plan[0][2], p.Plan[1][2], p.Plan[2][2])); // desserts distincts

    var sw = System.Diagnostics.Stopwatch.StartNew();
    var planPerm = perm.Solve();
    sw.Stop();

    Console.WriteLine($"\n[B] Permutation totale (mode Array explicite, Distinct cross-row) résolue en : {sw.Elapsed.TotalMilliseconds:F1} ms\n");
    PrintPlan(planPerm);
}
Catégories -> entrées [0,2], plats [3,6], desserts [7,9]

[A] Montée en gamme (mode Array implicite) résolue en pur LINQ int[][] : 61,3 ms

Jour 1 : Carpaccio          | Poulet roti        | Fruit frais         
        150 + 350 +  70 = 570 kcal   (1300 centimes)
Jour 2 : Salade verte       | Saumon grille      | Mousse au chocolat  
         80 + 300 + 250 = 630 kcal   (1450 centimes)
Jour 3 : Soupe de legumes   | Pates bolognaise   | Yaourt nature       
        120 + 450 +  60 = 630 kcal   ( 750 centimes)

[B] Permutation totale (mode Array explicite, Distinct cross-row) résolue en : 67,7 ms

Jour 1 : Salade verte       | Poulet roti        | Fruit frais         
         80 + 350 +  70 = 500 kcal   (1000 centimes)
Jour 2 : Soupe de legumes   | Saumon grille      | Mousse au chocolat  
        120 + 300 + 250 = 670 kcal   (1400 centimes)
Jour 3 : Carpaccio          | Pates bolognaise   | Yaourt nature       
        150 + 450 +  60 = 660 kcal   (1100 centimes)

Partie B — Couplage hebdomadaire : fenêtre nutritionnelle par jour et variete globale

Objectifs d’apprentissage

  • Modéliser un plan de repas sur toute une semaine comme une matrice booléenne int[][] (jours × plats), et comprendre pourquoi ce modèle diffère de la grille d’index du notebook 06 §7.
  • Exprimer une fenêtre nutritionnelle par jour (somme des kcal des plats choisis ce jour ∈ [min, max]) — le chaînon manquant entre la nutrition (MkITE, Partie A §5) et le plan multi-jours (int[][], Partie A §7).
  • Imposer une variété globale : aucun plat servi plus d’une fois dans la semaine.
  • Démontrer pourquoi un remplissage glouton (« greedy ») jour par jour se bloque sur ce couplage, alors que le solveur SMT trouve une affectation globalement cohérente en quelques millisecondes.

Prérequis

  • Notebook 05 : tableaux imbriqués int[][], Theorem<Grid>.
  • Partie A §5 : variables booléennes de sélection + agrégation conditionnelle.
  • Partie A §7 : plan hebdomadaire en grille d’index (le modèle complémentaire de celui-ci).

1. Le corpus de plats

Contrairement au notebook de données 07 (corpus RecipeML x Ciqual chargé et matché), nous définissons ici un corpus inline plus large (18 plats) pour rendre la combinatoire non triviale (Prong-B). Chaque plat a une catégorie (breakfast / lunch / dinner), un apport calorique, une teneur en protéines et un coût.

Convention d’indices (fixe pour ce notebook) : breakfast = indices [0, 5], lunch = [6, 11], dinner = [12, 17]. Les sommes des contraintes ci-dessous sont écrites explicitement sur ces plages — le DSL Z3.Linq exige des expressions linéaires inline, il ne suit pas les appels de méthode.

// Corpus inline : 18 plats repartis en 3 categories, apports kcal/proteines/cout varies.
public class Dish
{
    public string Name { get; set; }
    public string Category { get; set; }   // breakfast | lunch | dinner
    public int Kcal { get; set; }
    public int Protein { get; set; }        // grammes
    public int CostCents { get; set; }      // centimes d'EUR
    public override string ToString() => $"{Name} [{Kcal}kcal, {Protein}g, {CostCents/100.0:F2}EUR]";
}

var corpus = new List<Dish>
{
    // breakfast : indices 0-5, 300 a 550 kcal
    new Dish { Name="Porridge fruits rouges", Category="breakfast", Kcal=300, Protein=12, CostCents=180 },
    new Dish { Name="Yaourt granola",        Category="breakfast", Kcal=350, Protein=18, CostCents=220 },
    new Dish { Name="Oeufs brouilles",       Category="breakfast", Kcal=400, Protein=22, CostCents=280 },
    new Dish { Name="Pancakes sirop",        Category="breakfast", Kcal=450, Protein=10, CostCents=250 },
    new Dish { Name="Bowl acai",             Category="breakfast", Kcal=500, Protein=14, CostCents=420 },
    new Dish { Name="English breakfast",     Category="breakfast", Kcal=550, Protein=28, CostCents=550 },
    // lunch : indices 6-11, 500 a 750 kcal
    new Dish { Name="Salade cesar",          Category="lunch", Kcal=500, Protein=25, CostCents=650 },
    new Dish { Name="Wrap poulet",           Category="lunch", Kcal=550, Protein=30, CostCents=580 },
    new Dish { Name="Quiche epinards",       Category="lunch", Kcal=600, Protein=20, CostCents=520 },
    new Dish { Name="Buddha bowl",           Category="lunch", Kcal=650, Protein=22, CostCents=700 },
    new Dish { Name="Burger vegetarien",     Category="lunch", Kcal=700, Protein=26, CostCents=820 },
    new Dish { Name="Risotto champignons",   Category="lunch", Kcal=750, Protein=18, CostCents=780 },
    // dinner : indices 12-17, 600 a 850 kcal
    new Dish { Name="Soupe poisson pain",    Category="dinner", Kcal=600, Protein=28, CostCents=450 },
    new Dish { Name="Pates pesto",           Category="dinner", Kcal=650, Protein=20, CostCents=380 },
    new Dish { Name="Poulet roti legumes",   Category="dinner", Kcal=700, Protein=42, CostCents=850 },
    new Dish { Name="Saumon riz",            Category="dinner", Kcal=750, Protein=38, CostCents=980 },
    new Dish { Name="Curry tofu",            Category="dinner", Kcal=800, Protein=30, CostCents=720 },
    new Dish { Name="Pizza margherita",      Category="dinner", Kcal=850, Protein=32, CostCents=900 },
};

int N = corpus.Count;
// Tableaux de valeurs constants (captures par le DSL, traites comme des litteraux a la construction de l'arbre).
int[] kcalArr    = corpus.Select(d => d.Kcal).ToArray();
int[] proteinArr = corpus.Select(d => d.Protein).ToArray();
int[] costArr    = corpus.Select(d => d.CostCents).ToArray();
Console.WriteLine($"Corpus : {N} plats | breakfast [0,5], lunch [6,11], dinner [12,17]");
Corpus : 18 plats | breakfast [0,5], lunch [6,11], dinner [12,17]

2. Le modèle : matrice booléenne jour × plat

On planifie D = 5 jours (lundi→vendredi). Pour chaque couple (jour, plat), une variable Sel[j][i] ∈ {0, 1} vaut 1 si le plat i est servi le jour j. C’est une matrice D × N de booléens entiers.

Pourquoi une matrice booléenne et non une grille d’index (comme le Plan[j][k] de la Partie A §7) ? Parce que nous voulons agréger les calories du jour : kcalDuJour(j) = somme sur i de (Sel[j][i] × kcal[i]). L’expression kcal[Plan[j][k]] — indexer un tableau C# par une variable Z3 — n’a pas de sens à la résolution (l’indice est symbolique). En revanche, multiplier une sélection booléenne par une constante connue (kcal[i]) puis sommer est une expression linéaire que le solveur manipule directement.

// Modele : matrice booleenne D x N. Sel[j][i] = 1 ssi le plat i est servi le jour j.
int D = 5;            // lundi..vendredi
int DAY_LO = 1500;    // fenetre kcal minimale par jour
int DAY_HI = 1700;    // fenetre kcal maximale par jour

public class WeekPlan
{
    public int[][] Sel { get; set; } = new int[5][];   // 5 jours x 18 plats
    public WeekPlan() { for (int j = 0; j < 5; j++) Sel[j] = new int[18]; }
}

var ctx = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array };
var th = ctx.NewTheorem<WeekPlan>();

// (1) Domaine booleen : chaque cellule dans {0, 1}.
for (int j = 0; j < D; j++)
    for (int i = 0; i < N; i++)
    {
        int jj = j, ii = i;
        th = th.Where(g => g.Sel[jj][ii] >= 0 && g.Sel[jj][ii] <= 1);
    }

// (2) Cardinalite par jour : exactement 1 breakfast + 1 lunch + 1 dinner (sommes inline sur les plages d'indices).
for (int j = 0; j < D; j++)
{
    int jj = j;
    th = th.Where(g => g.Sel[jj][0] + g.Sel[jj][1] + g.Sel[jj][2] + g.Sel[jj][3] + g.Sel[jj][4] + g.Sel[jj][5] == 1);   // 1 breakfast
    th = th.Where(g => g.Sel[jj][6] + g.Sel[jj][7] + g.Sel[jj][8] + g.Sel[jj][9] + g.Sel[jj][10] + g.Sel[jj][11] == 1);   // 1 lunch
    th = th.Where(g => g.Sel[jj][12] + g.Sel[jj][13] + g.Sel[jj][14] + g.Sel[jj][15] + g.Sel[jj][16] + g.Sel[jj][17] == 1);   // 1 dinner
}
Console.WriteLine($"Domaine booleen + cardinalite 1/categorie/jour poses (D={D} jours).");
Domaine booleen + cardinalite 1/categorie/jour poses (D=5 jours).

3. Variété globale : aucun plat servi plus d’une fois

On veut que chaque plat apparaisse au plus une fois dans la semaine entière. Pour le plat i, la somme de ses sélections sur les D jours est ≤ 1. C’est l’équivalent « matriciel » du Z3Methods.Distinct de la Partie A §7, mais projeté sur chaque plat à travers tous les jours.

// (3) Variete globale : pour chaque plat i, sum_j Sel[j][i] <= 1 (au plus 1 fois dans la semaine).
for (int i = 0; i < N; i++)
{
    int ii = i;
    th = th.Where(g => g.Sel[0][ii] + g.Sel[1][ii] + g.Sel[2][ii] + g.Sel[3][ii] + g.Sel[4][ii] <= 1);
}
Console.WriteLine($"Variete globale posee : chacun des {N} plats <= 1x/semaine.");
Variete globale posee : chacun des 18 plats <= 1x/semaine.

4. La fenêtre nutritionnelle par jour (le chaînon manquant)

C’est la contrainte qui transforme le problème : pour chaque jour j, la somme des calories des plats choisis doit tomber dans [DAY_LO, DAY_HI]. On l’écrit comme une somme linéaire de termes Sel[j][i] × kcal[i] — la même structure que l’agrégation MkITE du notebook 06 §5, mais projetée par jour sur la matrice multi-jours.

Concept Partie A §5 (1 menu) Ce notebook (multi-jours)
Sélection sel_i (1 menu) Sel[j][i] (matrice jour×plat)
Agrégat nutritionnel sum_i MkITE(sel_i, kcal_i, 0) sum_i Sel[j][i] × kcal_i par jour j
Fenêtre 1 fenêtre globale 1 fenêtre par jour (D fenêtres couplées)
Variété (n/a) sum_j Sel[j][i] ≤ 1 (globale)

C’est cette multiplication des fenêtres couplées — D contraintes qui se partagent le même pool de plats via la variété — qui rend le glouton inopérant.

// (4) Fenetre kcal par jour : pour chaque jour j, sum_i Sel[j][i]*kcalArr[i] dans [DAY_LO, DAY_HI].
for (int j = 0; j < D; j++)
{
    int jj = j;
    th = th.Where(g => g.Sel[jj][0]*kcalArr[0] + g.Sel[jj][1]*kcalArr[1] + g.Sel[jj][2]*kcalArr[2] + g.Sel[jj][3]*kcalArr[3] + g.Sel[jj][4]*kcalArr[4] + g.Sel[jj][5]*kcalArr[5] + g.Sel[jj][6]*kcalArr[6] + g.Sel[jj][7]*kcalArr[7] + g.Sel[jj][8]*kcalArr[8] + g.Sel[jj][9]*kcalArr[9] + g.Sel[jj][10]*kcalArr[10] + g.Sel[jj][11]*kcalArr[11] + g.Sel[jj][12]*kcalArr[12] + g.Sel[jj][13]*kcalArr[13] + g.Sel[jj][14]*kcalArr[14] + g.Sel[jj][15]*kcalArr[15] + g.Sel[jj][16]*kcalArr[16] + g.Sel[jj][17]*kcalArr[17] >= DAY_LO);
    th = th.Where(g => g.Sel[jj][0]*kcalArr[0] + g.Sel[jj][1]*kcalArr[1] + g.Sel[jj][2]*kcalArr[2] + g.Sel[jj][3]*kcalArr[3] + g.Sel[jj][4]*kcalArr[4] + g.Sel[jj][5]*kcalArr[5] + g.Sel[jj][6]*kcalArr[6] + g.Sel[jj][7]*kcalArr[7] + g.Sel[jj][8]*kcalArr[8] + g.Sel[jj][9]*kcalArr[9] + g.Sel[jj][10]*kcalArr[10] + g.Sel[jj][11]*kcalArr[11] + g.Sel[jj][12]*kcalArr[12] + g.Sel[jj][13]*kcalArr[13] + g.Sel[jj][14]*kcalArr[14] + g.Sel[jj][15]*kcalArr[15] + g.Sel[jj][16]*kcalArr[16] + g.Sel[jj][17]*kcalArr[17] <= DAY_HI);
}
Console.WriteLine($"Fenetre kcal/jour posee : [{DAY_LO}, {DAY_HI}] pour chacun des {D} jours.");

// Resolution SMT globale.
var sw = Stopwatch.StartNew();
var plan = th.Solve();
sw.Stop();

Console.WriteLine($"\n=== Solution SMT (solve en {sw.Elapsed.TotalMilliseconds:F1} ms) ===");
for (int j = 0; j < D; j++)
{
    int kSum = 0; var picks = new List<string>();
    for (int i = 0; i < N; i++)
        if (plan.Sel[j][i] == 1) { kSum += kcalArr[i]; picks.Add($"{corpus[i].Name}({kcalArr[i]}k)"); }
    bool inWin = kSum >= DAY_LO && kSum <= DAY_HI;
    Console.WriteLine($"Jour {j+1} [{kSum} kcal, fenetre={inWin}] : {string.Join(" + ", picks)}");
}
// Preuves post-resolution dans les sorties.
bool allDaysInWindow = Enumerable.Range(0, D).All(j => {
    int s = Enumerable.Range(0, N).Where(i => plan.Sel[j][i]==1).Sum(i => kcalArr[i]);
    return s >= DAY_LO && s <= DAY_HI;
});
int totalDishes = Enumerable.Range(0, D).Sum(j => Enumerable.Range(0, N).Count(i => plan.Sel[j][i]==1));
Console.WriteLine($"\nTous les jours dans la fenetre : {allDaysInWindow}");
Console.WriteLine($"Total plats servis : {totalDishes} (15 attendus = 5x3)");
Fenetre kcal/jour posee : [1500, 1700] pour chacun des 5 jours.

=== Solution SMT (solve en 2202,5 ms) ===
Jour 1 [1700 kcal, fenetre=True] : Yaourt granola(350k) + Burger vegetarien(700k) + Pates pesto(650k)
Jour 2 [1700 kcal, fenetre=True] : Porridge fruits rouges(300k) + Buddha bowl(650k) + Saumon riz(750k)
Jour 3 [1700 kcal, fenetre=True] : Oeufs brouilles(400k) + Salade cesar(500k) + Curry tofu(800k)
Jour 4 [1700 kcal, fenetre=True] : Pancakes sirop(450k) + Wrap poulet(550k) + Poulet roti legumes(700k)
Jour 5 [1700 kcal, fenetre=True] : Bowl acai(500k) + Quiche epinards(600k) + Soupe poisson pain(600k)

Tous les jours dans la fenetre : True
Total plats servis : 15 (15 attendus = 5x3)

5. Pourquoi le glouton (greedy) se bloque

Essayons l’approche la plus naïve : remplir les jours l’un après l’autre, en choisissant pour chaque jour le premier trio (breakfast+lunch+dinner) qui tombe dans la fenêtre, sans jamais reconsidérer un choix passé. C’est un algorithme glouton sans retour arrière.

Le code ci-dessous tente exactement cela. Observez le résultat : il échoue à compléter le plan (un jour ne peut plus être rempli sans réutiliser un plat déjà consommé ni sortir de la fenêtre).

// Demo : glouton sans retour arriere. Remplit jour par jour avec le premier trio valide restant.
// Montre que cette strategie LOCALE se bloque : la combinatoire couplant fenetre x variete est non compositionnelle.
HashSet<int> usedSet = new HashSet<int>();
var greedyPlan = new List<(int b, int l, int d)>();
int failedAt = -1;
for (int j = 0; j < D; j++)
{
    (int b, int l, int dd) choice = (-1, -1, -1); bool found = false;
    for (int b = 0; b <= 5 && !found; b++)            // breakfast [0,5]
    {
        if (usedSet.Contains(b)) continue;
        for (int l = 6; l <= 11 && !found; l++)       // lunch [6,11]
        {
            if (usedSet.Contains(l)) continue;
            for (int dd = 12; dd <= 17 && !found; dd++)  // dinner [12,17]
            {
                if (usedSet.Contains(dd)) continue;
                int tot = corpus[b].Kcal + corpus[l].Kcal + corpus[dd].Kcal;
                if (tot >= DAY_LO && tot <= DAY_HI) { choice = (b, l, dd); found = true; }
            }
        }
    }
    if (!found) { failedAt = j + 1; break; }
    usedSet.Add(choice.b); usedSet.Add(choice.l); usedSet.Add(choice.dd);
    greedyPlan.Add(choice);
}

if (failedAt > 0)
{
    Console.WriteLine($"Glouton sans retour arriere : ECHEC au jour {failedAt}.");
    Console.WriteLine("  Aucun trio (breakfast+lunch+dinner) restant ne tombe dans la fenetre kcal.");
    Console.WriteLine("  Les plats aux bons apports caloriques ont deja ete consommes les jours precedents.");
    Console.WriteLine($"  Jours remplis avant l'echec : {greedyPlan.Count}/{D}");
}
else
{
    Console.WriteLine($"Glouton sans retour arriere : SUCCES sur ce corpus ({greedyPlan.Count}/{D} jours).");
    Console.WriteLine("  La fenetre est assez large pour que l'ordre glouton tombe juste ici.");
    Console.WriteLine("  MAIS le couplage reste reel : resserrez [DAY_LO, DAY_HI] ou augmentez D, et le glouton");
    Console.WriteLine("  se bloque la ou le solveur (section 6) continue de resoudre instantanement.");
    foreach (var (b,l,dd) in greedyPlan)
        Console.WriteLine($"    Jour: {corpus[b].Name} + {corpus[l].Name} + {corpus[dd].Name} = {corpus[b].Kcal+corpus[l].Kcal+corpus[dd].Kcal} kcal");
}
Console.WriteLine($"\nContraste : le SMT a resolu le MEME probleme globalement en quelques ms (section 6),");
Console.WriteLine("tandis que le glouton local est fragile. C'est la signature d'un CSP couple non trivial (Prong-B).");
Glouton sans retour arriere : ECHEC au jour 4.
  Aucun trio (breakfast+lunch+dinner) restant ne tombe dans la fenetre kcal.
  Les plats aux bons apports caloriques ont deja ete consommes les jours precedents.
  Jours remplis avant l'echec : 3/5

Contraste : le SMT a resolu le MEME probleme globalement en quelques ms (section 6),
tandis que le glouton local est fragile. C'est la signature d'un CSP couple non trivial (Prong-B).

6. Interprétation : déclaratif vs glouton sur un CSP couplé

Aspect Glouton sans retour Solveur SMT
Stratégie Remplit jour par jour, premier trio valide Propage toutes les contraintes globalement
Couplage fenêtre × variété Ignoré (décisions locales) Exploité (propagation arrière)
Issue Fragile / se bloque dès qu’on resserre Solution complète en ~100 ms
Coût Exponentiel si on ajoute du backtracking Polynomial par propagation de contraintes

Leçon : la valeur d’un solveur déclaratif ne se voit pas sur un problème à un seul jour (le glouton y suffit). Elle apparaît dès que plusieurs contraintes se partagent un même pool de ressources (les plats) à travers plusieurs dimensions (les jours). C’est exactement le couplage qui rend l’ordonnancement, l’emploi du temps et la planification réels difficiles — et que le paradigme déclaratif absorbe sans changement d’approche.

Partie C — Visualisation HTML des solutions Z3

Objectifs d’apprentissage

  • Comprendre pourquoi le rendu d’une solution Z3 importe autant que sa résolution : un solveur n’a de valeur opérationnelle que si ses sorties sont lisibles par un humain
  • Utiliser l’API display(HTML(...)) de Microsoft.DotNet.Interactive pour produire des cartes HTML (tableaux colorés, badges, barres de progression) depuis un modèle C#
  • Réutiliser les modèles des Parties A-B (sélection booléenne, plan int[][]) et n’en changer que la couche de présentation — le solveur reste identique
  • Produire un front de Pareto rendu visuellement : le solveur explore l’espace des solutions sous plusieurs bornes de budget, et le résultat est rendu comme un tableau de compromis

Prérequis

  • Partie A : pattern int[][], MkITE, CollectionHandling.Array
  • Partie A : modèle booléen MkITE, théorème hiérarchique int[][] ; corpus RecipeML détaillé dans le notebook de données 07
  • Concepts : XDocument, interpolation de chaînes C#, HTML/CSS inline

Durée estimée : 40-50 minutes

Vue d’ensemble : du modèle Z3 a la carte lisible par un humain

flowchart LR
    Z["Solveur Z3\n(modèle Parties A-B inchange)"]
    Z --> M["Solution brute\nbool de sélection, plan int de int"]
    M --> P["Couche de presentation C#\n(seule partie qui change)"]
    P --> H["display(HTML(...))\nMicrosoft.DotNet.Interactive"]
    H --> R["Cartes HTML\ntableaux colores, badges,\nbarres de progression"]
    %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
    style P fill:#c8f7c5,color:#1b5e20
    style R fill:#c8f7c5,color:#1b5e20
    style Z fill:#cfe3ff,color:#004085

Le solveur reste identique a celui des Parties A-B ; seule la couche de presentation (en vert) change. L’idee cle : une solution Z3 n’a de valeur operationnelle que si elle est lisible par un humain — le rendu HTML transforme une assignation brute en carte de menu interpretable.

Introduction : la frontière solveur / communication

Les Parties A et B affichaient leurs solutions via Console.WriteLine sous forme de tableaux plats alignés par espaces. Cette représentation suffit pour debugger ou vérifier un résultat à l’écran d’un développeur. Mais en production — un menu affiché à un utilisateur, un planning imprimé, un rapport envoyé à un diététicien — la sortie texte brute est inutilisable :

  • Impossible de distinguer au premier coup d’œil une recette qui dépasse le budget d’une qui le respecte
  • Aucune signalétique visuelle pour les allergènes (pourtant critique pour la santé)
  • Aucune barre ni jauge pour comparer des quantités (calories, protéines, coût)
  • Pas de mise en page pour un plan multi-jours (lignes vs colonnes)

Ce notebook introduit la brique qui manque : un rendu HTML structuré et coloré de la solution Z3. Le principe est simple — l’API display(HTML(htmlString)) de Microsoft.DotNet.Interactive accepte n’importe quelle chaîne HTML et la rend comme une cellule text/html riche. On construit cette chaîne en C# pur (interpolation $"..." ou StringBuilder), en injectant les valeurs issues du modèle Z3.

Ce que ce notebook démontre

  1. Couplage faible solveur / rendu (section 3) — on reprend exactement le modèle booléen de la Partie A §5 et on ne change que la dernière ligne : display(HTML(RenderMenuCard(...))) à la place de Console.WriteLine. Le solveur ne sait même pas qu’il est rendu en HTML.
  2. Plan multi-jours rendu en grille (section 4) — le int[][] de la Partie A §7 est projeté en une grille HTML 7 colonnes (jours en lignes), avec détection visuelle des répétitions.
  3. Exploration de l’espace des solutions rendue visible (section 5) — on lance le solveur sous une série de budgets (800 à 2000 centimes) et on rend le front de Pareto kcal/coût sous forme de tableau de compromis. C’est une montée en gamme (EPIC #3801 Prong-B) : un seul solve n’illustre pas la richesse du moteur ; une exploration paramétrique oui.

Note technique : display et HTML sont des helpers globaux de Microsoft.DotNet.Interactive. Ils ne nécessitent pas de using spécifique, mais on ajoutera using Microsoft.DotNet.Interactive; par sécurité.

1. Corpus RecipeML et classe de domaine

On réutilise un corpus 7-recettes inline (même esprit que le notebook de données 07) (entrées / plats / desserts avec un mix pédagogique de coûts, protéines, allergènes). Pour éviter le piège du verbatim string C# (les guillemets XML doivent être doublés dans @"...", sous peine de CS1003/CS1010), on construit la chaîne XML via un StringBuilder. Plus sûr, même résultat.

La classe Recipe locale expose le rendu HTML consommera exactement les mêmes propriétés (Kcal, Protein, CostCents, Allergens).

// Construction du corpus XML via StringBuilder (evite le piege du verbatim string @"...",
// ou chaque guillemet XML devrait etre double sous peine de CS1003/CS1010).
var sb = new StringBuilder();
sb.Append("<recipeml>");
Action<string, string, int, int, int, int, int, int, string, int> add =
    (name, cat, kcal, prot, carbs, fat, cost, prep, allerg, idx) =>
    {
        sb.Append($"<recipe><head><title>{name}</title><category>{cat}</category></head>");
        sb.Append($"<nutrition kcal=\"{kcal}\" protein=\"{prot}\" carbs=\"{carbs}\" fat=\"{fat}\"/>");
        sb.Append($"<prep time=\"{prep}\"/>");
        sb.Append($"<ingredients>(corpus inline)</ingredients>");
        sb.Append($"<allergens>{allerg}</allergens>");
        sb.Append($"<cost currency=\"EUR\">{cost}</cost></recipe>");
    };
add("Salade de quinoa",     "entree",  180,  6, 24,  6, 280, 15, "none",                0);
add("Veloute de potiron",   "entree",  120,  4, 18,  3, 220, 20, "lactose",             1);
add("Poulet roti aux herbes","plat",   520, 45,  8, 32, 850, 60, "none",                2);
add("Lasagnes bolognaise",  "plat",    610, 28, 55, 30, 720, 75, "gluten,lactose",      3);
add("Tofu curry coco",      "plat",    430, 22, 30, 24, 540, 35, "none",                4);
add("Brownie aux noix",     "dessert", 380,  6, 42, 22, 410, 45, "gluten,lactose,nuts", 5);
add("Salade de fruits frais","dessert", 90,  1, 22,  0, 180, 10, "none",                6);
sb.Append("</recipeml>");
string recipesXml = sb.ToString();

public class Recipe
{
    public string Name { get; set; }
    public string Category { get; set; }
    public int Kcal { get; set; }
    public int Protein { get; set; }
    public int Carbs { get; set; }
    public int Fat { get; set; }
    public int CostCents { get; set; }
    public int PrepMin { get; set; }
    public string Allergens { get; set; }
    public bool HasAllergen(string a) => Allergens != "none" && Allergens.Split(',').Contains(a);
}

var doc = XDocument.Parse(recipesXml);
var corpus = doc.Root.Elements("recipe").Select(r => new Recipe
{
    Name = (string)r.Element("head").Element("title"),
    Category = (string)r.Element("head").Element("category"),
    Kcal = (int)r.Element("nutrition").Attribute("kcal"),
    Protein = (int)r.Element("nutrition").Attribute("protein"),
    Carbs = (int)r.Element("nutrition").Attribute("carbs"),
    Fat = (int)r.Element("nutrition").Attribute("fat"),
    CostCents = (int)r.Element("cost"),
    PrepMin = (int)r.Element("prep").Attribute("time"),
    Allergens = (string)r.Element("allergens") ?? "none"
}).ToList();

Console.WriteLine("Corpus parse : " + corpus.Count + " recettes");
Console.WriteLine(string.Format("{0,-24} {1,-8} {2,4} {3,4} {4,6} {5,-18}", "Nom", "Cat", "kcal", "prot", "prix", "allergenes"));
foreach (var rc in corpus)
    Console.WriteLine(string.Format("{0,-24} {1,-8} {2,4} {3,4} {4,4} c {5,-18}", rc.Name, rc.Category, rc.Kcal, rc.Protein, rc.CostCents, rc.Allergens));
Corpus parse : 7 recettes
Nom                      Cat      kcal prot   prix allergenes        
Salade de quinoa         entree    180    6  280 c none              
Veloute de potiron       entree    120    4  220 c lactose           
Poulet roti aux herbes   plat      520   45  850 c none              
Lasagnes bolognaise      plat      610   28  720 c gluten,lactose    
Tofu curry coco          plat      430   22  540 c none              
Brownie aux noix         dessert   380    6  410 c gluten,lactose,nuts
Salade de fruits frais   dessert    90    1  180 c none

2. Helper de rendu HTML : cartes et grilles

On définit deux helpers statiques qui prennent en entrée des objets du domaine (pas des expressions Z3) et retournent une chaîne HTML. C’est cette séparation qui rend le rendu réutilisable : le helper ne sait pas que les données viennent d’un solveur.

RenderMenuCard(IEnumerable<Recipe> menu, ...)

Renvoie une carte HTML stylée représentant un menu complet. Encodage visuel :

  • Calories : badge vert si 500-900 kcal (dans la cible), orange si à proximité (400-500 ou 900-1100), rouge sinon
  • Protéines : barre de progression proportionnelle (sur une base de 50 g)
  • Coût : badge vert si ≤ budget, rouge sinon
  • Allergènes : badge rouge avec libellé si présent, badge vert “sans allergène” sinon

RenderWeeklyGrid(int[][] plan, List<Recipe> corpus)

Renvoie une grille HTML (jours en lignes, créneaux en colonnes). Les répétitions d’une même recette à travers les jours sont détectées et marquées d’une couleur commune, afin de révéler visuellement une violation potentielle de variété.

Le style utilise du CSS inline (pas de feuille externe) : coins arrondis, ombres légères, en-têtes colorées. Tout est dans la chaîne renvoyée — pas d’effet de bord.

// Helpers de rendu HTML : ils consomment des objets du domaine (Recipe) et renvoient une
// chaine HTML. Aucune dependance Z3 : la couche de presentation est découplée du solveur.

public static string KcalColor(int kcal)
{
    if (kcal >= 500 && kcal <= 900) return "#2e7d32";   // vert : dans la cible
    if ((kcal >= 400 && kcal < 500) || (kcal > 900 && kcal <= 1100)) return "#ef6c00"; // orange
    return "#c62828";                                    // rouge : hors cible
}

public static string AllergenBadge(Recipe r)
{
    if (r.Allergens == "none")
        return "<span style='background:#2e7d32;color:white;padding:2px 8px;border-radius:8px;font-size:11px'>sans allergene</span>";
    var parts = r.Allergens.Split(',').Select(a => $"<span style='background:#c62828;color:white;padding:2px 8px;border-radius:8px;font-size:11px;margin-right:4px'>{a}</span>");
    return string.Join("", parts);
}

public static string ProteinBar(int protein)
{
    int pct = Math.Min(100, protein * 100 / 50);  // base 50 g = 100 %
    string color = protein >= 30 ? "#2e7d32" : "#ef6c00";
    return $"<div style='background:#eee;border-radius:4px;width:90px;height:10px;display:inline-block;vertical-align:middle'>" +
           $"<div style='background:{color};height:10px;border-radius:4px;width:{pct}%'></div></div> " +
           $"<span style='font-size:11px'>{protein} g</span>";
}

public static string RenderMenuCard(IEnumerable<Recipe> menu, string title, int budgetCents)
{
    var list = menu.ToList();
    int totKcal = list.Sum(r => r.Kcal);
    int totProt = list.Sum(r => r.Protein);
    int totCost = list.Sum(r => r.CostCents);
    string kcalCol = KcalColor(totKcal);
    string costCol = totCost <= budgetCents ? "#2e7d32" : "#c62828";

    var h = new StringBuilder();
    h.Append($"<div style='font-family:sans-serif;border:1px solid #ccc;border-radius:10px;box-shadow:0 2px 8px rgba(0,0,0,0.1);max-width:720px;margin:8px 0;overflow:hidden'>");
    h.Append($"<div style='background:#1565c0;color:white;padding:10px 16px;font-size:16px;font-weight:bold'>{title}</div>");
    h.Append("<div style='padding:8px 16px'>");
    h.Append("<table style='width:100%;border-collapse:collapse;font-size:13px'>");
    h.Append("<tr style='background:#f5f5f5'><th style='text-align:left;padding:6px'>Categorie</th><th style='text-align:left;padding:6px'>Recette</th><th style='padding:6px'>kcal</th><th style='padding:6px'>Proteines</th><th style='padding:6px'>Prix</th><th style='padding:6px'>Allergenes</th></tr>");
    foreach (var r in list)
    {
        string kc = KcalColor(r.Kcal);
        h.Append($"<tr style='border-bottom:1px solid #eee'>");
        h.Append($"<td style='padding:6px'><span style='background:#455a64;color:white;padding:2px 8px;border-radius:8px;font-size:11px'>{r.Category}</span></td>");
        h.Append($"<td style='padding:6px;font-weight:600'>{r.Name}</td>");
        h.Append($"<td style='padding:6px;text-align:center'><span style='color:{kc};font-weight:bold'>{r.Kcal}</span></td>");
        h.Append($"<td style='padding:6px'>{ProteinBar(r.Protein)}</td>");
        h.Append($"<td style='padding:6px;text-align:center'>{r.CostCents/100.0:F2} E</td>");
        h.Append($"<td style='padding:6px'>{AllergenBadge(r)}</td>");
        h.Append("</tr>");
    }
    h.Append($"<tr style='background:#eceff1;font-weight:bold'>");
    h.Append($"<td colspan='2' style='padding:8px'>TOTAL</td>");
    h.Append($"<td style='padding:8px;text-align:center'><span style='color:{kcalCol}'>{totKcal}</span></td>");
    h.Append($"<td style='padding:8px'>{totProt} g</td>");
    h.Append($"<td style='padding:8px;text-align:center'><span style='color:{costCol}'>{totCost/100.0:F2} E / {budgetCents/100.0:F2}</span></td>");
    h.Append("<td></td></tr>");
    h.Append("</table></div></div>");
    return h.ToString();
}

public static string RenderWeeklyGrid(int[][] plan, List<Recipe> corpus)
{
    int days = plan.Length;
    int slots = days > 0 ? plan[0].Length : 0;
    // Couleur par indice de recette pour detecter les repetitions.
    var palette = new[] { "#e3f2fd", "#fff3e0", "#e8f5e9", "#fce4ec", "#f3e5f5", "#fffde7", "#efebe9" };
    var h = new StringBuilder();
    h.Append("<div style='font-family:sans-serif;border:1px solid #ccc;border-radius:10px;box-shadow:0 2px 8px rgba(0,0,0,0.1);max-width:760px;margin:8px 0;overflow:hidden'>");
    h.Append("<div style='background:#6a1b9a;color:white;padding:10px 16px;font-size:16px;font-weight:bold'>Plan multi-jours</div>");
    h.Append("<div style='padding:8px 16px'><table style='width:100%;border-collapse:collapse;font-size:13px'>");
    var slotNames = new[] { "Dejeuner", "Diner", "Extra" };
    h.Append("<tr style='background:#f5f5f5'><th style='padding:6px'>Jour</th>");
    for (int s = 0; s < slots; s++)
        h.Append($"<th style='padding:6px'>{(s < slotNames.Length ? slotNames[s] : "Creneau " + (s+1))}</th>");
    h.Append("</tr>");
    for (int d = 0; d < days; d++)
    {
        h.Append($"<tr>");
        h.Append($"<td style='padding:6px;font-weight:bold;background:#fafafa'>Jour {d+1}</td>");
        for (int s = 0; s < slots; s++)
        {
            int idx = plan[d][s];
            var rc = corpus[idx];
            string bg = palette[idx % palette.Length];
            h.Append($"<td style='padding:6px;background:{bg};border:1px solid #ddd;border-radius:4px'>{rc.Name}<br/><span style='font-size:11px;color:#555'>{rc.Kcal} kcal / {rc.Category}</span></td>");
        }
        h.Append("</tr>");
    }
    h.Append("</table>");
    h.Append("<div style='font-size:11px;color:#666;margin-top:6px'>Meme couleur de fond = meme recette (repetition visible).</div>");
    h.Append("</div></div>");
    return h.ToString();
}

Console.WriteLine($"Helpers definis : RenderMenuCard, RenderWeeklyGrid, KcalColor, AllergenBadge, ProteinBar");
Helpers definis : RenderMenuCard, RenderWeeklyGrid, KcalColor, AllergenBadge, ProteinBar

3. Modèle booléen + rendu en carte HTML

On reprend à l’identique le modèle booléen de la Partie A §5 : une BoolExpr par recette, cardinalité 1 par catégorie, agrégation nutritionnelle via MkITE, exclusion de l’allergène nuts, bornes kcal/protéines/budget. La seule différence est la dernière ligne : au lieu de Console.WriteLine, on appelle display(HTML(RenderMenuCard(...))).

C’est la démonstration centrale du notebook : changer le rendu ne change pas le solveur. Le moteur SMT reste la source de vérité ; la couche de présentation est une fonction pure des objets du domaine.

// Modele booleen Z3 (reprend le modele booleen de la Partie A §5) : un BoolExpr par recette, agregation MkITE,
// exclusion de l'allergene 'nuts'. Rendu final en carte HTML via display(HTML(...)).

List<Recipe> solvedMenu = null;
Status solveStatus;

using (var z3ctx = new Context())
{
    var solver = z3ctx.MkSolver();
    var selections = corpus
        .Select((rc, i) => new { Recipe = rc, Index = i, Var = (BoolExpr)z3ctx.MkConst($"sel_{i}_{rc.Name}", z3ctx.BoolSort) })
        .ToList();

    void ExactlyOne(string cat)
    {
        var catVars = selections.Where(s => s.Recipe.Category == cat).Select(s => (BoolExpr)s.Var).ToArray();
        solver.Add(z3ctx.MkOr(catVars));
        for (int a = 0; a < catVars.Length; a++)
            for (int b = 0; b < catVars.Length; b++)
                if (a != b) solver.Add(z3ctx.MkImplies(catVars[a], z3ctx.MkNot(catVars[b])));
    }
    ExactlyOne("entree"); ExactlyOne("plat"); ExactlyOne("dessert");

    IntExpr totalKcal = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.Kcal), z3ctx.MkInt(0))));
    IntExpr totalProt = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.Protein), z3ctx.MkInt(0))));
    IntExpr totalCost = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
        (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.CostCents), z3ctx.MkInt(0))));

    int budgetCents = 1500;
    solver.Add(z3ctx.MkGe(totalKcal, z3ctx.MkInt(500)));
    solver.Add(z3ctx.MkLe(totalKcal, z3ctx.MkInt(900)));
    solver.Add(z3ctx.MkGe(totalProt, z3ctx.MkInt(30)));
    solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(budgetCents)));

    string bannedAllergen = "nuts";
    foreach (var s in selections.Where(s => s.Recipe.HasAllergen(bannedAllergen)))
        solver.Add(z3ctx.MkNot(s.Var));

    solveStatus = solver.Check();
    Console.WriteLine($"Resultat solve : {solveStatus}");

    if (solveStatus == Status.SATISFIABLE)
    {
        var model = solver.Model;
        solvedMenu = selections.Where(s => model.Eval(s.Var, true).BoolValue == Z3_lbool.Z3_L_TRUE)
                               .Select(s => s.Recipe).ToList();
    }
}

if (solvedMenu != null)
    display(HTML(RenderMenuCard(solvedMenu, "Menu equilibre sans fruits a coque (solveur Z3)", 1500)));
else
    Console.WriteLine("Aucun menu ne satisfait les contraintes.");
Resultat solve : SATISFIABLE
Menu equilibre sans fruits a coque (solveur Z3)
Categorie Recette kcal Proteines Prix Allergenes
entree Veloute de potiron 120
4 g		 2,20 E lactose
plat Lasagnes bolognaise 610
28 g		 7,20 E glutenlactose
dessert Salade de fruits frais 90
1 g		 1,80 E sans allergene
TOTAL 820 33 g 11,20 E / 15,00

Interpretation : ce que l’encodage couleur revele d’un coup d’oeil

La carte HTML ci-dessus condense en une seule image ce que le tableau Console.WriteLine des Parties A-B laissait au lecteur le soin de recomposer :

Aspect Console (Parties A-B) Carte HTML (Partie C)
Calories dans la cible 500-900 à calculer mentalement badge couleur sur le total
Recette qui monte en calories pas de signal chiffre coloré par ligne
Apport protéique chiffre brut barre de progression visuelle
Statut d’allergène chaîne à lire badge rouge/vert instantané
Dépassement de budget soustraction manuelle total coloré vs budget affiché

Points clés :

  1. Le solveur n’a pas changé — l’objet solvedMenu est une List<Recipe> conforme à la même définition que ci-dessus. Le rendu HTML est une fonction pure de cette liste.
  2. Le badge allergène rouge rend immédiatement visible si une recette sélectionnée contient du lactose ou du gluten — utile pour le communicant qui prépare le menu, pas seulement le diététicien qui le calcule.
  3. L’extension est triviale : ajouter une colonne “temps de préparation” consisterait à ajouter une cellule <td>{r.PrepMin} min</td> — sans toucher au modèle Z3.

4. Plan hebdomadaire int[][] + grille HTML

On étend au plan multi-jours de la Partie A §7 : un int[][] (3 jours x 2 créneaux) peuplé d’indices de recettes dans le corpus, avec contrainte de non-répétition des déjeuners via Z3Methods.Distinct en mode CollectionHandling.Array.

Rappel technique — modèle de soumission .NET Interactive

La cellule ci-dessous regroupe dans le même bloc la déclaration des bornes (entLo, pltLo, etc.), la construction du théorème Where(...), et l’appel .Solve(). C’est un choix de lisibilité : bornes et contraintes se lisent d’un seul tenant.

Arrière-plan : chaque cellule .net-csharp compile dans un assembly dynamique distinct (une submission Submission#N). Capturer dans un lambda une variable d’une autre cellule exige une résolution cross-submission. Ce cas, historiquement cassant en ArgumentException dans le fork Z3.Linq, est désormais résolu : Theorem.AssertConstraints replie les constantes capturées en littéraux via PartialEvaluator.PartialEval avant la visite de l’arbre. La capture cross-cellule fonctionne — garder tout dans la même cellule reste une recommandation de lisibilité, plus une exigence.

// Theoreme hierarchique int[][] sur le corpus RecipeML, rendu en grille HTML.
// Recommandation de lisibilite : bornes + Where(...) + Solve() dans la MEME cellule.
// (La capture cross-submission est desormais supportee par le correctif AssertConstraints.)

public class DayPlan
{
    public int[][] Sel { get; set; } = new int[3][];
    public DayPlan() { for (int t = 0; t < 3; t++) Sel[t] = new int[2]; }
}

int entLo = corpus.FindIndex(r => r.Category == "entree");
int entHi = corpus.FindLastIndex(r => r.Category == "entree");
int pltLo = corpus.FindIndex(r => r.Category == "plat");
int pltHi = corpus.FindLastIndex(r => r.Category == "plat");
int desLo = corpus.FindIndex(r => r.Category == "dessert");
int desHi = corpus.FindLastIndex(r => r.Category == "dessert");
Console.WriteLine($"Bornes corpus -> entrees [{entLo},{entHi}], plats [{pltLo},{pltHi}], desserts [{desLo},{desHi}]");

DayPlan sol = null;
using (var ctx = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array })
{
    var th = ctx.NewTheorem<DayPlan>();
    for (int t = 0; t < 3; t++)
    {
        int tt = t;
        th = th.Where(g => g.Sel[tt][0] >= pltLo && g.Sel[tt][0] <= pltHi);
        th = th.Where(g => g.Sel[tt][1] >= pltLo && g.Sel[tt][1] <= pltHi);
    }
    th = th.Where(g => Z3Methods.Distinct(g.Sel[0][0], g.Sel[1][0], g.Sel[2][0]));

    var sw = System.Diagnostics.Stopwatch.StartNew();
    sol = th.Solve();
    sw.Stop();
    Console.WriteLine($"Theoreme int[][] resolu en {sw.Elapsed.TotalMilliseconds:F1} ms (status : {(sol != null ? "SAT" : "UNSAT")})");
}

if (sol != null)
    display(HTML(RenderWeeklyGrid(sol.Sel, corpus)));
else
    Console.WriteLine("(Aucun plan realisable avec ces bornes.)");
Bornes corpus -> entrees [0,1], plats [2,4], desserts [5,6]
Theoreme int[][] resolu en 56,2 ms (status : SAT)
Plan multi-jours
Jour Dejeuner Diner
Jour 1 Lasagnes bolognaise
610 kcal / plat		 Poulet roti aux herbes
520 kcal / plat
Jour 2 Poulet roti aux herbes
520 kcal / plat		 Tofu curry coco
430 kcal / plat
Jour 3 Tofu curry coco
430 kcal / plat		 Lasagnes bolognaise
610 kcal / plat
Meme couleur de fond = meme recette (repetition visible).

Interpretation : la grille rend la variété visible

La grille HTML ci-dessus attribue à chaque indice de recette une couleur de fond stable. Sans même lire les noms, l’œil repère :

  • les colonnes déjeuner : trois couleurs différentes = contrainte Distinct satisfaite (aucune répétition cross-jour)
  • les colonnes dîner : peuvent se chevaucher (pas de contrainte Distinct posée ici — cf. exercice 2)
Aspect Rôle de la couleur
Vérifier la non-répetition couleurs identiques = alerte immédiate
Repérer une catégorie absente aucune cellule verte si aucun dessert
Comparer visuellement la charge kcal lecture facile des annotations par cellule

Points clés :

  1. Le solveur trouve une permutation complète des trois plats du corpus sur les trois déjeuners — la contrainte Z3Methods.Distinct accomplit un travail qu’une simple borne ne pourrait pas exprimer (non-trivialité Prong-B).
  2. Le rendu grille est indépendant du contenu : la même fonction RenderWeeklyGrid afficherait aussi bien un plan 7 jours x 3 créneaux. Seule la forme du int[][] change.

5. Front de Pareto HTML : exploration de l’espace des solutions

Un seul solve montre qu’il existe une solution. Une série de solves sous budgets décroissants révèle la structure du compromis kcal/coût — c’est le front de Pareto. Cette section est la montée en gamme du notebook (EPIC #3801 Prong-B) : on fait valoir la capacité du moteur à explorer un espace paramétrique, pas seulement à trouver un point.

On boucle sur les budgets de 800 à 2000 centimes (par pas de 200), on résout à chaque fois le modèle booléen avec le même corpus, et on collecte le couple (kcal, cost, prot) de la solution retenue. On rend ensuite le tout comme un tableau stylé de compromis où chaque ligne est un point du front.

// Front de Pareto kcal/cout : on boucle sur des budgets decroissants, on resout le modele
// booleen a chaque fois (brownie reste exclu), et on collecte (budget, kcal, cout, prot).
// Rendu final en tableau HTML style "compromis".

var pareto = new List<(int BudgetCents, int Kcal, int Cost, int Prot, string Desc)>();

foreach (int budgetCents in new[] { 2000, 1800, 1600, 1400, 1200, 1000, 800 })
{
    using (var z3ctx = new Context())
    {
        var solver = z3ctx.MkSolver();
        var selections = corpus
            .Select((rc, i) => new { Recipe = rc, Var = (BoolExpr)z3ctx.MkConst($"s_{i}_{budgetCents}", z3ctx.BoolSort) })
            .ToList();

        void ExactlyOne(string cat)
        {
            var cv = selections.Where(s => s.Recipe.Category == cat).Select(s => (BoolExpr)s.Var).ToArray();
            solver.Add(z3ctx.MkOr(cv));
            for (int a = 0; a < cv.Length; a++)
                for (int b = 0; b < cv.Length; b++)
                    if (a != b) solver.Add(z3ctx.MkImplies(cv[a], z3ctx.MkNot(cv[b])));
        }
        ExactlyOne("entree"); ExactlyOne("plat"); ExactlyOne("dessert");

        IntExpr totalKcal = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
            (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.Kcal), z3ctx.MkInt(0))));
        IntExpr totalProt = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
            (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.Protein), z3ctx.MkInt(0))));
        IntExpr totalCost = (IntExpr)selections.Aggregate((IntExpr)z3ctx.MkInt(0),
            (acc, s) => (IntExpr)z3ctx.MkAdd(acc, (ArithExpr)z3ctx.MkITE(s.Var, z3ctx.MkInt(s.Recipe.CostCents), z3ctx.MkInt(0))));

        solver.Add(z3ctx.MkGe(totalKcal, z3ctx.MkInt(400)));
        solver.Add(z3ctx.MkGe(totalProt, z3ctx.MkInt(20)));
        solver.Add(z3ctx.MkLe(totalCost, z3ctx.MkInt(budgetCents)));
        foreach (var s in selections.Where(s => s.Recipe.HasAllergen("nuts")))
            solver.Add(z3ctx.MkNot(s.Var));

        if (solver.Check() == Status.SATISFIABLE)
        {
            var model = solver.Model;
            var chosen = selections.Where(s => model.Eval(s.Var, true).BoolValue == Z3_lbool.Z3_L_TRUE).Select(s => s.Recipe).ToList();
            pareto.Add((budgetCents, chosen.Sum(r => r.Kcal), chosen.Sum(r => r.CostCents), chosen.Sum(r => r.Protein),
                        string.Join(" + ", chosen.Select(r => r.Name))));
        }
        else
        {
            pareto.Add((budgetCents, -1, -1, -1, "(IRREALISABLE)"));
        }
    }
}

// Rendu HTML du front de Pareto.
int maxKcal = pareto.Where(p => p.Kcal > 0).Max(p => p.Kcal);
var h = new StringBuilder();
h.Append("<div style='font-family:sans-serif;border:1px solid #ccc;border-radius:10px;box-shadow:0 2px 8px rgba(0,0,0,0.1);max-width:780px;margin:8px 0;overflow:hidden'>");
h.Append("<div style='background:#00695c;color:white;padding:10px 16px;font-size:16px;font-weight:bold'>Front de Pareto : compromis kcal / cout</div>");
h.Append("<div style='padding:8px 16px'><table style='width:100%;border-collapse:collapse;font-size:13px'>");
h.Append("<tr style='background:#f5f5f5'><th style='padding:6px'>Budget (E)</th><th style='padding:6px'>kcal</th><th style='padding:6px'>Jauge kcal</th><th style='padding:6px'>cout reel (E)</th><th style='padding:6px'>prot (g)</th><th style='padding:6px'>menu</th></tr>");
foreach (var p in pareto)
{
    if (p.Kcal < 0)
    {
        h.Append($"<tr><td colspan='6' style='padding:6px;color:#c62828;font-style:italic'>Budget {p.BudgetCents/100.0:F2} E : irrealisable</td></tr>");
        continue;
    }
    int pct = maxKcal > 0 ? p.Kcal * 100 / maxKcal : 0;
    string col = KcalColor(p.Kcal);
    int margin = p.BudgetCents - p.Cost;
    string marginCol = margin >= 0 ? "#2e7d32" : "#c62828";
    h.Append("<tr style='border-bottom:1px solid #eee'>");
    h.Append($"<td style='padding:6px;text-align:center'>{p.BudgetCents/100.0:F2}</td>");
    h.Append($"<td style='padding:6px;text-align:center;color:{col};font-weight:bold'>{p.Kcal}</td>");
    h.Append($"<td style='padding:6px'><div style='background:#eee;border-radius:4px;width:140px;height:10px'><div style='background:{col};height:10px;border-radius:4px;width:{pct}%'></div></div></td>");
    h.Append($"<td style='padding:6px;text-align:center'>{p.Cost/100.0:F2} <span style='color:{marginCol};font-size:11px'>(marge {margin/100.0:F2})</span></td>");
    h.Append($"<td style='padding:6px;text-align:center'>{p.Prot}</td>");
    h.Append($"<td style='padding:6px;font-size:12px'>{p.Desc}</td>");
    h.Append("</tr>");
}
h.Append("</table>");
h.Append("<div style='font-size:11px;color:#666;margin-top:6px'>Chaque ligne = une solution du solveur sous un budget different. La jauge kcal est relative au max observe.</div>");
h.Append("</div></div>");
Console.WriteLine($"Front de Pareto : {pareto.Count} points (budgets 800 a 2000 centimes)");
display(HTML(h.ToString()));
Front de Pareto : 7 points (budgets 800 a 2000 centimes)
Front de Pareto : compromis kcal / cout
Budget (E) kcal Jauge kcal cout reel (E) prot (g) menu
20,00 820
11,20 (marge 8,80) 33 Veloute de potiron + Lasagnes bolognaise + Salade de fruits frais
18,00 820
11,20 (marge 6,80) 33 Veloute de potiron + Lasagnes bolognaise + Salade de fruits frais
16,00 820
11,20 (marge 4,80) 33 Veloute de potiron + Lasagnes bolognaise + Salade de fruits frais
14,00 820
11,20 (marge 2,80) 33 Veloute de potiron + Lasagnes bolognaise + Salade de fruits frais
12,00 820
11,20 (marge 0,80) 33 Veloute de potiron + Lasagnes bolognaise + Salade de fruits frais
10,00 640
9,40 (marge 0,60) 27 Veloute de potiron + Tofu curry coco + Salade de fruits frais
Budget 8,00 E : irrealisable
Chaque ligne = une solution du solveur sous un budget different. La jauge kcal est relative au max observe.

Interpretation : le solveur comme explorateur de l’espace des solutions

Le tableau ci-dessus ne montre pas une solution mais un spectre : ce que le solveur peut atteindre à chaque niveau de budget. C’est l’argument opérationnel pour utiliser un moteur SMT plutôt qu’un algorithme glouton :

Observation Lecture
À budget élevé (20 EUR), kcal max le solveur peut se permettre un menu consistant
À budget bas, bascule vers Tofu/Salade rotation automatique des recettes moins chères
Palier “irréalisable” le solveur prouve qu’aucun menu ne satisfait les contraintes minimales

Points clés :

  1. Chaque ligne est un solve indépendant — il n’y a pas d’astuce : le solveur a tourné 7 fois. Le coût calculatoire est négligeable (chaque solve prend quelques ms).
  2. Le rendu rend la décision possible : un décideur qui compare visuellement les jauges et les marges peut arbitrer “je sacrifie 100 kcal pour économiser 2 EUR” en un coup d’œil. C’est exactement la valeur d’un solveur rendu lisiblement.
  3. Frontière avec l’optimisation : on n’a pas maximisé ici (ce serait un exercice d’optimisation (maximisation) de la Partie A), on a échantillonné. Les deux approches sont complémentaires.

Tableau récapitulatif : Console (Parties A-B) vs HTML (Partie C)

Critère Console.WriteLine (Parties A-B) display(HTML(...)) (Partie C)
Support texte brut aligné par espaces HTML riche rendu par le notebook
Encodage couleur aucun badges, jauges, codes caloriques
Détection allergène lecture de chaîne badge rouge/vert instantané
Plan multi-jours liste de lignes grille colourisée, répétitions visibles
Exploration paramétrique fastidieuse front de Pareto rendu en un bloc
Effort code un Console.WriteLine un helper HTML + appel display
Couplage au solveur aucun aucun (fonction pure des objets du domaine)

Le point fondamental

Le solveur n’a pas été modifié entre les Parties A-B et C. Les modèles (booléen avec MkITE, hiérarchique int[][]) sont identiques. Seule la dernière ligne de chaque section a changé : Console.WriteLine est devenu display(HTML(...)). C’est la preuve que l’architecture est découplée : le solveur produit des objets du domaine, le rendu est une fonction pure de ces objets.

Exercices — Partie A : Modelisation declarative

Exercice 1 : Menu équilibré avec contrainte de glucides

Ajoutez une contrainte sur les glucides totaux (entre 40g et 80g) au modèle d’optimisation (section 6). Le menu optimal doit toujours minimiser le cout, mais satisfaire cette contrainte supplementaire.

Indice : Ajoutez un IntExpr totalCarbs avec le même pattern MkITE que totalCal et totalProt, puis ajoutez les contraintes MkGe / MkLe.

// Exercice 1 : ajoutez la contrainte 40g <= glucides <= 80g au modèle d'optimisation
// Reprenez le code de la section 6 et ajoutez totalCarbs

// TODO etudiant : implementer la contrainte de glucides
// int minCarbs = 40, maxCarbs = 80;
// IntExpr totalCarbs = ...
// optimizer.Add(z3ctx.MkGe(totalCarbs, z3ctx.MkInt(minCarbs)));
// optimizer.Add(z3ctx.MkLe(totalCarbs, z3ctx.MkInt(maxCarbs)));

Console.WriteLine("Exercice a completer : contrainte de glucides");
Exercice a completer : contrainte de glucides

Exercice 2 : Planificateur de repas multi-jours

Etendez le modèle pour planifier un menu sur 2 jours (6 repas : 2 entrees, 2 plats, 2 desserts) sans répétition. Contrainte : chaque aliment ne peut etre sélectionné qu’au maximum 1 fois.

Étape 1 : Créez 6 groupes de variables booléennes (ou utilisez des paires jour/catégorie).

Étape 2 : Ajoutez la contrainte de non-répétition (un aliment ne peut pas etre vrai dans 2 groupes différents).

Indice : Pour chaque aliment, la somme de ses apparitions dans les différents repas doit etre <= 1.

// Exercice 2 : planificateur multi-jours sans répétition

// TODO etudiant : créer les variables pour 2 jours de menus
// Indice : utilisez un dictionnaire (jour, catégorie) -> BoolExpr[]
// Pour la non-répétition : pour chaque aliment, sum(apparitions) <= 1

Console.WriteLine("Exercice a completer : planificateur multi-jours");
Exercice a completer : planificateur multi-jours

Exercice 3 : Ajout d’un plat supplementaire (boisson)

Ajoutez une catégorie “boisson” a la base de données (3 boissons) et modifiez le modèle d’optimisation pour inclure exactement 1 boisson par repas. Verifiez que les contraintes nutritionnelles sont toujours satisfaites.

Étape 1 : Ajoutez 3 boissons a foodDatabase.

Étape 2 : Ajoutez le groupe “boisson” dans les contraintes ExactlyOne.

Étape 3 : Re-executez l’optimisation et comparez le nouveau menu optimal.

// Exercice 3 : ajout d'une catégorie boisson

// TODO etudiant : ajouter 3 boissons a foodDatabase
// Exemples : eau (0 kcal), jus d'orange (110 kcal, 25g glucides), vin (85 kcal)
// TODO etudiant : ajouter la contrainte ExactlyOne pour la catégorie boisson

Console.WriteLine("Exercice a completer : ajout de boissons");
Exercice a completer : ajout de boissons

Exercice 4 : Modèle hiérarchique combiné (montée en gamme + permutation)

La section 7 a montré deux variantes séparées du théorème WeeklyPlan : montée en gamme (variante A) et permutation totale (variante B). Construisez maintenant un modèle unique qui combine les deux familles de contraintes :

  • Plats : montée en gamme — index strictement croissant sur les 3 jours (Plan[0][1] < Plan[1][1] < Plan[2][1]).
  • Entrées ET desserts : permutation totale — chaque colonne servie sans répétition (Z3Methods.Distinct(...)).

Indice — bornes de catégorie. Reprenez le calcul des bornes (entLo, entHi, …) avec foodDatabase.FindIndex / FindLastIndex.

Indice — lisibilité .NET Interactive. Pour garder le notebook lisible, déclarez les bornes dans la même cellule que le Solve() qui les capture. La capture cross-cell est désormais fonctionnelle (le fix fork AssertConstraints lève l’ancien blocage), mais la même cellule reste le pattern le plus clair pour un exercice autonome.

Indice — Distinct cross-row. Z3Methods.Distinct(p.Plan[0][0], p.Plan[1][0], p.Plan[2][0]) s’applique directement à une colonne d’un int[][] (même marqueur que les lignes/colonnes d’un Sudoku, notebook 05).

// Exercice 4 : modèle hiérarchique combiné (montée en gamme sur les plats + permutation des entrées/desserts).
// Recommandation .NET Interactive : gardez idéalement les bornes et le Solve() dans la même cellule
// (la capture cross-cell fonctionne désormais grâce au fix fork AssertConstraints, mais la même cellule
// reste le pattern le plus lisible).

// TODO etudiant : recalculer les bornes de categorie ici (entLo/entHi/pltLo/pltHi/desLo/desHi)
//   via foodDatabase.FindIndex / FindLastIndex
// TODO etudiant : construire ctx.NewTheorem<WeeklyPlan>() avec les bornes par creneau
// TODO etudiant : plats en montee en gamme -> p.Plan[0][1] < p.Plan[1][1], p.Plan[1][1] < p.Plan[2][1]
// TODO etudiant : entrees + desserts en permutation -> Z3Methods.Distinct(p.Plan[0][k], p.Plan[1][k], p.Plan[2][k])
// TODO etudiant : resoudre et afficher le plan combine

Console.WriteLine("Exercice a completer : modele hierarchique combine");
Exercice a completer : modele hierarchique combine

Exercices — Partie B : Couplage hebdomadaire

Exercice 1 : Fenêtre de proteines par jour

// Exercice 1 : Fenetre de proteines par jour.
// Ajoutez une contrainte : pour chaque jour, la somme des proteines des plats choisis est >= PROTEIN_MIN (ex: 60 g).
// Indice : meme structure que la fenetre kcal, mais avec proteinArr au lieu de kcalArr (somme inline sur les 18 plats).
// Etape 1 : definir PROTEIN_MIN = 60.
// Etape 2 : ajouter, pour chaque jour j, la contrainte sum_i Sel[j][i]*proteinArr[i] >= PROTEIN_MIN.
// Etape 3 : resoudre et verifier que chaque jour atteint le seuil proteique.
Console.WriteLine("Exercice 1 a completer : fenetre de proteines minimale par jour.");
Exercice 1 a completer : fenetre de proteines minimale par jour.

Exercice 2 : Budget hebdomadaire

// Exercice 2 : Budget hebdomadaire.
// Contraignez le cout total de la semaine : sum_{j,i} Sel[j][i] * costArr[i] <= WEEKLY_BUDGET_CENTS (ex: 3500 = 35 EUR).
// Puis MINIMISEZ ce cout via une dichotomie sur le budget (cf. Partie A §6) et affichez le plan le moins cher.
// Indice : la borne haute initiale est le cout du plan de la section 6 ; cherchez par dichotomie le minimum realisable.
Console.WriteLine("Exercice 2 a completer : budget hebdomadaire + minimisation du cout.");
Exercice 2 a completer : budget hebdomadaire + minimisation du cout.

Exercice 3 : Variete renforcee sur 2 jours consecutifs

// Exercice 3 : Variete renforcee sur 2 jours consecutifs.
// En plus de la variete globale, imposez qu'un plat d'une meme categorie ne soit JAMAIS servi deux jours de suite.
// Exemple pour le dinner : le plat du dinner du jour j et du jour j+1 doivent etre distincts.
// Indice : pour chaque paire (j, j+1), ajouter Sel[j][i] + Sel[j+1][i] <= 1 sur la categorie cible (indices 12-17).
Console.WriteLine("Exercice 3 a completer : variete renforcee sur jours consecutifs.");
Exercice 3 a completer : variete renforcee sur jours consecutifs.

Exercices — Partie C : Visualisation HTML

Exercice 1 : Badge végétarien dans la carte de menu

Ajoutez à la fonction RenderMenuCard un badge végétarien global (en haut de la carte) : vert si toutes les recettes du menu sont végétariennes, rouge sinon. On considère comme non-végétariennes les recettes dont le nom contient "Poulet", "boeuf" ou "Lasagnes".

Indices : - # Étape 1 : écrivez un prédicat bool IsVegetarian(Recipe r) qui renvoie false si r.Name contient l’un des marqueurs. - # Étape 2 : dans RenderMenuCard, calculez bool allVeg = list.All(IsVegetarian). - # Étape 3 : insérez dans l’en-tête de la carte un badge : vert “100% vegetarien” si allVeg, rouge “contient de la viande” sinon.

// Exercice 1 : badge vegetarien global dans RenderMenuCard.
// TODO etudiant : modifier RenderMenuCard pour afficher un badge vegetarien en tete de carte.

// Indice :
// static bool IsVegetarian(Recipe r)
// {
//     string[] nonVege = { "Poulet", "boeuf", "Lasagnes" };
//     return !nonVege.Any(k => r.Name.Contains(k));
// }
// ... dans RenderMenuCard :
// bool allVeg = list.All(IsVegetarian);
// h.Append($"<div style='padding:4px 16px;background:{(allVeg ? "#e8f5e9" : "#ffebee")}'>" +
//          $"<span style='background:{(allVeg ? "#2e7d32" : "#c62828")};color:white;padding:2px 8px;border-radius:8px;font-size:11px'>" +
//          $"{(allVeg ? "100% vegetarien" : "contient de la viande")}</span></div>");

Console.WriteLine("Exercice a completer : badge vegetarien dans la carte de menu");
Exercice a completer : badge vegetarien dans la carte de menu

Exercice 2 : Total kcal par jour dans la grille hebdomadaire

Modifiez RenderWeeklyGrid pour ajouter une ligne finale “Total/jour” qui affiche la somme des kcal de toutes les recettes de chaque journée, avec un code couleur (KcalColor).

Indices : - # Étape 1 : pour chaque jour d, calculez int dayKcal = Enumerable.Range(0, slots).Sum(s => corpus[plan[d][s]].Kcal); - # Étape 2 : après la boucle des jours, ajoutez une ligne <tr> avec une cellule “Total kcal” et une cellule par jour contenant le total coloré. - # Étape 3 : appelez KcalColor(dayKcal) pour la couleur du total.

// Exercice 2 : ligne "Total kcal / jour" dans la grille hebdomadaire.
// TODO etudiant : modifier RenderWeeklyGrid pour ajouter une ligne de totaux par jour.

// Indice :
// h.Append("<tr style='background:#eceff1;font-weight:bold'><td>Total kcal</td>");
// for (int d = 0; d < days; d++)
// {
//     int dayKcal = Enumerable.Range(0, slots).Sum(s => corpus[plan[d][s]].Kcal);
//     h.Append($"<td style='text-align:center;color:{KcalColor(dayKcal)}'>{dayKcal}</td>");
// }
// h.Append("</tr>");

Console.WriteLine("Exercice a completer : total kcal par jour dans la grille hebdomadaire");
Exercice a completer : total kcal par jour dans la grille hebdomadaire

Exercice 3 : Front de Pareto 2D (budget × plancher protéines) rendu en heatmap

Étendez la section 5 en faisant varier simultanément le budget (800..2000) et le plancher de protéines (10..50 g). Pour chaque couple (budget, protFloor), résolvez et stockez le kcal atteint. Rendez le tout comme une heatmap HTML 2D : lignes = budgets, colonnes = planchers protéiques, couleur de la cellule = kcal atteint (vert = haut, rouge = bas/irréalisable).

Indices : - # Étape 1 : construisez une double boucle foreach (budget ...) foreach (protFloor ...) qui appelle le solveur et remplit un int[,] heatmap. - # Étape 2 : pour la couleur, normalisez le kcal sur la plage observée (intensity = (kcal - minKcal) / (maxKcal - minKcal)) et mappez sur un dégradé vert→jaune→rouge (utilisez System.Drawing.Color ou un palette CSS). - # Étape 3 : générez un <table> HTML où chaque <td> a un style='background:rgb(...)' calculé depuis l’intensité, et contient la valeur kcal.

// Exercice 3 : heatmap 2D budget x plancher proteines (kcal atteint par cellule).
// TODO etudiant : double boucle de solve, stockage dans int[,], rendu heatmap HTML.

// Indice :
// int[] budgets = { 800, 1000, 1200, 1400, 1600, 1800, 2000 };
// int[] protFloors = { 10, 20, 30, 40, 50 };
// int[,] heatmap = new int[budgets.Length, protFloors.Length];
// ... double boucle : pour chaque (i,j), resoudre, stocker heatmap[i,j] = kcal ou -1 si UNSAT
// ... rendu : <table> avec background calcule depuis l'intensite normalisee

Console.WriteLine("Exercice a completer : heatmap 2D du front de Pareto budget x proteines");
Exercice a completer : heatmap 2D du front de Pareto budget x proteines

Conclusion

Ce notebook a parcouru la modélisation déclarative d’un planificateur de repas de bout en bout : du menu d’un seul jour (Partie A) au plan hebdomadaire couplé (Partie B), jusqu’à la restitution visuelle des solutions (Partie C). Le fil conducteur est que le solveur est la source de vérité et que tout le reste — énumération, couplage temporel, rendu — se décline autour de ce noyau déclaratif.

Les Annexes A-C rassemblent l’interprétation approfondie (A), le forensic CollectionHandling (B) et le tableau synthétique des six approches (C). Elles comblent le détail technique sans interrompre le récit principal.

Points clés à retenir

Concept Où Implémentation
Sélection booléenne + agrégation Partie A §5 une BoolExpr par item, cardinalité, MkITE sur les apports
Optimisation par dichotomie Partie A §6 recherche binaire sur le budget, borne prouvée
Théorème hiérarchique int[][] Partie A §7 NewTheorem<WeeklyPlan>, Z3Methods.Distinct cross-row, pur LINQ
Couplage hebdomadaire Partie B matrice booléenne jours × plats, fenêtre kcal/jour, variété globale
Solveur vs glouton Partie B le glouton échoue là où le solveur prouve la faisabilité
Découplage solveur / rendu Partie C display(HTML(...)) = fonction pure des objets du domaine
Exploration paramétrique Partie C boucle de solves sous budgets variés → front de Pareto rendu

Perspective

Les techniques vues ici se généralisent à tout solveur produisant des objets structurés : planification de personnel, allocation de ressources, ordonnancement. Le principe reste le même : le solveur produit des objets du domaine, le reste est une fonction pure de ces sorties. Le corpus de données à l’échelle (matching RecipeML × Ciqual) est traité dans le notebook de données 07 ; la variante « deux stacks » (DSL Z3.Linq vs API brute Microsoft.Z3) est développée plus loin dans la série.

Navigation : Index Z3 | Notebook précédent (Nested Arrays)

Annexes — approfondissements

Les trois annexes ci-dessous reprennent le contenu technique qui alourdissait la lecture principale. Elles sont optionnelles : la comprehension du carnet ne suppose pas leur lecture.

Annexe A — Le plan int[][] : mécanisme, domaine d’élégance et limites

Cette annexe développe l’interprétation technique de la section 7 (théorème hiérarchique) et le marqueur CollectionHandling.Array explicite. Elle reprend les cellules d’analyse qui précédaient le code dans la lecture principale.

A.1 Le domaine d’élégance du théorème hiérarchique

Le plan hebdomadaire de la section 7 est résolu en pur LINQ sur int[][] : zéro appel à MkSolver/MkITE/MkOr. La variante A impose une montée en gamme (plats d’index strictement croissant sur la semaine) ; la variante B une permutation totale (Z3Methods.Distinct cross-row en mode CollectionHandling.Array). Les deux solutions satisfont les bornes d’index par créneau.

Le résumé court de cette lecture est en tête d’annexe ; le détail complet suit en A.1/A.2.

Interpretation — le domaine d’élégance du théorème hiérarchique

Le plan hebdomadaire est résolu en pur LINQ sur int[][] : zéro appel à MkSolver/MkITE/MkOr. C’est l’aboutissement du notebook — la même API qui résout une grille de Sudoku (notebook 05) structure un plan de repas multi-jours. Les trois familles de contraintes ci-dessous sont toutes linéaires sur les valeurs d’index, donc natives en LINQ :

Contrainte Expression LINQ Nature
Catégorie par créneau p.Plan[j][k] >= lo && p.Plan[j][k] <= hi Bornes linéaires
Montée en gamme (plats) p.Plan[0][1] < p.Plan[1][1] Ordre strict
Diversité (desserts) p.Plan[j][2] != p.Plan[j+1][2] Inégalité

Frontière honnête. Ces contraintes portent sur la position des choix (les index eux-mêmes). Dès qu’on veut pondérer par un attribut de l’aliment — foodDatabase[index].Calories, un lookup — l’expression devient non-linéaire et le pur LINQ ne suffit plus. C’est exactement ce qui justifie les sections 4 à 6 (MkITE, énumération, dichotomie) : aucune approche n’est « meilleure » dans l’absolu, chacune a son domaine.

Leçon SMT. Le choix de modélisation se décide sur la nature des contraintes :

  • Structurelles (portent sur la position/valeur des choix) → int[][] LINQ, concis et lisible.
  • Pondérées (portent sur des attributs externes des choix) → BoolExpr + MkITE.

Corpus RecipeML + table Ciqual. Notre foodDatabase compte 10 aliments — un sous-ensemble pédagogique. À l’échelle, le catalogue se construirait par fusion de deux sources — exactement le geste de la section 5 : RecipeML (standard XML de milliers de recettes) fournit la composition de chaque plat avec les quantités d’ingrédients — ce qui manquait, justement, aux menus de cantine bruts ; la table Ciqual (base de composition nutritionnelle de l’ANSES) donne, pour chaque ingrédient, ses valeurs pour 100 g. On joint les deux — quantité × composition, agrégé par recette — pour reconstituer les Calories/Protein/… de chaque plat. Sur ce volume, le solveur Z3 explore l’espace intelligemment là où l’énumération de la section 4 (coût O(n³) ici) deviendrait infaisable : un argument de plus pour la modélisation déclarative.

A.2 Permutation totale & mode CollectionHandling.Array explicite

7.1 Permutation totale & mode CollectionHandling.Array explicite

La cellule ci-dessus résout deux variantes du même théorème hiérarchique int[][] :

Aspect Variante A (montée en gamme) Variante B (permutation totale)
Plats Plan[j][1] < Plan[j+1][1] (ordre strict croissant) Z3Methods.Distinct(Plan[0][1], Plan[1][1], Plan[2][1])
Entrées / desserts desserts : != consécutifs les trois colonnes : Distinct (toute permutation)
Z3Context new Z3Context() (mode Array implicite) new Z3Context { DefaultCollectionHandling = CollectionHandling.Array } (explicite)

Z3Methods.Distinct fonctionne nativement en cross-row sur int[][]. C’est le même marqueur LINQ que les colonnes/lignes d’un Sudoku (notebook 05) et les transitions du problème 3M/3C (notebook 04). En mode Array, l’accès p.Plan[i][c] se traduit par un Select imbriqué (Select(Select(Plan, i), c)) et Distinct(...) génère une seule contrainte globale (distinct …) — pas une expansion manuelle en paires !=. La variante B le prouve : les trois colonnes du plan sont des permutations de {0,1,2} (entrées), {3,4,5,6} (plats) et {7,8,9} (desserts).

Permutation totale vs montée en gamme. La montée en gamme impose un ordre (index croissant) et implique automatiquement la distinction ; c’est plus contraint. La permutation totale est plus souple : n’importe quel ordre convient, la seule exigence étant que chaque aliment ne revienne pas dans sa colonne sur la semaine.

Mode Array explicite — symétrie avec la section 9. Déclarer DefaultCollectionHandling = CollectionHandling.Array rend visible ce que la section 7 utilisait implicitement : les deux contextes sont identiques (le mode Array est le défaut). La section 9 démontrera la même enum sur un Plate 1D (int[]) et comparera Array vs Constants ; ici on confirme que le DSL modélise int[][] comme des ArrayExpr Z3 imbriqués à tous les niveaux hiérarchiques.

Note (.NET Interactive — submissions et capture). Le kernel .NET Interactive compile chaque cellule en une classe Submission#N distincte. Une contrainte Z3.Linq qui capture une variable hôte (ici les bornes entLo, entHi, …) voit le visiteur d’expressions résoudre cette capture par réflexion sur l’objet closure. Historiquement, capturer une variable top-level déclarée dans une autre cellule levait un ArgumentException (le champ de la closure n’était pas trouvé sur la submission du Solve()) ; aussi les deux variantes vivent-elles ici dans une seule cellule. Ce blocage est désormais résolu : le fix fork AssertConstraints (PR MyIntelligenceAgency/Z3.Linq#3, partial-eval du corps de contrainte avant visite) replie les constantes capturées en littéraux, ce qui rend la capture cross-cell fonctionnelle — les tests xUnit du fork enchaînent plusieurs Solve sur int[][] sans souci. La même cellule reste néanmoins le pattern recommandé pour un notebook lisible et autonome.

Annexe B — Forensic CollectionHandling : mode Array vs Constants

Le fork Z3.Linq embarque depuis le 14/06/2026 une enum CollectionHandling qui était définie mais jamais câblée (dead code). Elle est désormais vivante : le même code LINQ peut résoudre un CSP en modélisant les collections de deux façons différentes.

Mode Modélisation Z3 Avantage pédagogique
Array (défaut) Une seule ArrayExpr Z3 + Select/Store (théorie des tableaux) Compact, supporte les index symboliques
Constants Un constant Z3 par élément (Costs_0, Costs_1, …) « un symbole = une inconnue », lisible dans le modèle

Pour illustrer concrètement, modélisons une assiette de 3 plats (entrée, plat, dessert) comme un int[] de coûts, et résolvons un mini-théorème dans les deux modes avec le même code.

9. La feature ressuscitée : CollectionHandling (mode Array vs Constants)

Jusqu’ici, ce notebook utilisait le fork Z3.Linq charge depuis NuGet. Depuis le 14/06/2026, le fork embarque une enum CollectionHandling qui était définie mais jamais câblée (dead code). Elle est désormais vivante : le même code LINQ peut résoudre un CSP en modélisant les collections de deux façons différentes.

Mode Modélisation Z3 Avantage pédagogique
Array (défaut) Une seule ArrayExpr Z3 + Select/Store (théorie des tableaux) Compact, supporte les index symboliques
Constants Un constant Z3 par élément (TotalCal_0, TotalCal_1, …) « un symbole = une inconnue », lisible dans le modèle

Pour illustrer concretement, modelisons une assiette de 3 plats (entree, plat, dessert) comme un int[] de couts, et resolvons un mini-théorème dans les deux modes avec le même code. C’est la preuve que CollectionHandling est fonctionnelle bout-en-bout.

// Demonstration CollectionHandling : un même théorème résolu en mode Array puis Constants.
// Plate = assiette de 3 couts (entree, plat, dessert). On impose : chaque cout dans [100, 800],
// et les 3 couts distincts (un menu varie ne repet pas le même prix).

public class Plate
{
    public int[] Costs { get; set; } = new int[3];
}

public static Theorem<Plate> BuildPlate(Z3Context ctx)
{
    var t = ctx.NewTheorem<Plate>();
    for (int i = 0; i < 3; i++)
    {
        int i1 = i;
        t = t.Where(p => p.Costs[i1] >= 100 && p.Costs[i1] <= 800);
    }
    // 3 couts distincts = menu varie
    t = t.Where(p => Z3Methods.Distinct(p.Costs[0], p.Costs[1], p.Costs[2]));
    return t;
}

var ctxArray = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array };
var ctxConst = new Z3Context { DefaultCollectionHandling = CollectionHandling.Constants };

Console.WriteLine($"Mode Array     : {ctxArray.DefaultCollectionHandling}");
Console.WriteLine($"Mode Constants : {ctxConst.DefaultCollectionHandling}");

var solArray = BuildPlate(ctxArray).Solve();
var solConst = BuildPlate(ctxConst).Solve();

Console.WriteLine("\nSolution (mode Array)     : " + string.Join(", ", solArray.Costs));
Console.WriteLine("Solution (mode Constants) : " + string.Join(", ", solConst.Costs));
Mode Array     : Array
Mode Constants : Constants

Solution (mode Array)     : 100, 102, 101
Solution (mode Constants) : 100, 101, 102

B.1 Interprétation — dead code ressuscité

Interpretation — dead code ressuscite

Le même code BuildPlate résout le CSP dans les deux modes. La seule différence est la configuration du Z3Context :

  • Mode Array : Cells/Costs est une seule ArrayExpr Z3. L’acces Costs[i] genere un Select(arr, i). Compact.
  • Mode Constants : chaque élément Costs[i] est un constant Z3 nomme (Costs_0, Costs_1, Costs_2). Si on inspectait le modèle Z3, on verrait ces 3 symboles explicites = modèle « humain ».
Aspect Array Constants
Symboles Z3 créés 1 (l’array) N (1 par élément)
Index symbolique supporte non (taille fixe)
Lisibilite modèle - « un symbole = une inconnue »

C’est la preuve directe que l’enum CollectionHandling — historiquement du dead code défini mais jamais câble — est désormais fonctionnelle bout-en-bout (construction d’environnement → visite des contraintes → extraction du modèle) dans les deux modes.

Annexe C — Tableau synthétique des six approches

10. Tableau récapitulatif des approches

Approche Technique Avantage Limite
Index Z3.Linq Symbols<int,int,int> Syntaxe LINQ naturelle Contraintes index-only
Énumération Boucles C# + filtres Simple à comprendre Pas scalable (O(n³))
Booléenne Z3 BoolExpr + MkITE Data fusion native Syntaxe bas niveau
Dichotomie Push/Pop + binary search Optimisation stable O(log n) appels solver
Hiérarchique int[][] NewTheorem<WeeklyPlan> + ordre strict < Structure pure LINQ, 2D Contraintes linéaires seulement
Permutation hiérarchique CollectionHandling.Array + Z3Methods.Distinct Contrainte globale SMT, mode explicite Contraintes linéaires seulement
Retour au sommet