Z3-Python-16c — Meal-Planner : capstone patient (restrictions nutritionnelles)

Compagnon « capstone » de la jambe Python-large #1206 : 16 (modélisation jouet) → 16b (couche de données réelles) → 16c (ce notebook) : le patient → 16d (convergence à l’échelle).

Le capstone : un patient impose des restrictions nutritionnelles (énergie bornée, protéines minimum, lipides maximum) et le solveur doit composer un menu multi-jours qui les satisfait. Port fidèle du C# 08_Meal_Planner_Patient_Capstone (Z3-Linq2Z3).

Patient ──> Menu (1 jour) ──> Plat (1 créneau) ──> Denrées (nutrition Ciqual)
            [energie?]       [entrée | plat | accomp.]

Deux mouvements : (1) un squelette structural à grande échelle (semaine 7×5, sans nutrition) ; (2) le capstone patient curé (nutrition contrainte).

0. Dépendances : le cache produit par 16b

Ce notebook consomme le cache solveur-usable régénéré par 16b (data/meals/mealplan_cache.json). Pas de solveur ici tant que le cache est absent — échec bruyant (règle SOTA : pas de corpus de substitution).

# Chargement du cache 16b + derivation du creneau (Ordre 1..5) depuis les cats RecipeML.
import json, time
from z3 import Solver, Int, Or, Distinct, sat, Implies
from pathlib import Path

def _meal_base():
    """Ancrage CWD-independant : le corpus vit dans Z3-API/data/meals/ (mirror Python du pin C# #8901)."""
    cwd = Path.cwd().resolve()
    if cwd.name == "Z3-API":
        return cwd / "data" / "meals"
    for _anc in (cwd, *cwd.parents):
        _c = _anc / "MyIA.AI.Notebooks" / "SymbolicAI" / "SMT" / "Z3-API" / "data" / "meals"
        if _c.exists():
            return _c
    raise FileNotFoundError("Serie Z3-API introuvable depuis " + str(cwd))

CACHE = _meal_base() / "mealplan_cache.json"
if not CACHE.exists():
    print(f"[CACHE ABSENT] {CACHE}")
    print("Executez d'abord Z3-Python-16b-Meal-Planner-Data-External (couche de donnees).")
    raise FileNotFoundError(CACHE)
print(f"Cache present : {CACHE.relative_to(_meal_base().parents[1])} ({CACHE.stat().st_size/1024:.0f} Ko)")

root = json.loads(CACHE.read_text(encoding="utf-8"))
constituants = root["constituants"]; C = len(constituants)

class Plat:
    __slots__ = ("nom", "ordre", "comp")
    def __init__(self, nom, ordre, comp): self.nom, self.ordre, self.comp = nom, ordre, comp

def ordre_from_cats(cats):
    j = " ".join(cats).lower()
    if any(k in j for k in ("appetizer","starter","soup")): return 1
    if any(k in j for k in ("main dish","beef","pork","chicken","meat","fish")): return 2
    if any(k in j for k in ("vegetable","salad","rice","pasta","potato","bread","side")): return 3
    if any(k in j for k in ("cheese","dairy","yogurt","cream")): return 4
    if any(k in j for k in ("dessert","cake","cookie","pie","fruit","sweet","tart")): return 5
    return 0

t0 = time.perf_counter()
all_plats = []
for r in root["recipes"]:
    t = r["title"].strip()[:44]                 # tronque a 44 (miroir C#)
    o = ordre_from_cats(r["cats"])
    if o < 1: continue                          # orphelin ecarte
    all_plats.append(Plat(t, o, [float(x) for x in r["vec"]]))
print(f"Cache charge en {time.perf_counter()-t0:.2f}s : {len(all_plats)} recettes exploitables "
      f"(sur {root['n_total']} brutes), {C} constituants.")
print("Constituants : " + " | ".join(f"[{i}] {n.split(',')[0].strip()}" for i,n in enumerate(constituants)))

