08 — Capstone hiérarchique : du squelette `int[][]` réel aux restrictions patient (port fidèle)

< Série Z3 | Capstone MealPlanner capstone (Part of #4617, See #1206)

Ce notebook est le cœur solveur du capstone MealPlanner. Il porte fidèlement la méthode PlanificateurDeMenus.Create du Demo2 d’origine (fork Z3.Linq, branche EPFdevelopment), et le construit en deux mouvements sur le corpus réel Ciqual ANSES 2025 × Recettes (mealplan_cache.json, produit par la [couche de données 07] — 07) :

Mouvement 1 — le squelette structurel int[][] sur les recettes reelles du cache. Bornes de créneau par rôle (entrée, plat, accompagnement…), montée en gamme, permutation totale (Distinct cross-row en mode CollectionHandling.Array). C’est la structure hiérarchique — quel plat à quel créneau — qui passe sans modification du corpus jouet (06) à l’échelle réelle. Aucune nutrition ici.
Mouvement 2 — la couche nutritionnelle fidèle : linking de composition + restrictions patient. On ajoute ce que le squelette n’avait pas : la variable nutritionnelle liée au plat réellement choisi (PlatId != candidat || Comp == teneur) et les restrictions patient Min/Max par constituant. C’est le chaînon qui relie le corpus réel (07) au raisonnement Z3.

La hiérarchie à 4 niveaux (fidèle à la source)

Patient (restrictions Min/Max par constituant)
   |
   +-- Menu 1 .. Menu N           (un menu = un jour)
          |
          +-- Plat 1 .. Plat P    (un plat par créneau : ordre 1, 2, 3, ...)
                 |
                 +-- Denrées      (composition nutritionnelle réelle, vecteur Ciqual)

La nutrition d’un menu est la somme des compositions de ses plats ; chaque plat apporte le vecteur de teneurs (5 constituants Ciqual) calculé par 07. Le patient impose des bornes Min/Max par constituant (ex : énergie dans une fenêtre kJ, lipides plafonnées) — exactement la classe Restriction { Min, Max } du source.

Note de consolidation. Ce notebook réunit le squelette structurel à l’échelle réelle (Mouvement 1) et le théorème nutritionnel fidèle (Mouvement 2), auparavant éclatés en deux notebooks. La leçon est séquentielle : la structure passe à l’échelle sans effort, c’est l’ajout de la nutrition fidèle (le linking) qui fait exploser l’instance et impose de curer un sous-ensemble (cf Mouvement 2).

0. Dependances et corpus

Le notebook charge le cache mealplan_cache.json produit par [07(07_Meal_Planner_Data_External.ipynb)). Si le cache est absent : executer 07 (ou python download_meal_data.py puis 07). Echec bruyant, pas de corpus de substitution (règle SOTA : on raisonne sur les vraies données nutritionnelles).

Le fork Z3.Linq est charge depuis .deploy/ (script de build unique, cf README) — même build que toute la serie, incluant le support int[][] et CollectionHandling.Array.

#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.IO;
using System.Linq;
using System.Collections.Generic;
using System.Text.Json;
using System.Diagnostics;

// Plat du corpus (miroir du contrat du cache 07 : recipes[].{title,cats,vec}).
public class PlatImport {
    public string Nom { get; set; }
    public int Ordre { get; set; }              // creneau 1..5, derive des cats RecipeML
    public decimal[] Compositions { get; set; } // vec[5] = [Energie kJ, Proteines, Glucides, Lipides, Sel]
}

// Cache solveur-usable produit par le notebook 07 (couche Ciqual x Recettes RecipeML).
var CACHE = Path.Combine("data/meals", "mealplan_cache.json");
if (!File.Exists(CACHE)) {
    Console.WriteLine("[CACHE ABSENT] " + CACHE);
    Console.WriteLine("Executez d'abord 07 (couche de donnees) de bout en bout,");
    Console.WriteLine("ou : python download_meal_data.py puis 07. Echec bruyant (regle SOTA).");
    throw new FileNotFoundException(CACHE);
}
Console.WriteLine($"Cache present : {CACHE} ({new FileInfo(CACHE).Length / 1024} Ko)");

// Derivation du creneau (Ordre 1..5) depuis les cats RecipeML (corpus anglo-saxon).
// 1=entree/appetizer, 2=plat principal/main dish, 3=accompagnement/vegetal, 4=laitage/fromage, 5=dessert.
// Les recettes non-categorisees (cats=['None'] ou ambigu) sont ecartees (pas de fabrication de creneau).
int OrdreFromCats(List<string> cats) {
    var j = string.Join(" ", cats).ToLowerInvariant();
    if (j.Contains("appetizer") || j.Contains("starter") || j.Contains("soup")) return 1;
    if (j.Contains("main dish") || j.Contains("beef") || j.Contains("pork") || j.Contains("chicken") || j.Contains("meat") || j.Contains("fish")) return 2;
    if (j.Contains("vegetable") || j.Contains("salad") || j.Contains("rice") || j.Contains("pasta") || j.Contains("potato") || j.Contains("bread") || j.Contains("side")) return 3;
    if (j.Contains("cheese") || j.Contains("dairy") || j.Contains("yogurt") || j.Contains("cream")) return 4;
    if (j.Contains("dessert") || j.Contains("cake") || j.Contains("cookie") || j.Contains("pie") || j.Contains("fruit") || j.Contains("sweet") || j.Contains("tart")) return 5;
    return 0;
}

var sw = Stopwatch.StartNew();
var root = JsonDocument.Parse(File.ReadAllText(CACHE)).RootElement;
var constituants = root.GetProperty("constituants").EnumerateArray().Select(x => x.GetString()).ToArray();
int C = constituants.Length;
var allPlats = new List<PlatImport>();
foreach (var r in root.GetProperty("recipes").EnumerateArray()) {
    var t = r.GetProperty("title").GetString().Trim();
    var cats = r.GetProperty("cats").EnumerateArray().Select(x => x.GetString()).ToList();
    int o = OrdreFromCats(cats);
    if (o < 1) continue;   // orphan ecarte
    allPlats.Add(new PlatImport {
        Nom = t.Length > 44 ? t.Substring(0, 44) : t,
        Ordre = o,
        Compositions = r.GetProperty("vec").EnumerateArray().Select(x => x.GetDecimal()).ToArray()
    });
}
sw.Stop();
Console.WriteLine($"Cache charge en {sw.Elapsed.TotalSeconds:F1}s : {allPlats.Count} recettes exploitables (sur {root.GetProperty("n_total").GetInt32()} brutes), {C} constituants.");
Console.WriteLine("Constituants : " + string.Join(" | ", constituants.Select((n, i) => $"[{i}] {n.Split(',')[0].Trim()}")));

Cache present : data/meals\mealplan_cache.json (418 Ko)
Cache charge en 0,1s : 2347 recettes exploitables (sur 8286 brutes), 5 constituants.
Constituants : [0] Energie | [1] Protéines | [2] Glucides (g/100 g) | [3] Lipides (g/100 g) | [4] Sel chlorure de sodium (g/100 g)

Mouvement 1 — Le squelette structurel `int[][]` sur le corpus réel (plusieurs centaines de recettes)

Avant la nutrition, on établit la structure : sélectionner, parmi le vrai catalogue de plusieurs centaines de recettes (cache 07 plats, un plan de 7 jours qui respecte le rôle de chaque créneau et la diversité — le tout en LINQ pur sur un int[][]. C’est le théorème hiérarchique du notebook 06 (corpus jouet) porté sans modification à l’échelle réelle, en deux variantes : montée en gamme et permutation totale. Aucune teneur nutritionnelle n’intervient encore — uniquement les index de plats.

1.1 Le corpus réel et sa structure en créneaux

Chaque plat porte un creneau (Ordre, de 1 a 7) : entree, plat principal, accompagnement, laitage/fromage, dessert, etc. C’est cette structure qui rend le problème hiérarchique — un plan de repas n’est pas un sac de plats interchangeables, chaque jour doit servir un plat par creneau, du bon type.

Pour rendre chaque creneau adressable par une plage d’index contigue (exactement comme les bornes de catégorie [entLo, entHi] du notebook 06 jouet), on trie les plats par creneau. On se restreint aux creneaux 1 a 5 (les plus garnis), suffisants pour un plan equilibre de 7 jours.

const int Jours = 7;
const int Creneaux = 5;   // ordres 1..5

// Trie par creneau -> chaque ordre occupe une plage d'index contigue [lo[o]..hi[o]].
var plats = allPlats.Where(p => p.Ordre >= 1 && p.Ordre <= Creneaux)
                      .OrderBy(p => p.Ordre).ThenBy(p => p.Nom).ToList();

var lo = new int[Creneaux + 1];
var hi = new int[Creneaux + 1];
string[] roles = { "", "entree", "plat principal", "accompagnement", "laitage/fromage", "dessert" };
for (int o = 1; o <= Creneaux; o++)
{
    lo[o] = plats.FindIndex(p => p.Ordre == o);
    hi[o] = plats.FindLastIndex(p => p.Ordre == o);
    Console.WriteLine($"  creneau {o} ({roles[o],-16}) : index [{lo[o]}..{hi[o]}]  ({hi[o] - lo[o] + 1} plats)");
}
Console.WriteLine($"\nTotal exploitable : {plats.Count} plats sur {Creneaux} creneaux.");
Console.WriteLine("\nExemples (creneau 1) : " + string.Join(", ",
    plats.Where(p => p.Ordre == 1).Take(4).Select(p => p.Nom.Trim())));

  creneau 1 (entree          ) : index [0..239]  (240 plats)
  creneau 2 (plat principal  ) : index [240..578]  (339 plats)
  creneau 3 (accompagnement  ) : index [579..1442]  (864 plats)
  creneau 4 (laitage/fromage ) : index [1443..1475]  (33 plats)
  creneau 5 (dessert         ) : index [1476..2346]  (871 plats)

Total exploitable : 2347 plats sur 5 creneaux.

Exemples (creneau 1) : 'ncapriata Di Fave (Fava Bean Puree with Gre, "Ketch" a Clam Dip, "The Postman" Italian Fish Soup, "Trick" Kibbeh

1.2 Le théorème hiérarchique `int[][]`

On modelise le plan hebdomadaire comme un tableau en escalier int[][] : Plan[j][c] = l’index (dans la liste triee plats) du plat servi le jour j au creneau c. C’est la même structure que le notebook 06 jouet, mais a l’echelle reelle.

Les helpers sont définis dans une classe statique (Menu) : dans un noyau .NET Interactive, une classe statique persiste d’une cellule a l’autre, contrairement a une fonction locale. Le theoreme et les exercices la reutilisent.

WithBounds impose, pour chaque jour et chaque creneau, que l’index reste dans la plage du bon creneau (Plan[j][c] in [lo[c+1], hi[c+1]]). C’est la contrainte de catégorie, exprimee une fois pour les 7 x 5 = 35 cases.
PrintPlan affiche le plan resolu en remontant des index aux noms de plats.

// Plan hebdomadaire : 7 jours x 5 creneaux, modelise comme int[][] (jagged).
public class WeeklyMenuPlan
{
    public int[][] Plan { get; set; } = new int[7][];
    public WeeklyMenuPlan() { for (int j = 0; j < 7; j++) Plan[j] = new int[5]; }
}

// Classe statique -> persiste entre cellules. Reutilisee par le theoreme ET les exercices.
public static class Menu
{
    public const int Jours = 7;
    public const int Creneaux = 5;

    // Bornes de categorie : Plan[j][c] doit indexer un plat du creneau (c+1).
    public static Theorem<WeeklyMenuPlan> WithBounds(Z3Context ctx, int[] lo, int[] hi)
    {
        var t = ctx.NewTheorem<WeeklyMenuPlan>();
        for (int j = 0; j < Jours; j++)
        {
            int jj = j;
            for (int c = 0; c < Creneaux; c++)
            {
                int cc = c, o = c + 1;
                int basLo = lo[o], basHi = hi[o];   // capture en constantes pour la traduction Z3
                t = t.Where(p => p.Plan[jj][cc] >= basLo && p.Plan[jj][cc] <= basHi);
            }
        }
        return t;
    }

    public static void PrintPlan(WeeklyMenuPlan plan, List<PlatImport> plats)
    {
        for (int j = 0; j < Jours; j++)
        {
            var noms = Enumerable.Range(0, Creneaux).Select(c => plats[plan.Plan[j][c]].Nom.Trim());
            Console.WriteLine($"  Jour {j + 1} : " + string.Join(" | ",
                noms.Select(n => n.Length > 22 ? n.Substring(0, 22) : n)));
        }
    }
}
Console.WriteLine("Helpers definis : WeeklyMenuPlan, Menu.WithBounds, Menu.PrintPlan.");

Helpers definis : WeeklyMenuPlan, Menu.WithBounds, Menu.PrintPlan.

// --- Variante A : montee en gamme (mode Array implicite) ---
// Pour chaque creneau, l'index du plat croit strictement au fil de la semaine :
// une selection ordonnee, sans repetition, qui "monte en gamme" jour apres jour.
using (var ctx = new Z3Context())
{
    var th = Menu.WithBounds(ctx, lo, hi);
    for (int c = 0; c < Creneaux; c++)
    {
        int cc = c;
        for (int j = 0; j < Jours - 1; j++)
        {
            int jj = j;
            th = th.Where(p => p.Plan[jj][cc] < p.Plan[jj + 1][cc]);
        }
    }
    var sw = Stopwatch.StartNew();
    var plan = th.Solve();
    sw.Stop();
    Console.WriteLine($"[A] Montee en gamme resolue en {sw.Elapsed.TotalMilliseconds:F0} ms :\n");
    if (plan != null) Menu.PrintPlan(plan, plats); else Console.WriteLine("  UNSAT");
}

[A] Montee en gamme resolue en 86 ms :

  Jour 1 : Ajoblanco De Malaga (G | "Cheese" Fricadelle | 'sense and Sensibility | 3-Step Cheesecake | 'gimme Both' Pumpkin-P
  Jour 2 : Ajvar | "Our Chicken Nuggets" | "Faux" Sourdough | Acapulco Rice | "21" Club Rice Pudding
  Jour 3 : Ajvar (Roasted Peppers | "Philly-Style" White P | "Field of Greens" Wilt | Amaretto Cheesecake | "Better Than Sex" Dess
  Jour 4 : Akkra (Bean Fritters) | "The Original" Lamb Sp | "Foolproof" Sourdough  | Amaretto Chocolate Che | "Binx" Gardner's Cream
  Jour 5 : Alaska Sourest Dough | (Sort-Of) Sweet and So | "Gold Room" Scones | Ananas a la Creme (Cre | "Brown Bag" French App
  Jour 6 : Albondigas (Spanish) | 1-Pot Pastitsio Goes L | "Gourmet" Pizza Dough | Ann's White Chocolate  | "Foot in the Fire" Cho
  Jour 7 : Albondigas Soup (Meatb | 1-Pot: Pastitsio Goes  | "Herman" Yeast Starter | Annemarie's German App | "Instant" Chocolate Mo

Interpretation — variante A

La contrainte de montee en gamme (Plan[j][c] < Plan[j+1][c]) force, pour chaque creneau, une suite d’index strictement croissante sur les 7 jours. Comme les plats sont tries par creneau, cela revient a parcourir le catalogue dans l’ordre, sans jamais reservir le même plat. Z3.Linq traduit le int[][] en variables entieres et resout en LINQ pur, sans expansion manuelle des paires.

// --- Variante B : permutation totale (CollectionHandling.Array EXPLICITE, Distinct cross-row) ---
// Chaque creneau est servi 7 fois dans la semaine, sans aucune repetition :
// Z3Methods.Distinct s'applique directement aux acces cross-row d'un int[][]
// (meme marqueur que les colonnes d'un Sudoku) -> une contrainte globale SMT.
using (var ctxPerm = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array })
{
    var perm = Menu.WithBounds(ctxPerm, lo, hi);
    for (int c = 0; c < Creneaux; c++)
    {
        int cc = c;
        perm = perm.Where(p => Z3Methods.Distinct(
            p.Plan[0][cc], p.Plan[1][cc], p.Plan[2][cc], p.Plan[3][cc],
            p.Plan[4][cc], p.Plan[5][cc], p.Plan[6][cc]));
    }
    var sw = Stopwatch.StartNew();
    var planPerm = perm.Solve();
    sw.Stop();
    Console.WriteLine($"[B] Permutation totale (Distinct cross-row) resolue en {sw.Elapsed.TotalMilliseconds:F0} ms :\n");
    if (planPerm != null) Menu.PrintPlan(planPerm, plats); else Console.WriteLine("  UNSAT");
}

[B] Permutation totale (Distinct cross-row) resolue en 27 ms :

  Jour 1 : Ajoblanco De Malaga (G | "Cheese" Fricadelle | 'sense and Sensibility | 3-Step Cheesecake | 'gimme Both' Pumpkin-P
  Jour 2 : Ajvar | "Our Chicken Nuggets" | "Faux" Sourdough | Acapulco Rice | "21" Club Rice Pudding
  Jour 3 : Ajvar (Roasted Peppers | "Philly-Style" White P | "Field of Greens" Wilt | Amaretto Cheesecake | "Better Than Sex" Dess
  Jour 4 : Akkra (Bean Fritters) | "The Original" Lamb Sp | "Foolproof" Sourdough  | Amaretto Chocolate Che | "Binx" Gardner's Cream
  Jour 5 : Alaska Sourest Dough | 1-Pot: Pastitsio Goes  | "Gold Room" Scones | Ananas a la Creme (Cre | "Brown Bag" French App
  Jour 6 : Albondigas (Spanish) | (Sort-Of) Sweet and So | "Gourmet" Pizza Dough | Ann's White Chocolate  | "Foot in the Fire" Cho
  Jour 7 : Albondigas Soup (Meatb | 1-Pot Pastitsio Goes L | "Herman" Yeast Starter | Annemarie's German App | "Instant" Chocolate Mo

Interpretation — variante B

La variante B n’impose plus d’ordre, seulement la diversite : chaque creneau est servi sans repetition sur la semaine. Z3Methods.Distinct appliquee aux acces cross-row d’un int[][] produit une seule contrainte SMT globale par creneau (et non C(7,2) inegalites deux-a-deux) — exactement le mécanisme qui modelise les colonnes d’un Sudoku.

Le mode CollectionHandling.Array est ici explicite : il indique a Z3.Linq de reifier le tableau comme un tableau SMT, ce qui rend les acces cross-row adressables par Distinct. C’est le levier qui fait passer le int[][] du statut de simple structure de données a celui de variable de decision hiérarchique.

Mouvement 2 — La nutrition fidèle force la curation

Le squelette structurel passe à l’échelle réelle sans effort (Z3 résout les deux variantes en quelques dizaines de millisecondes sur le corpus réel). On ajoute maintenant la couche nutritionnelle fidèle au Demo2 : le linking de composition (la variable de teneur liée au plat réellement choisi) et les restrictions patient Min/Max sur la somme par menu. Mais le linking, à l’échelle complète, génère 7 × 5 × R × C assertions (R recettes, C constituants) — l’instance explose. On cure donc d’abord un sous-ensemble tractable, en préservant la structure du théorème (port fidèle de PlanificateurDeMenus.Create).

2.1 Curation d’un sous-ensemble tractable

La source pose le theoreme sur plusieurs centaines de recettes x 5 constituants x 7 menus x 5 creneaux. Le linking de composition genere alors 7 x 5 x R x C (R recettes, C constituants) assertions — l’instance explose (c’est précisément le problème de convergence a l’echelle, objet de 09 (convergence a l’echelle)). Le corps de l’issue #4617 le prevoit : on cure d’abord un sous-ensemble.

On reduit donc a 2 menus x 3 creneaux, 5 candidats par creneau, et 3 constituants cles (energie kJ, proteines, lipides). Le theoreme reste fidele dans sa structure ; seules les dimensions sont reduites pour rester pedagogiquement lisible et resoluble en quelques secondes.

// --- Parametres du sous-ensemble cure ---
const int NbMenus = 2;          // 2 jours
const int NbPlats = 3;          // 3 creneaux (ordre 1, 2, 3)
const int CandParOrdre = 5;     // 5 candidats par creneau

// 3 constituants cles du cache 07 (ordre fixe : [0] Energie kJ, [1] Proteines, [3] Lipides).
int cEnergie = 0;
int cProt    = 1;
int cLip     = 3;
int[] CONST  = new[]{ cEnergie, cProt, cLip };
string[] NOMK = new[]{ "energie(kJ)", "proteines(g)", "lipides(g)" };
Console.WriteLine("Constituants suivis :");
foreach (var ci in CONST) Console.WriteLine($"  [{ci}] {constituants[ci].Trim()}");

// Pool curee : CandParOrdre plats par ordre 1..NbPlats, re-indexes 0..(NbPlats*CandParOrdre-1).
var pool = new List<PlatImport>();
for (int o = 1; o <= NbPlats; o++)
    pool.AddRange(allPlats.Where(p => p.Ordre == o).Take(CandParOrdre));
Console.WriteLine($"\nPool curee : {pool.Count} plats ({NbPlats} creneaux x {CandParOrdre} candidats)");

// teneur arrondie a l'entier (arithmetique entiere Z3) ; helpers d'indexation aplatie
int Teneur(int poolIdx, int constIdx) => (int)Math.Round(pool[poolIdx].Compositions[constIdx]);
int Slot(int m, int p) => m * NbPlats + p;   // ligne aplatie pour le slot (menu m, creneau p)
Console.WriteLine("\nApercu (creneau : candidats -> energie kJ) :");
for (int p = 0; p < NbPlats; p++) {
    var noms = Enumerable.Range(p*CandParOrdre, CandParOrdre)
        .Select(i => $"{pool[i].Nom.Trim()}({Teneur(i, cEnergie)})");
    Console.WriteLine($"  creneau {p+1} : " + string.Join(", ", noms));
}

Constituants suivis :
  [0] Energie, Règlement UE N° 1169/2011 (kJ/100 g)
  [1] Protéines, N x facteur de Jones (g/100 g)
  [3] Lipides (g/100 g)

Pool curee : 15 plats (3 creneaux x 5 candidats)

Apercu (creneau : candidats -> energie kJ) :
  creneau 1 : 'ncapriata Di Fave (Fava Bean Puree with Gre(5922), 4 B's Restaurant Tomato Soup(3409), 5-Minute Broccoli Soup(6415), 7 Layer Dip(11374), 90-Minute Soft Pretzels(7426)
  creneau 2 : (Sort-Of) Sweet and Sour Chicken (Also Good(1018), 1-Pot Pastitsio Goes Light(15054), 1-Pot: Pastitsio Goes Light(15054), 10 Minute Szechuan Chicken(1178), 16th-Street Stew(10678)
  creneau 3 : 'sense and Sensibility' Scones(5329), ( From Bread Mix ) Big Soft Pretzels(4421), ( From Bread Mix ) Cinnamon Rolls(13568), 1-2-3 Meurbeteig Dough (Mellow Dough)(14026), 1-Pot Creamy Chicken Noodle Casserole(3471)

2.2 Le modèle : 3 tableaux `int[][]`

Le Demo2 d’origine modelise un graphe d’objets (Menu[] contenant Plat[] contenant PlatId + Compositions[]). Le binding Z3.Linq de la serie expose, lui, des tableaux int[][] (cf 05) : c’est l’encodage index que le fork resout en notebook. On reproduit donc la sémantique de la source avec trois int[][] :

Tableau	Forme	Rôle
`PlatId[m][p]`	`[NbMenus][NbPlats]`	index (dans la pool) du plat choisi au creneau (m, p)
`Comp[slot][k]`	`[NbMenus*NbPlats][3]`	composition du plat choisi a ce slot (variable liee par disjonction)
`MenuNut[m][k]`	`[NbMenus][3]`	somme nutritionnelle du menu m (ce que le patient contraint)

Comp est l’aux variable qui resout l’impossibilite d’indexer un tableau C# par une variable Z3 (on ne peut pas ecrire Plats[PlatId[m][p]]) : on la lie au bon plat par une disjonction (section 3.3), exactement la technique de la source.

public class PlanRepas {
    public int[][] PlatId  { get; set; }   // [NbMenus][NbPlats]      : plat choisi par creneau
    public int[][] Comp    { get; set; }   // [NbMenus*NbPlats][3]    : composition liee du slot
    public int[][] MenuNut { get; set; }   // [NbMenus][3]            : somme par menu
    public PlanRepas() {
        PlatId  = Enumerable.Range(0, 2).Select(_ => new int[3]).ToArray();
        Comp    = Enumerable.Range(0, 6).Select(_ => new int[3]).ToArray();
        MenuNut = Enumerable.Range(0, 2).Select(_ => new int[3]).ToArray();
    }
}
Console.WriteLine("Modele PlanRepas defini (PlatId, Comp, MenuNut).");

Modele PlanRepas defini (PlatId, Comp, MenuNut).

2.3 Le patient et ses restrictions

Fidele a la classe Patient { Restriction[] Restrictions } du source : chaque restriction porte un Min et un Max par constituant (-1 = pas de borne). Ici, le patient impose une fenêtre energetique par menu et un plafond de lipides.

// Restrictions patient (fidele a Restriction { Min, Max }, -1 = pas de borne), par MENU.
// Echelle : cache 07 en kJ/100 g (Energie Ciqual) sommees sur les 3 plats du menu.
// ( bornes rescalees de kcal -> kJ lors du rewire sur le cache 07 : x4,184 )
int energieMin = 3347;   // ~800 kcal cumules minimum par menu
int energieMax = 10878;  // ~2600 kcal cumules maximum par menu
int protMin    = 30;     // proteines minimum par menu (g)
int lipMax     = 600;    // lipides maximum par menu (g)
Console.WriteLine($"Patient : energie in [{energieMin}, {energieMax}] kJ, proteines >= {protMin} g, lipides <= {lipMax} g (par menu)");

Patient : energie in [3347, 10878] kJ, proteines >= 30 g, lipides <= 600 g (par menu)

3.1 -> 3.5 Construction du theoreme (port fidele de `Create`)

Les cinq familles de contraintes reproduisent PlanificateurDeMenus.Create (source lignes 38-101) :

Bornes = ordre : PlatId[m][p] indexe un plat du creneau (p+1) — la source impose allPlats[rid].Ordre == p+1 ; ici la partition de la pool par ordre l’encode dans les bornes.
Variete : Z3Methods.Distinct(...) sur tous les slots — pas deux fois le même plat (source : Distinct sur la grille des PlatId).
Linking composition : PlatId[m][p] != cand || Comp[slot][k] == teneur(cand, k) — lie la variable de composition au plat reellement choisi (source lignes 71-74).
Somme par menu : MenuNut[m][k] == somme_p Comp[slot(m,p)][k] (source lignes 84-85).
Restrictions patient : Min < MenuNut[m][k] < Max selon les bornes du patient (source lignes 90-99).

var sw = Stopwatch.StartNew();
PlanRepas sol = null;
using (var ctx = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array })
{
    var th = ctx.NewTheorem<PlanRepas>();

    // (1) bornes = contrainte d'ordre : slot p -> candidats du creneau (p+1)
    for (int m = 0; m < NbMenus; m++) for (int p = 0; p < NbPlats; p++) {
        int mm = m, pp = p, lo = p * CandParOrdre, hi = p * CandParOrdre + CandParOrdre - 1;
        th = th.Where(x => x.PlatId[mm][pp] >= lo && x.PlatId[mm][pp] <= hi);
    }

    // (2) variete : Distinct global sur les 6 slots
    th = th.Where(x => Z3Methods.Distinct(
        x.PlatId[0][0], x.PlatId[0][1], x.PlatId[0][2],
        x.PlatId[1][0], x.PlatId[1][1], x.PlatId[1][2]));

    // (3) linking composition : PlatId[m][p] != cand || Comp[slot][k] == teneur(cand, k)
    for (int m = 0; m < NbMenus; m++) for (int p = 0; p < NbPlats; p++) {
        int slot = Slot(m, p), mm = m, pp = p;
        for (int cand = p * CandParOrdre; cand < p * CandParOrdre + CandParOrdre; cand++) {
            int cc = cand;
            for (int k = 0; k < CONST.Length; k++) {
                int kk = k, val = Teneur(cand, CONST[k]);
                th = th.Where(x => x.PlatId[mm][pp] != cc || x.Comp[slot][kk] == val);
            }
        }
    }

    // (4) somme par menu : MenuNut[m][k] == Comp[s0][k] + Comp[s1][k] + Comp[s2][k]
    for (int m = 0; m < NbMenus; m++) for (int k = 0; k < CONST.Length; k++) {
        int mm = m, kk = k, s0 = Slot(m, 0), s1 = Slot(m, 1), s2 = Slot(m, 2);
        th = th.Where(x => x.MenuNut[mm][kk] == x.Comp[s0][kk] + x.Comp[s1][kk] + x.Comp[s2][kk]);
    }

    // (5) restrictions patient : energie in [min,max], proteines >= min, lipides <= max (par menu)
    for (int m = 0; m < NbMenus; m++) {
        int mm = m;
        th = th.Where(x => x.MenuNut[mm][0] >= energieMin && x.MenuNut[mm][0] <= energieMax);
        th = th.Where(x => x.MenuNut[mm][1] >= protMin);
        th = th.Where(x => x.MenuNut[mm][2] <= lipMax);
    }

    sol = th.Solve();
}
sw.Stop();
Console.WriteLine($"Theoreme resolu en {sw.Elapsed.TotalMilliseconds:F0} ms\n");
if (sol == null) {
    Console.WriteLine("UNSAT : aucun plan ne satisfait les restrictions du patient sur cette pool.");
} else {
    for (int m = 0; m < NbMenus; m++) {
        Console.WriteLine($"== Menu {m + 1} ==  energie={sol.MenuNut[m][0]} kJ | "
            + $"proteines={sol.MenuNut[m][1]} g | lipides={sol.MenuNut[m][2]} g");
        for (int p = 0; p < NbPlats; p++) {
            var plat = pool[sol.PlatId[m][p]];
            Console.WriteLine($"   creneau {p + 1} : {plat.Nom.Trim(),-30} "
                + $"(kJ={Teneur(sol.PlatId[m][p], cEnergie)}, prot={Teneur(sol.PlatId[m][p], cProt)}, lip={Teneur(sol.PlatId[m][p], cLip)})");
        }
    }
}

Theoreme resolu en 70 ms

== Menu 1 ==  energie=10571 kJ | proteines=111 g | lipides=119 g
   creneau 1 : 'ncapriata Di Fave (Fava Bean Puree with Gre (kJ=5922, prot=58, lip=73)
   creneau 2 : 10 Minute Szechuan Chicken     (kJ=1178, prot=11, lip=15)
   creneau 3 : 1-Pot Creamy Chicken Noodle Casserole (kJ=3471, prot=42, lip=31)
== Menu 2 ==  energie=9756 kJ | proteines=43 g | lipides=111 g
   creneau 1 : 4 B's Restaurant Tomato Soup   (kJ=3409, prot=16, lip=63)
   creneau 2 : (Sort-Of) Sweet and Sour Chicken (Also Good (kJ=1018, prot=3, lip=0)
   creneau 3 : 'sense and Sensibility' Scones (kJ=5329, prot=24, lip=48)

2.4 Vérification : les restrictions sont-elles vraiment respectées ?

Un solveur garantit les contraintes par construction — mais on verifie independamment (re-calcul hors Z3) que chaque menu respecte la fenêtre du patient. C’est la différence entre croire le solveur et prouver le résultat.

if (sol == null) {
    Console.WriteLine("Pas de solution a verifier (UNSAT).");
} else {
    bool ok = true;
    for (int m = 0; m < NbMenus; m++) {
        // re-somme directe depuis la pool (independante des variables Z3)
        int e = 0, pr = 0, li = 0;
        for (int p = 0; p < NbPlats; p++) {
            e  += Teneur(sol.PlatId[m][p], cEnergie);
            pr += Teneur(sol.PlatId[m][p], cProt);
            li += Teneur(sol.PlatId[m][p], cLip);
        }
        bool eOk = e >= energieMin && e <= energieMax, pOk = pr >= protMin, lOk = li <= lipMax;
        bool match = e == sol.MenuNut[m][0] && pr == sol.MenuNut[m][1] && li == sol.MenuNut[m][2];
        ok &= eOk && pOk && lOk && match;
        Console.WriteLine($"Menu {m+1} : recalc energie={e}({(eOk?"OK":"HORS")}), prot={pr}({(pOk?"OK":"HORS")}), "
            + $"lip={li}({(lOk?"OK":"HORS")}) ; coherent avec MenuNut={(match?"oui":"NON")}");
    }
    Console.WriteLine(ok ? "\nVERIFIE : toutes les restrictions patient sont respectees."
                         : "\nINCOHERENCE detectee (a investiguer).");
}

Menu 1 : recalc energie=10571(OK), prot=111(OK), lip=119(OK) ; coherent avec MenuNut=oui
Menu 2 : recalc energie=9756(OK), prot=43(OK), lip=111(OK) ; coherent avec MenuNut=oui

VERIFIE : toutes les restrictions patient sont respectees.

Exercices

Quatre exercices pour s’approprier le capstone, du squelette structurel (Mouvement 1) au théorème hiérarchique à restrictions patient (Mouvement 2). Les stubs s’exécutent tels quels (ils n’échouent pas) ; complétez le corps marqué TODO.

Exercice 1 — Diversité des entrées sur jours consécutifs (structure)

Renforcez le théorème structurel du Mouvement 1 : interdisez de servir deux fois la même entrée (créneau 1) sur deux jours consécutifs. Repartez de Menu.WithBounds(ctx, lo, hi) et ajoutez la contrainte d’inégalité consécutive.

Indice : pour j de 0 à Jours-2, ajoutez p.Plan[j][0] != p.Plan[j+1][0].

// Exercice 1 — Diversite renforcee : pas deux fois la meme entree (creneau 1)
//              sur deux jours CONSECUTIFS.
//
// Indice : ajoutez, pour j de 0 a Jours-2, une contrainte
//          p.Plan[j][0] != p.Plan[j+1][0]  sur un theoreme construit avec Menu.WithBounds.
// Etape 1 : creez un Z3Context (mode Array implicite suffit).
// Etape 2 : partez de Menu.WithBounds(ctx, lo, hi), ajoutez la contrainte d'inegalite consecutive.
// Etape 3 : resolvez et affichez avec Menu.PrintPlan.
//
// TODO etudiant : completez ci-dessous.
Console.WriteLine("Exercice 1 a completer : diversite des entrees sur jours consecutifs.");

Exercice 1 a completer : diversite des entrees sur jours consecutifs.

Exercice 2 — Une restriction qui rend le problème insatisfiable

Le patient devient diabetique : imposez un plafond energetique strict par menu (ex. energieMax = 1500) et reconstruisez le theoreme. Observez si Z3 trouve encore un plan ou repond UNSAT, et expliquez pourquoi (quel creneau porte l’essentiel de l’energie kJ ?).

Indice : recopiez le bloc de la section 3.5 en changeant energieMax, ou parametrez-le.

// Exercice 2 : trouver le plafond energetique qui bascule SAT -> UNSAT.
// TODO etudiant : reconstruire le theoreme avec un energieMax plus strict et reporter le verdict.
int ExerciceUnsatThreshold()
{
    // Etape 1 : choisir un energieMax candidat (ex. 1500)
    // Etape 2 : reconstruire le theoreme (sections 1-5 bornes/Distinct/linking/somme/restrictions)
    //           en remplacant la borne energieMax
    // Etape 3 : retourner le plus grand energieMax pour lequel le probleme est UNSAT (ou -1 si toujours SAT)
    Console.WriteLine("Exercice 2 a completer");
    return -1;
}
ExerciceUnsatThreshold();

Exercice 2 a completer

Exercice 3 — Passer a 3 menus (tractabilite)

Portez NbMenus de 2 a 3 (3 jours). Adaptez la taille des tableaux du modèle PlanRepas (PlatId [3][3], Comp [9][3], MenuNut [3][3]) et le Distinct (9 slots). Mesurez le temps de resolution : reste-t-il de l’ordre de la seconde ? C’est un premier pas vers 09 (convergence a l’echelle) (convergence a l’echelle).

Indice : Z3Methods.Distinct accepte une liste d’arguments ; enumerez les 9 PlatId[m][p].

// Exercice 3 : etendre a NbMenus = 3 et mesurer le temps de resolution.
// TODO etudiant : adapter le modele (tailles), le Distinct (9 slots) et resoudre.
double ExerciceTroisMenus()
{
    // Etape 1 : definir un modele PlanRepas3 avec PlatId[3][3], Comp[9][3], MenuNut[3][3]
    // Etape 2 : reconstruire les 5 familles de contraintes pour 3 menus
    // Etape 3 : chronometrer Solve() et retourner le temps en millisecondes (ou -1 si UNSAT)
    Console.WriteLine("Exercice 3 a completer");
    return -1.0;
}
ExerciceTroisMenus();

Exercice 3 a completer

Exercice 4 — Ajouter un quatrieme constituant suivi

Le patient surveille aussi le sel (Sel chlorure de sodium). Ajoutez ce constituant a CONST (repere par nom), etendez Comp/MenuNut a 4 colonnes, et imposez un plafond de sel par menu. Le plan reste-t-il satisfiable ?

Indice : constituants.Select((n,i) => (n,i)).First(x => x.n.ToLowerInvariant().Contains("sel chlorure")).

// Exercice 4 : suivre un 4e constituant (sel) et lui imposer un plafond par menu.
// TODO etudiant : etendre CONST a 4 elements et ajouter la restriction de sel.
int ExerciceConstituantSel()
{
    // Etape 1 : reperer l'index du constituant "Sel chlorure de sodium"
    // Etape 2 : etendre CONST/Comp/MenuNut a 4 colonnes
    // Etape 3 : ajouter Where(MenuNut[m][3] <= selMax) et retourner le sel max du menu 1 de la solution
    Console.WriteLine("Exercice 4 a completer");
    return 0;
}
ExerciceConstituantSel();

Exercice 4 a completer

Conclusion

Ce notebook a porté fidèlement le cœur solveur du Demo2 (PlanificateurDeMenus.Create) en deux mouvements sur le corpus réel Ciqual × Recettes construit par 07 (couche de données) :

Mouvement 1 — la structure prime sur l’échelle. Le même int[][] modélise un plan de 7 jours sur un vrai catalogue de plusieurs centaines de plats ; c’est la structure en créneaux (et non le nombre de plats) qui fait du problème un problème hiérarchique. Bornes de catégorie, montée en gamme et permutation totale (Distinct cross-row, CollectionHandling.Array) passent sans modification du corpus jouet (06) au réel — Z3 résout en quelques dizaines de millisecondes.
Mouvement 2 — le théorème fidèle à 4 niveaux. Patient → Menus → Plats → Denrées, avec le linking de composition (la variable nutritionnelle liée au plat réellement choisi) et les restrictions patient Min/Max sur la somme par menu — le chaînon nutritionnel que le squelette n’avait pas. À l’échelle complète, le linking explose (un nombre eleve d’assertions) : on a curé un sous-ensemble (2 menus, 3 créneaux, 5 candidats, 3 constituants) pour rester résoluble en quelques secondes, en préservant la structure du théorème.

La place de ce notebook dans le capstone #4617 :

Slice	Notebook	Apport
A	07	construction du corpus (cache Ciqual x Recettes, 0 SMT)
C	08 (ce notebook)	squelette structurel réel + théorème hiérarchique à restrictions patient (port fidèle)
B+D	09	convergence à l’échelle réelle (RecipeML × Ciqual, trois encodages comparés)

Vers la convergence à l’échelle : le passage du sous-ensemble curé au corpus complet fait exploser le linking — c’est le problème de convergence à l’échelle que la 09 (convergence a l echelle) adresse, en reformulant la contrainte nutritionnelle en one-hot pseudo-booléen (le seul encodage qui reste tractable là où la disjonction-liée naïve explose dès la construction).

Série SMT / Z3.Linq — voir le README pour le parcours complet.

Retour au sommet