Cache present : data\meals\mealplan_cache.json (89 Ko)
Cache charge en 0.00s : 447 recettes exploitables (sur 1465 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 — squelette structural à grande échelle (7 jours × 5 créneaux)

Avant la nutrition, le squelette : une semaine de 7 jours × 5 créneaux, où chaque créneau choisit un plat dans sa catégorie. C’est l’occasion d’examiner l’idiome « tableau imbriqué » (int[][]) en SMT — et pourquoi le binding C# Z3.Linq le réifie via CollectionHandling.Array tandis qu’en z3-py on déclare simplement une grille plate de Int.

Divergence de port (honnête) : le C# pose DefaultCollectionHandling = CollectionHandling.Array pour traduire int[][] en un SMT Array (théorie des tableaux de McCarthy, Select/Store). z3-py n’impose pas cette couche : on déclare une list[list[Int]] — chaque cellule est une variable Int indépendante. Fonctionnellement équivalent pour ce squelette ; la vraie théorie des Array est l’objet du notebook 15.

1.1 Corpus + créneaux : pourquoi trier par Ordre

# Semaine 7x5 : on groupe les plats par creneau, ranges contigus [lo,hi] par categorie.
JOURS, CRENEAUX = 7, 5
# tri par (ordre, nom) pour des ranges contigus par creneau (le tri n'affecte que lo/hi, pas le modele M2).
plats = sorted([p for p in all_plats], key=lambda p: (p.ordre, p.nom))
lo, hi = [], []
for o in range(1, CRENEAUX + 1):
    idxs = [i for i, p in enumerate(plats) if p.ordre == o]
    lo.append(idxs[0] if idxs else 0)
    hi.append(idxs[-1] if idxs else -1)
print(f"{len(plats)} plats ranges en 5 creneaux :")
for o in range(CRENEAUX):
    n = 0 if hi[o] < lo[o] else hi[o] - lo[o] + 1
    print(f"  creneau {o+1} (ordre {o+1}) : [{lo[o]}..{hi[o]}] ({n} candidats)")

447 plats ranges en 5 creneaux :
  creneau 1 (ordre 1) : [0..45] (46 candidats)
  creneau 2 (ordre 2) : [46..99] (54 candidats)
  creneau 3 (ordre 3) : [100..227] (128 candidats)
  creneau 4 (ordre 4) : [228..237] (10 candidats)
  creneau 5 (ordre 5) : [238..446] (209 candidats)

1.2 Le théorème hiérarchique + deux variantes

with_bounds encadre chaque créneau dans sa range contigue. Variante A : montée en gamme (chaque jour fait mieux que le précédent, même créneau). Variante B : variété totale (Distinct croisé sur la colonne d’un même créneau, tous jours confondus).

# M1 : squelette 7x5 + Variante A (montee en gamme) + Variante B (Distinct cross-row).
def with_bounds(plan):
    cs = []
    for jj in range(JOURS):
        for cc in range(CRENEAUX):
            cs.append(plan[jj][cc] >= lo[cc]); cs.append(plan[jj][cc] <= hi[cc])
    return cs
def print_plan(plan, mdl, titre):
    print(titre)
    for jj in range(JOURS):
        row = []
        for cc in range(CRENEAUX):
            v = mdl.eval(plan[jj][cc]).as_long()
            row.append(f"{plats[v].nom[:14]:14}")
        print(f"  J{jj+1}: " + " | ".join(row))

t0 = time.perf_counter()
# Variante A : montee en gamme, chaque jour > precedent (meme creneau)
sA = Solver()
planA = [[Int(f"a_j{jj}_c{cc}") for cc in range(CRENEAUX)] for jj in range(JOURS)]
for c in with_bounds(planA): sA.add(c)
for jj in range(JOURS - 1):
    for cc in range(CRENEAUX):
        sA.add(planA[jj][cc] < planA[jj+1][cc])
satA = (sA.check() == sat); mA = sA.model() if satA else None
print(f"[A] Montee en gamme : {'resolue' if satA else 'UNSAT'} en {(time.perf_counter()-t0)*1000:.0f} ms")

# Variante B : Distinct cross-row par creneau (tous jours differents dans la meme categorie)
t1 = time.perf_counter()
sB = Solver()
planB = [[Int(f"b_j{jj}_c{cc}") for cc in range(CRENEAUX)] for jj in range(JOURS)]
for c in with_bounds(planB): sB.add(c)
for cc in range(CRENEAUX):
    if hi[cc] >= lo[cc] and (hi[cc] - lo[cc] + 1) >= JOURS:
        sB.add(Distinct(*[planB[jj][cc] for jj in range(JOURS)]))
satB = (sB.check() == sat); mB = sB.model() if satB else None
print(f"[B] Permutation totale (Distinct cross-row) : {'resolue' if satB else 'UNSAT'} en {(time.perf_counter()-t1)*1000:.0f} ms")
if satA: print_plan(planA, mA, "\n== Variante A (montee en gamme) ==")

[A] Montee en gamme : resolue en 44 ms
[B] Permutation totale (Distinct cross-row) : resolue en 10 ms

== Variante A (montee en gamme) ==
  J1: 'ncapriata Di  | (Sort-Of) Swee | 'sense and Sen | 3-Step Cheesec | #1 Lemon Bars 
  J2: 4 B's Restaura | 1-Pot Pastitsi | ( From Bread M | Acapulco Rice  | #10 Cake      
  J3: 5-Minute Brocc | 1-Pot: Pastits | ( From Bread M | Almond Cheesec | $100 Chocolate
  J4: 7 Layer Dip    | 10 Minute Szec | 1-2-3 Meurbete | Almond Fried I | 'gimme Both' P
  J5: 90-Minute Soft | 16th-Street St | 1-Pot Creamy C | Almond Ice Cre | (Sort of Light
  J6: Abadoo's Walnu | 19-Alarm Chili | 1-Pot: Creamy  | Almond Poppyse | 1 Egg Butter S
  J7: Abalone Soup # | 2 Pungent Bbq  | 10-Minute Lasa | Almond, Lemon  | 1,000 Calorie-

Mouvement 2 — le capstone patient : la nutrition force la curation

Le squelette M1 ignore la nutrition. Lui ajouter des restrictions patient à l’échelle pleine (7×5×R×C) ferait exploser le modèle. D’où la curation : on réduit à 2 menus × 3 créneaux × 5 candidats × 3 constituants — un sous-ensemble à taille humaine où le capstone reste lisible.

Note de fidélité : le C# 08 référence dans sa prose une classe upstream Patient { Restriction[] Restrictions } (chaque restriction porte un Min/Max par constituant, -1 = pas de borne), qui n’existe pas dans ce dépôt (fork externe Z3.LinqBinding). Le notebook 08 lui-même inline le patient comme quatre entiers et n’a aucune classe Patient/ Restriction. Ce port Python reste fidèle à 08 (patient inline) plutôt que de reconstruire la classe upstream absente — ne pas lui attribuer une structure que 08 n’a pas.

2.1 Curation : 2 menus × 3 créneaux × 5 candidats × 3 constituants

# Curation : pool de 5 candidats par creneau 1..3 (cache order, PAS le tri M1), 3 constituants.
NB_MENUS, NB_PLATS, CAND = 2, 3, 5
# 3 constituants cles : [0] Energie kJ, [1] Proteines, [3] Lipides (le 2 = Glucides est SKIPPE).
cEnergie, cProt, cLip = 0, 1, 3
CONST = [cEnergie, cProt, cLip]
NOMK = ["energie(kJ)", "proteines(g)", "lipides(g)"]
K = len(CONST)
print("Constituants suivis :")
for k, ci in enumerate(CONST): print(f"  k={k} -> cache[{ci}] {constituants[ci].split(',')[0].strip()}")

pool = []
for o in range(1, NB_PLATS + 1):
    pool.extend([p for p in all_plats if p.ordre == o][:CAND])   # cache order, fidèle a 08
def teneur(i, constIdx): return int(round(pool[i].comp[constIdx]))   # round half-to-even (caveat float)
def slot(m, p): return m * NB_PLATS + p
print(f"\nPool curee : {len(pool)} plats ({NB_PLATS} creneaux x {CAND} candidats)")
print("Apercu (creneau : candidats -> energie kJ) :")
for p in range(NB_PLATS):
    noms = [f"{pool[i].nom.strip()[:18]}({teneur(i,cEnergie)})" for i in range(p*CAND, p*CAND+CAND)]
    print(f"  creneau {p+1} : " + ", ".join(noms))

Constituants suivis :
  k=0 -> cache[0] Energie
  k=1 -> cache[1] Protéines
  k=2 -> cache[3] Lipides (g/100 g)

Pool curee : 15 plats (3 creneaux x 5 candidats)
Apercu (creneau : candidats -> energie kJ) :
  creneau 1 : 'ncapriata Di Fave(5922), 4 B's Restaurant T(3409), 5-Minute Broccoli (6415), 7 Layer Dip(11374), 90-Minute Soft Pre(7426)
  creneau 2 : (Sort-Of) Sweet an(1018), 1-Pot: Pastitsio G(15054), 1-Pot Pastitsio Go(15054), 10 Minute Szechuan(1178), 16th-Street Stew(10678)
  creneau 3 : 'sense and Sensibi(5329), ( From Bread Mix )(4421), ( From Bread Mix )(13568), 1-2-3 Meurbeteig D(14026), 1-Pot: Creamy Chic(3471)

2.2 Trois matrices d’entiers : `PlatId`, `Comp`, `MenuNut`

Matrice	Forme	Rôle
`PlatId[m][p]`	2×3	index pool du plat choisi par (menu, créneau)
`Comp[slot][k]`	6×3	composition liée du slot aplati (variable auxiliaire)
`MenuNut[m][k]`	2×3	somme nutritionnelle par menu

Comp est la variable auxiliaire qui résout l’impossibilité d’indexer un tableau hôte par une variable Z3 (pool[PlatId[m][p]] est interdit). Total : 30 variables Int.

# Variables de decision : 30 Int (PlatId 6 + Comp 18 + MenuNut 6).
platid = [[Int(f"pid_{m}_{p}") for p in range(NB_PLATS)] for m in range(NB_MENUS)]
comp = [[Int(f"comp_{slot(m,p)}_{k}") for k in range(K)] for m in range(NB_MENUS) for p in range(NB_PLATS)]
menunut = [[Int(f"nut_{m}_{k}") for k in range(K)] for m in range(NB_MENUS)]
print(f"{NB_MENUS*NB_PLATS} PlatId + {NB_MENUS*NB_PLATS*K} Comp + {NB_MENUS*K} MenuNut = "
      f"{NB_MENUS*NB_PLATS + NB_MENUS*NB_PLATS*K + NB_MENUS*K} variables Int.")

6 PlatId + 18 Comp + 6 MenuNut = 30 variables Int.

2.3 Le patient et ses restrictions (bornes par MENU)

Fidèle au C# 08 : un seul patient, inline comme quatre bornes entières, par menu (la somme des 3 plats du menu doit respecter chaque borne). Bornes rescalées kcal→kJ (×4,184) au moment du rewiring sur le cache Ciqual (kJ/100 g).

ATTENTION millésime (#8901) : ces bornes ont été réglées contre un cache C# aujourd’hui désuet (08 tourne sur 121 Ko / 736 recettes ; 07+09 s’accordent sur 270 Ko / 2387). Ici on consomme le cache Python 16b régénéré frais — les valeurs du menu résolu différeront des sorties C# (qu’on ne reproduit pas). On vérifie que le patient reste SAT sur ce pool (sinon = finding à reporter, pas de retouche silencieuse des bornes).

# Restrictions patient (fidele a Restriction{Min,Max}, -1 = pas de borne), par MENU.
energieMin = 3347    # ~800 kcal cumules minimum par menu
energieMax = 10878   # ~2600 kcal cumules maximum par menu
protMin    = 30      # proteines minimum par menu (g)
lipMax     = 600     # lipides maximum par menu (g)
print(f"Patient : energie in [{energieMin}, {energieMax}] kJ, proteines >= {protMin} g, "
      f"lipides <= {lipMax} g (par menu)")

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

2.4 Les cinq familles de contraintes

Bornes d’ordre : PlatId[m][p] dans la fenêtre des 5 candidats de son créneau.
Variété : Distinct global sur les 6 slots (pas deux fois le même plat).
Linking composition : Or(PlatId[m][p] ≠ cand, Comp[slot][k] == teneur(cand, k)) — l’idiome index + disjonction (90 assertions) qui relie l’index choisi à sa composition. C’est l’idiom que la jambe Python n’avait aucun exemple avant ce notebook.
Somme par menu : MenuNut[m][k] == Σ Comp[slot][k] sur les 3 créneaux.
Restrictions patient : MenuNut[m][·] dans les bornes (énergie, protéines, lipides).

# THE MODEL : 5 familles de contraintes + Solve (pure satisfiabilite, pas d'objectif).
t0 = time.perf_counter()
s = Solver()
# (1) bornes d'ordre
for m in range(NB_MENUS):
    for p in range(NB_PLATS):
        s.add(platid[m][p] >= p*CAND, platid[m][p] <= p*CAND + CAND - 1)
# (2) variete : Distinct global sur les 6 slots
s.add(Distinct(*[platid[m][p] for m in range(NB_MENUS) for p in range(NB_PLATS)]))
# (3) linking composition : PlatId != cand || Comp[slot][k] == teneur(cand, k)
for m in range(NB_MENUS):
    for p in range(NB_PLATS):
        sl = slot(m, p)
        for cand in range(p*CAND, p*CAND + CAND):
            for k in range(K):
                s.add(Or(platid[m][p] != cand, comp[sl][k] == teneur(cand, CONST[k])))
# (4) somme par menu
for m in range(NB_MENUS):
    for k in range(K):
        s.add(menunut[m][k] == comp[slot(m,0)][k] + comp[slot(m,1)][k] + comp[slot(m,2)][k])
# (5) restrictions patient (par menu)
for m in range(NB_MENUS):
    s.add(menunut[m][0] >= energieMin, menunut[m][0] <= energieMax)
    s.add(menunut[m][1] >= protMin)
    s.add(menunut[m][2] <= lipMax)

sat_cap = (s.check() == sat)
mdl = s.model() if sat_cap else None
print(f"Modele resolu en {(time.perf_counter()-t0)*1000:.0f} ms")
if not sat_cap:
    print("UNSAT : aucun plan ne satisfait les restrictions du patient sur cette pool (finding #8901).")
else:
    for m in range(NB_MENUS):
        e = mdl.eval(menunut[m][0]).as_long(); pr = mdl.eval(menunut[m][1]).as_long(); li = mdl.eval(menunut[m][2]).as_long()
        print(f"== Menu {m+1} ==  energie={e} kJ | proteines={pr} g | lipides={li} g")
        for p in range(NB_PLATS):
            v = mdl.eval(platid[m][p]).as_long()
            print(f"   creneau {p+1} : {pool[v].nom.strip():<30} "
                  f"(kJ={teneur(v,cEnergie)}, prot={teneur(v,cProt)}, lip={teneur(v,cLip)})")

Modele resolu en 19 ms
== Menu 1 ==  energie=8848 kJ | proteines=45 g | lipides=168 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 : ( From Bread Mix ) Big Soft Pretzels (kJ=4421, prot=26, lip=105)
== Menu 2 ==  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)

2.5 Vérification hors-Z3 (croire vs prouver)

Un solveur garantit les contraintes par construction — mais on vérifie indépendamment (re-calcul hors Z3). Deux prongs : (a) les sommes recomputées depuis la pool satisfont les bornes patient ; (b) ces sommes égalent les MenuNut du solveur — ce qui valide la couche de linking elle-même, pas seulement les bornes.

# Re-verification hors Z3 : re-somme depuis la pool, compare aux MenuNut du solveur.
if not sat_cap:
    print("Pas de solution a verifier (UNSAT).")
else:
    ok = True
    for m in range(NB_MENUS):
        e = pr = li = 0
        for p in range(NB_PLATS):
            v = mdl.eval(platid[m][p]).as_long()
            e  += teneur(v, cEnergie); pr += teneur(v, cProt); li += teneur(v, cLip)
        eOk = energieMin <= e <= energieMax; pOk = pr >= protMin; lOk = li <= lipMax
        Me = mdl.eval(menunut[m][0]).as_long(); Mpr = mdl.eval(menunut[m][1]).as_long(); Mli = mdl.eval(menunut[m][2]).as_long()
        match = (e == Me and pr == Mpr and li == Mli)
        ok = ok and eOk and pOk and lOk and match
        print(f"Menu {m+1} : recalc energie={e}({'OK' if eOk else 'HORS'}), prot={pr}({'OK' if pOk else 'HORS'}), "
              f"lip={li}({'OK' if lOk else 'HORS'}) ; coherent avec MenuNut={'oui' if match else 'NON'}")
    print("\nVERIFIE : toutes les restrictions patient sont respectees." if ok
          else "\nINCOHERENCE detectee (a investiguer).")

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

VERIFIE : toutes les restrictions patient sont respectees.

3. Exercices

Quatre prolongements (stubs : ils s’exécutent tels quels, n’échouent pas, à compléter).

Exercice 1 — Diversité d’entrée sur jours consécutifs : forcer que le créneau 1 diffère entre Menu 1 et Menu 2 (déjà couvert par le Distinct global, mais l’exprimer comme une contrainte dédiée Or(PlatId[0][0] != PlatId[1][0], ...) et mesurer l’impact).

# Exercice 1 (stub) : diversite entree jours consecutifs.
# TODO: ajouter s.add(Or(...)) forçant créneau 1 different entre menus, re-solve, comparer.
print("[Ex.1] Stub : a completer (diversite entree jours consecutifs).")
def exercice_diversite_entree():
    # ... ajouter la contrainte, re-solve, retourner le nb de plans ...
    return -1

[Ex.1] Stub : a completer (diversite entree jours consecutifs).

Exercice 2 — Seuil d’énergie strict → UNSAT : resserrer energieMax par dichotomie jusqu’à rendre le modèle insatisfiable. Quel créneau porte l’essentiel de l’énergie kJ ?

# Exercice 2 (stub) : seuil UNSAT par dichotomie sur energieMax.
# TODO: boucle resserrant energieMax, re-solve, retourner le seuil ou ca casse.
print("[Ex.2] Stub : a completer (seuil UNSAT energie).")
def exercice_unsat_threshold():
    # ... dichotomie sur energieMax ...
    return -1

[Ex.2] Stub : a completer (seuil UNSAT energie).

Exercice 3 — Passage à 3 menus : adapter les dimensions des matrices (PlatId 3×3, Comp 9×3, MenuNut 3×3) et re-solve. Note : les formes sont hardcoded à NB_MENUS=2 dans la déclaration des variables — les paramétrer est le cœur de l’exercice.

# Exercice 3 (stub) : passer a 3 menus (adapter les formes de matrices).
# TODO: parametriser NB_MENUS=3, redeclarer les matrices, re-solve, retourner le temps.
print("[Ex.3] Stub : a completer (3 menus).")
def exercice_trois_menus():
    # ... NB_MENUS=3, redeclarer vars, re-solve ...
    return -1.0

[Ex.3] Stub : a completer (3 menus).

Exercice 4 — Ajouter le sel (Sel chlorure de sodium, cache idx 4) comme 4e constituant contraint (borne max selMax), et re-solve.

# Exercice 4 (stub) : ajouter le constituant Sel (cache idx 4).
# TODO: CONST.append(4), ajouter selMax, re-declarer Comp/MenuNut sur K=4, re-solve.
print("[Ex.4] Stub : a completer (constituant sel).")
def exercice_constituant_sel():
    cSel = next(i for i, n in enumerate(constituants) if "sel chlorure" in n.lower())
    # ... CONST.append(cSel) ...
    return cSel

[Ex.4] Stub : a completer (constituant sel).

Synthèse — le capstone patient, en Python

Mouvement	Ce qu’il montre	Idiome Z3
M1 squelette	semaine 7×5 sans nutrition	`int[][]` plate de `Int` (vs `CollectionHandling.Array` C#)
M2 capstone	patient SAT avec restrictions nutritionnelles	index + linking disjonction (`Or(pid≠cand, comp==val)`)

Le capstone patient est le point où la nutrition rencontre la combinatoire : on ne peut pas forcer « 30 g de protéines minimum » sur un jouet de 24 plats — il faut un corpus réel (le cache 16b) pour que la contrainte morde. La re-vérification hors-Z3 clôt l’arc : on ne croit pas le solveur, on le prouve. C’est ce qui distingue ce capstone d’une simple démonstration.

Prochain grain (G3) : la convergence à l’échelle — comparer les encodages (index naïf vs one-hot pseudo-Boolean PbEq/PbLe) quand R et C augmentent, là où le naïf explose.

Retour au sommet