Z3-Python-16e — Meal-Planner : l’optimisation (du SAT à l’OPT sur corpus réel)

Grain « non-miroir » de la jambe Python-large du planificateur #1206. 16c (capstone patient) et 16d (convergence à l’échelle) répondaient à la question de satisfiabilité : existe-t-il un menu conforme ? Ce notebook 16e répond à la question d’optimisation : quel est le meilleur menu ?

Ce que ce grain apporte de neuf (net-new). Le corpus réel Ciqual × RecipeML (cache de 16b, R=594) n’avait jamais été confié à un solveur d’optimisation. Ce notebook le fait, en réutilisant l’encodage one-hot pseudo-booléen qui passe à l’échelle (leçon de 16d), et y ajoute trois familles absentes de toute la track Python :

  • Optimize.minimize / maximize sur R=594 (le toy 16 ne le faisait que sur 24 plats) ;
  • add_soft — l’API native de MaxSAT pondéré (zéro occurrence dans les notebooks Python du dépôt ; le notebook Z3-Python-06 l’émule à la main avec des variables de relaxation) ;
  • priority='pareto' | 'box' — les modes multi-objectif natifs de Z3, inutilisés jusqu’ici (le notebook 06 émule le front de Pareto par une boucle).

Ce n’est pas un port du C# 14_Optimize_MaxSAT (qui est DSL + toy corpus : knapsack 5 objets, nurse-roster 3×3). Ici l’optimisation est construite à frais nouveaux sur le corpus réel du meal-planner, en encodage PB brut.

Navigation : << 16d - Convergence | 17 - Array Theory >> | README Z3-Python

Objectifs

  1. Passer du Solver (existe-t-il une solution ?) à l’Optimize (quelle est la meilleure ?).
  2. Démontrer minimize / maximize sur le corpus réel (R=594) — et pourquoi le glouton rate l’optimum global.
  3. Introduire add_soft : la préférence souple pondérée (≠ restriction hard), exprimée en une ligne via le solveur MaxSAT natif de Z3.
  4. Introduire le multi-objectif natif (priority='pareto' / 'box') pour explorer le compromis sel ↔︎ protéines.
  5. Lire la valeur de l’objectif depuis le solveur (h.value()) et ré-optimiser incrémentalement (push/pop).

Prérequis : 16 (Optimize sur corpus jouet), 16b (cache réel), 16d (encodage one-hot PB qui scale).

1. Données + encodage : on réutilise le cache réel et le one-hot partitionné

Le cache de 16b (R=594 recettes solveur-usables) et l’encodage one-hot partitionné par cours de 16d (un pool de recettes par créneau : Entrée, Plat principal, Accompagnement, Pain, Dessert) sont notre point de départ. Pourquoi les pools plutôt que le one-hot plat ? Parce qu’ils réduisent le nombre de booléens (~4158 contre ~20790) sans perte d’expressivité — et rendent l’optimisation tractable à cette échelle.

# Chargement du cache (16b) + partition par cours (16d) -- la base commune.
import json, time
from pathlib import Path
from z3 import Optimize, Bool, If, PbEq, PbLe, PbGe, Or, Not, sat, is_true, Sum, IntVal

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"
assert CACHE.exists(), f"Cache absent : {CACHE} (executez 16b d'abord)."
doc = json.loads(CACHE.read_text(encoding="utf-8"))
constituants = doc["constituants"]; C = len(constituants)
plats = [(r["title"].strip()[:40], [float(v) for v in r["vec"]], list(r["cats"])) for r in doc["recipes"]]
R = len(plats)
vint = [[int(round(p[1][c])) for p in plats] for c in range(C)]   # valeurs entieres (banker rounding)
def pq(c, q):                       # quantile TRONQUE (pas interpole)
    vals = sorted(p[1][c] for p in plats); return vals[int(q * (len(vals) - 1))]
NMENUS, NPLATS = 7, 5
loE = NPLATS * int(pq(0, 0.20)); hiE = NPLATS * int(pq(0, 0.80))
loP = NPLATS * int(pq(1, 0.30));  hiS = max(1, NPLATS * int(pq(4, 0.70)))
# restr = [(constituantIndex, lo, hi)], -1 = pas de borne de ce cote.
restr = [(0, loE, hiE), (1, loP, -1), (4, -1, hiS)]
# Partition par cours (meme logique que 16d cell C').
COURSES = ["Entree", "Plat principal", "Accompagnement", "Pain", "Dessert"]
COURSE_CATS = [
    {"appetizers", "soups", "salads", "salad", "soup"},
    {"main dish", "meats", "beef", "poultry", "seafood", "fish", "pasta", "casseroles", "chili", "pork", "chicken", "stews"},
    {"vegetables", "vegetarian", "sauces", "sauce", "side dishes", "rice", "potatoes"},
    {"breads", "bread", "muffins", "rolls", "biscuits"},
    {"desserts", "cakes", "cake", "cookies", "chocolate", "fruits", "pies", "candy", "pastries"},
]
def course_of(cats):
    for cat in cats:
        for k in range(5):
            if cat.lower() in COURSE_CATS[k]:
                return k
    return 1
pool = [[] for _ in range(5)]
for r in range(R):
    pool[course_of(plats[r][2])].append(r)
SEL, PROT, GLU, LIP = 4, 1, 2, 3   # alias de constituants (indices C)
print(f"Cache : R={R} recettes, C={C} constituants. Pools : "
      + ", ".join(f"{COURSES[k]}={len(pool[k])}" for k in range(5)) + ".")
print(f"Theoreme : {NMENUS} menus x {NPLATS} plats. bornes patient dynamiques : "
      f"energie[{loE},{hiE}], proteines>={loP}, sel<={hiS}.")
Cache : R=712 recettes, C=5 constituants. Pools : Entree=52, Plat principal=370, Accompagnement=47, Pain=65, Dessert=178.
Theoreme : 7 menus x 5 plats. bornes patient dynamiques : energie[20515,91485], proteines>=135, sel<=25.

2. minimize / maximize : le menu le moins salé, le plus protéiné

Optimize sous-traite la recherche d’optimum : le solveur combine satisfiabilité et poursuite de l’objectif en un appel (algorithmes OBBTP/maxres). On optimise un menu unique (5 cours, un par pool) sous les restrictions hard patient, en minimisant le sel total — puis en maximisant les protéines.

Pourquoi un seul menu ? Parce que l’optimum d’un menu isolé suffit à porter la leçon (glouton vs optimum global), et reste tractable. Le plan hebdomadaire optimal (7 menus) vient au §5.

# Optimize sur UN menu (5 cours) : minimiser le sel, puis maximiser les proteines.
# sel[m_unused][p][j] : la j-eme recette du pool[p] occupe le cours p du menu 0.
sel0 = [[Bool(f"o_{p}_{j}") for j in range(len(pool[p]))] for p in range(NPLATS)]
def hard_menu(opt):                          # restrictions hard patient + structure du menu
    for p in range(NPLATS):                  # exactement 1 recette / cours
        opt.add(PbEq([(sel0[p][j], 1) for j in range(len(pool[p]))], 1))
    for (cc, lo, hi) in restr:               # fenetre nutritionnelle (borne sur le menu)
        pairs = [(sel0[p][j], int(vint[cc][pool[p][j]])) for p in range(NPLATS) for j in range(len(pool[p]))]
        if lo >= 0: opt.add(PbGe(pairs, lo))
        if hi >= 0: opt.add(PbLe(pairs, hi))

def sel_total(cc):                           # somme ponderee PB -> valeur du constituant cc sur le menu
    return [(sel0[p][j], int(vint[cc][pool[p][j]])) for p in range(NPLATS) for j in range(len(pool[p]))]

# --- (a) minimiser le sel ---
opt_min = Optimize(); hard_menu(opt_min)
h_sel = opt_min.minimize(Sum([sel0[p][j] * int(vint[SEL][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p]))]))
t0 = time.perf_counter(); st = opt_min.check(); dt = time.perf_counter() - t0
print(f"MIN sel : {st} en {dt:.2f}s, valeur optimale = {h_sel.value()}")
m = opt_min.model()
menu_min = [next(plats[pool[p][j]][0] for j in range(len(pool[p])) if is_true(m.eval(sel0[p][j]))) for p in range(NPLATS)]
print("  Menu min-sel : " + " | ".join(f"{COURSES[p]}: {n[:18]}" for p, n in enumerate(menu_min)))

# --- (b) maximiser les proteines ---
opt_max = Optimize(); hard_menu(opt_max)
h_prot = opt_max.maximize(Sum([sel0[p][j] * int(vint[PROT][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p]))]))
t0 = time.perf_counter(); st = opt_max.check(); dt = time.perf_counter() - t0
print(f"MAX prot : {st} en {dt:.2f}s, valeur optimale = {h_prot.value()}")
m = opt_max.model()
menu_max = [next(plats[pool[p][j]][0] for j in range(len(pool[p])) if is_true(m.eval(sel0[p][j]))) for p in range(NPLATS)]
print("  Menu max-prot : " + " | ".join(f"{COURSES[p]}: {n[:18]}" for p, n in enumerate(menu_max)))
MIN sel : sat en 0.03s, valeur optimale = 0
  Menu min-sel : Entree: All-You-Can-Eat Co | Plat principal: Abadoo's Granola | Accompagnement: Acorn Squash, Indo | Pain: Aberffraw Cakes | Dessert: $100 Chocolate Cak
MAX prot : sat en 0.27s, valeur optimale = 1763
  Menu max-prot : Entree: Aioli Platter | Plat principal: Alligator Sauce Pi | Accompagnement: African Vegetarian | Pain: Almond-Pumkin Muff | Dessert: Almond Cream Filli

Interprétation — pourquoi le glouton rate l’optimum global

Un glouton choisirait, cours par cours, la recette la moins salée du pool — mais ce choix local ignore le couplage nutritionnel : la recette la moins salée en plat principal peut être si pauvre en protéines qu’elle force un accompagnement très salé pour atteindre le plancher loP. La combinatoire (fenêtre × variété) n’est pas compositionnelle : optimiser cours par cours ne garantit pas l’optimum global. Optimize, lui, considère les 5 cours simultanément et trouve le vrai minimum.

minimize vs dichotomie manuelle. L’alternative sans Optimize serait une dichotomie sur le seuil de sel (Solver + sel <= mid, resserrer mid jusqu’à unsat) — N appels et une logique de boucle. minimize le fait en un appel.

3. add_soft : la préférence souple pondérée (MaxSAT natif)

Les restrictions hard patient (fenêtre énergétique, plancher protéique, plafond de sel) sont des contraintes inviolables : les violer rend le menu unsat. Mais un vrai patient a aussi des préférences : « je préfère les desserts aux fruits », « j’aime peu répéter la même catégorie d’entrée ». Ces préférences sont souples — on veut les satisfaire autant que possible, pas les exiger.

C’est exactement le MaxSAT pondéré : on attache un poids à chaque clause de préférence, et le solveur minimise le poids total des clauses violées. L’API native z3-py est opt.add_soft(expr, weight, group) — une ligne par préférence.

Net-new. Aucun notebook Python du dépôt n’utilise add_soft (le notebook Z3-Python-06 émule MaxSAT à la main : une variable de relaxation r par clause, Or(pref, r) puis minimize(Sum(If(r,1,0))) — six lignes pour une préférence, et pas de sémantique de group). add_soft fait la même chose en une ligne, via le solveur MaxSAT natif de Z3 (MaxRes/OLL).

# add_soft : preferences souples ponderees (MaxSAT natif) sur le menu.
# On ajoute au menu hard des preferences patient : poids eleve = prefere fortement.
opt_s = Optimize(); hard_menu(opt_s)
# Pref 1 (poids 10) : le dessert devrait etre a base de fruits (cats contient "fruits" / "fruits").
# Pref 2 (poids 3)  : l'accompagnement devrait etre vegetarien.
# Pref 3 (poids 1)  : le pain ne devrait pas etre "biscuits" (penalite legere).
def cats_of_course(p):
    return [set(c.lower() for c in plats[pool[p][j]][2]) for j in range(len(pool[p]))]
DESSERT, ACCOMP, PAIN = 4, 2, 3
# Pref 1 : exactement un dessert-fruits (PbEq sur les dessert-fruit) -- encode comme soft clause ponderee.
# On modelise "il existe un dessert fruit" comme une clause Or (soft).
fruit_bools = [sel0[DESSERT][j] for j in range(len(pool[DESSERT])) if "fruits" in cats_of_course(DESSERT)[j]]
if fruit_bools:
    opt_s.add_soft(Or(fruit_bools), weight=10, id="prefs")
veggie_bools = [sel0[ACCOMP][j] for j in range(len(pool[ACCOMP])) if "vegetarian" in cats_of_course(ACCOMP)[j]]
if veggie_bools:
    opt_s.add_soft(Or(veggie_bools), weight=3, id="prefs")
# Pref 3 : penaliser le pain "biscuits" -- clause soft Nie chaque biscuit-pain.
for j in range(len(pool[PAIN])):
    if "biscuits" in cats_of_course(PAIN)[j]:
        opt_s.add_soft(Not(sel0[PAIN][j]), weight=1, id="prefs")
t0 = time.perf_counter(); st = opt_s.check(); dt = time.perf_counter() - t0
print(f"Menu + soft prefs : {st} en {dt:.2f}s")
m = opt_s.model()
menu_pref = [next(plats[pool[p][j]][0] for j in range(len(pool[p])) if is_true(m.eval(sel0[p][j]))) for p in range(NPLATS)]
print("  Menu preferentiel : " + " | ".join(f"{COURSES[p]}: {n[:18]}" for p, n in enumerate(menu_pref)))
print("  (add_soft = MaxSAT natif : 1 ligne par preference, vs ~6 lignes de variable de relaxation a la main)")
Menu + soft prefs : sat en 0.01s
  Menu preferentiel : Entree: All-You-Can-Eat Co | Plat principal: Almond Horns | Accompagnement: Almonnaise | Pain: 'sense and Sensibi | Dessert: 1850 Blackberry Pi
  (add_soft = MaxSAT natif : 1 ligne par preference, vs ~6 lignes de variable de relaxation a la main)

Interprétation — add_soft et la sémantique de group

add_soft(expr, weight, group) attache un poids à la clause expr. Le solveur minimise la somme des poids des clauses violées. Quand plusieurs clauses partagent le même group, Z3 ne compte que la violation la plus coûteuse du groupe (sémantique max), ce qui permet de modéliser « au moins une de ces préférences » sans pénaliser doublement. C’est une sémantique que l’émulation manuelle par variable de relaxation n’exprime pas naturellement.

4. Multi-objectif : le compromis sel ↔︎ protéines (box + scalarisation)

Minimiser le sel et maximiser les protéines sont deux objectifs antagonistes : le menu le moins salé n’est pas le plus protéiné. On veut caractériser le compromis : ses bornes (le sel minimum absolu, les protéines maximum absolues) et le front de Pareto (les compromis optimaux). Deux outils complémentaires :

  • priority='box' — chaque objectif optimisé indépendamment, en un seul check() (renvoie les deux optima via les handles). Donne les bornes qui cadrent le compromis.
  • Scalarisation — on combine les objectifs en un seul scalaire alpha·sel − (1−alpha)·prot et on balaie alpha ∈ [0, 1] ; chaque alpha est un single-objectif minimize (rapide), et l’ensemble des solutions trace le front de Pareto.

Net-new. Le mode priority='box' est inutilisé dans tout le dépôt (priority = 0 occurrence). Le mode 'pareto' natif existe aussi (il énumère le front sans sweep), mais chaque check() y résout un compromis multi-objectif — coûteux sur une instance contrainte (timeout observé). À l’échelle réelle, box + scalarisation sont les outils pratiques (bornes en un check + front par sweep), c’est ce que ce notebook démontre.

# Multi-objectif sur le corpus plein R=594 : (a) box pour les bornes, (b) scalarisation pour le front.
expr_sel = Sum([sel0[p][j] * int(vint[SEL][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p]))])
expr_prot = Sum([sel0[p][j] * int(vint[PROT][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p]))])
# (a) BOX : min sel seul ET max prot seul, en UN check (deux optima independants lus via les handles).
ob = Optimize(); hard_menu(ob); ob.set("priority", "box")
hs = ob.minimize(expr_sel); hp = ob.maximize(expr_prot)
t0 = time.perf_counter(); ob.check(); dt = time.perf_counter() - t0
print(f"BOX (priority='box', 1 check, 2 optima independants) en {dt:.2f}s :")
print(f"   sel minimum absolu = {hs.value()} g  |  proteines maximum absolu = {hp.value()} g")
# (b) SCALARISATION : front de Pareto pratique (sweep pondere, chaque alpha = un single-objectif minimize).
print("Front de Pareto (scalarisation ponderee alpha*sel - (1-alpha)*prot) :")
print("   alpha | sel(g) | prot(g)")
seen = set()
for alpha in [i / 6 for i in range(7)]:
    oc = Optimize(); hard_menu(oc); oc.set("timeout", 15000)
    oc.minimize(expr_sel * int(round(alpha * 100)) - expr_prot * int(round((1 - alpha) * 100)))
    if oc.check() == sat:
        m = oc.model()
        sv = sum(int(vint[SEL][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p])) if is_true(m.eval(sel0[p][j])))
        pv = sum(int(vint[PROT][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p])) if is_true(m.eval(sel0[p][j])))
        if (sv, pv) not in seen:
            seen.add((sv, pv))
            print(f"   {alpha:.2f}  | {sv:>5}  | {pv:>5}")
print("  -> alpha=0 = maximise les proteines (sel libre) ; alpha=1 = minimise le sel (prot libre).")
BOX (priority='box', 1 check, 2 optima independants) en 0.34s :
   sel minimum absolu = 0 g  |  proteines maximum absolu = 1763 g
Front de Pareto (scalarisation ponderee alpha*sel - (1-alpha)*prot) :
   alpha | sel(g) | prot(g)
   0.00  |    25  |  1763
   1.00  |     0  |   178
  -> alpha=0 = maximise les proteines (sel libre) ; alpha=1 = minimise le sel (prot libre).

Interprétation — bornes box et front de scalarisation

priority='box' a livré en un seul check() les deux optima indépendants : le sel minimum absolu et les protéines maximum absolues — les bornes qui cadrent tout compromis possible. La scalarisation a ensuite tracé le front de Pareto : à mesure qu’on pénalise le sel (alpha croissant), le solveur accepte moins de protéines. Chaque point du front est un menu réel (5 cours) pour lequel aucun autre n’est à la fois moins salé et plus protéiné.

Contraste avec l’émulation. Le notebook Z3-Python-06 trace ce front par une boucle Python (sweep + dédoublonnage) sur un toy corpus ; ici la scalarisation court sur le corpus réel R=594, et le mode natif box (qui n’a d’équivalent nulle part dans le dépôt) donne les bornes en un check. Le mode 'pareto' natif existe pour énumérer le front sans sweep, mais reste coûteux par check sur instance contrainte.

5. Lire l’objectif et ré-optimiser incrémentalement (push/pop)

opt.minimize(e) / opt.maximize(e) renvoient un handle sur lequel on lit la valeur optimale (h.value()), la borne supérieure (h.upper()) ou inférieure (h.lower()). Et comme un Solver, un Optimize supporte push()/pop() : on ajoute temporairement une contrainte (ex. « cette semaine, végétarien »), on ré-optimise, puis on la retire sans reconstruire tout l’encodage — utile pour des variantes exploratoires.

# Handle d'objectif + push/pop : re-optimiser sous une variante sans tout reconstruire.
opt_h = Optimize(); hard_menu(opt_h)
h = opt_h.minimize(Sum([sel0[p][j] * int(vint[SEL][pool[p][j]]) for p in range(NPLATS) for j in range(len(pool[p]))]))
opt_h.check()
print(f"Optimum sel (baseline) : valeur = {h.value()}, borne sup = {h.upper()}")
# Variante : forcer un accompagnement vegetarien (comme si le patient etait vegetarian sur ce cours).
opt_h.push()
VEGGIE_ACCOMP = [sel0[ACCOMP][j] for j in range(len(pool[ACCOMP])) if "vegetarian" in cats_of_course(ACCOMP)[j]]
if VEGGIE_ACCOMP:
    opt_h.add(Or(VEGGIE_ACCOMP))   # au moins un accompagnement vegetarien
    st = opt_h.check()
    print(f"Variante (accompagnement vegetarien force) : {st}, nouvel optimum sel = {h.value() if st == sat else 'N/A'}")
opt_h.pop()   # on retire la contrainte -> retour a la baseline, sans reconstruire l'encodage.
# NB : un pop() invalide le handle jusqu'au prochain check() (l'etat interne du solveur a change).
opt_h.check()   # re-optimiser la baseline : le handle h redevient lisible.
print(f"Apres pop() + check() : retour a la baseline, optimum sel = {h.value()} (encodage preserve, pas regenere).")
Optimum sel (baseline) : valeur = 0, borne sup = 0
Variante (accompagnement vegetarien force) : sat, nouvel optimum sel = 0
Apres pop() + check() : retour a la baseline, optimum sel = 0 (encodage preserve, pas regenere).

6. Le plan hebdomadaire optimal : 7 menus au sel total minimal

Pour clore, on optimise le plan complet (7 menus × 5 cours) : minimiser le sel total de la semaine, sous les restrictions hard patient par menu + la variété (chaque recette au plus une fois par semaine). C’est l’encodage C’ de 16d (course-partitionné, ~4158 booléens) confié à Optimize — la démonstration que l’optimisation reste tractable à l’échelle réelle grâce au bon encodage.

# Plan hebdomadaire optimal : 7 menus, minimiser le sel total de la semaine.
opt_w = Optimize()
opt_w.set("timeout", 120000)   # garde-fou : 2 min max pour l'optimum hebdo (souvent resolu en quelques s).
selW = [[[Bool(f"w_{m}_{p}_{j}") for j in range(len(pool[p]))] for p in range(NPLATS)] for m in range(NMENUS)]
for m in range(NMENUS):
    for p in range(NPLATS):   # exactement 1 recette / cours / menu
        opt_w.add(PbEq([(selW[m][p][j], 1) for j in range(len(pool[p]))], 1))
    for (cc, lo, hi) in restr:   # fenetre nutritionnelle par menu
        pairs = [(selW[m][p][j], int(vint[cc][pool[p][j]])) for p in range(NPLATS) for j in range(len(pool[p]))]
        if lo >= 0: opt_w.add(PbGe(pairs, lo))
        if hi >= 0: opt_w.add(PbLe(pairs, hi))
for p in range(NPLATS):       # variete : chaque recette <= 1x / semaine (colonne sur les menus)
    for j in range(len(pool[p])):
        opt_w.add(PbLe([(selW[m][p][j], 1) for m in range(NMENUS)], 1))
week_sel = Sum([selW[m][p][j] * int(vint[SEL][pool[p][j]]) for m in range(NMENUS) for p in range(NPLATS) for j in range(len(pool[p]))])
hw = opt_w.minimize(week_sel)
t0 = time.perf_counter(); st = opt_w.check(); dt = time.perf_counter() - t0
print(f"Plan hebdo optimal (min sel semaine) : {st} en {dt:.2f}s, sel total optimal = {hw.value()}")
mw = opt_w.model()
for m in range(3):
    names = [next(plats[pool[p][j]][0] for j in range(len(pool[p])) if is_true(mw.eval(selW[m][p][j]))) for p in range(NPLATS)]
    print(f"  Menu {m+1} : " + " | ".join(f"{COURSES[p]}: {n[:16]}" for p, n in enumerate(names)))
print(f"  (... 4 menus supplementaires ; {NMENUS*NPLATS} cours sur la semaine au sel total minimal.)")
Plan hebdo optimal (min sel semaine) : sat en 0.26s, sel total optimal = 2
  Menu 1 : Entree: Airport Slaw | Plat principal: Almond Paste | Accompagnement: Almond Milk (Non | Pain: All-Bran Fruit L | Dessert: Almond Date Shak
  Menu 2 : Entree: Almond Brussels  | Plat principal: Almond Paste | Accompagnement: Acorn Squash W/  | Pain: Ale Bread | Dessert: Almond Tea Jelly
  Menu 3 : Entree: All-You-Can-Eat  | Plat principal: Almond Liqueur | Accompagnement: Acorn Squash, In | Pain: Aberffraw Cakes | Dessert: Acorns
  (... 4 menus supplementaires ; 35 cours sur la semaine au sel total minimal.)

6b. Le jouet a l’echelle : le plan hebdomadaire a cout minimal (24 plats, D=7)

La section 5 du 16 a resolu le plan hebdomadaire avec un Solver() (recherche de faisabilite : une grille valide suffit). C’est passer a cote de la capacite signature de Z3 : l’optimisation sous contraintes via Optimize(). On veut desormais le plan hebdomadaire le moins cher, en respectant fenetre kcal + apport proteique + variete (chaque plat au plus 2 fois dans la semaine).

On met aussi le probleme a l’echelle : un corpus de 24 plats (vs 9) et un plan sur D=7 jours (la semaine complete, vs 3). C’est le “probleme riche” (Prong-B) ou un glouton “jour par jour” echoue : minimiser le cout de chaque jour independamment violente la contrainte de variete hebdomadaire (les plats les moins chers reviennent trop souvent) et le couplage des apports proteiques. Le minimize de Z3, lui, optimise le cout global de la semaine en considerant toutes les contraintes simultanement.

Miroir “Python-large” de l’Epic #1206 : le corpus de 24 plats est un modele d’echelle (noms reels, kcal/proteines/couts realistes) du corpus RecipeML (~11 000 recettes). Le chemin vers les vraies donnees (download_meal_data.py : Ciqual ANSES 2025 + RecipeML) est un effort separe multi-jours ; ici on demontre la capacite d’optimisation SMT sur un tableau imbrique (jours x plats) a une echelle pedagogique bornee.

# Corpus elargi : 24 plats (8 par categorie), deterministe, kcal/proteines/couts realistes.
# Modele d'echelle du corpus RecipeML (~11k) — noms reels, pas de PRNG, pour la reproductibilite.
DISHES2 = [
    ("Porridge fruits rouges", "breakfast", 300, 12, 180),
    ("Yaourt granola",         "breakfast", 350, 18, 220),
    ("Oeufs brouilles",        "breakfast", 400, 22, 280),
    ("Pain beurre confiture",  "breakfast", 320,  8, 120),
    ("Smoothie banane",        "breakfast", 280, 10, 150),
    ("Pancakes sirop",         "breakfast", 380, 14, 250),
    ("Fromage blanc miel",     "breakfast", 260, 16, 170),
    ("Bowl chia",              "breakfast", 340, 12, 210),
    ("Salade cesar",           "lunch", 500, 25, 650),
    ("Wrap poulet",            "lunch", 550, 30, 580),
    ("Quiche epinards",        "lunch", 600, 20, 520),
    ("Sandwich thon",          "lunch", 480, 22, 420),
    ("Bowl quinoa legumes",    "lunch", 520, 18, 480),
    ("Soupe poireaux fromage", "lunch", 450, 16, 380),
    ("Pates pesto",            "lunch", 580, 16, 440),
    ("Riz saute legumes",      "lunch", 560, 14, 410),
    ("Poulet curry",           "dinner", 650, 35, 700),
    ("Saumon four",            "dinner", 700, 32, 850),
    ("Risotto champignons",    "dinner", 750, 18, 600),
    ("Boeuf bourguignon",      "dinner", 720, 38, 780),
    ("Lasagnes",               "dinner", 680, 26, 620),
    ("Poisson papillote",      "dinner", 600, 34, 720),
    ("Chili con carne",        "dinner", 690, 30, 560),
    ("Tarte tatin salee",      "dinner", 710, 22, 540),
]
DN2 = [d[0] for d in DISHES2]
DC2 = [d[1] for d in DISHES2]
DK2 = [d[2] for d in DISHES2]
DP2 = [d[3] for d in DISHES2]   # proteines (g)
DCOST2 = [d[4] for d in DISHES2]  # cout (centimes)
ND2 = len(DISHES2)
D2 = 7                          # semaine complete (lundi..dimanche)
DAY_LO2, DAY_HI2 = 1400, 1900    # fenetre kcal/jour (petit-dej + dejeuner + diner)
PROT_MIN = 40                    # apport proteique minimal par jour (g)
MAX_REPEAT = 2                   # variete : chaque plat au plus 2x dans la semaine
print(f"Corpus elargi : {ND2} plats ({sum(c=='breakfast' for c in DC2)} bf, "
      f"{sum(c=='lunch' for c in DC2)} lunch, {sum(c=='dinner' for c in DC2)} dinner). "
      f"Plan Optimize sur D={D2} jours, fenetre [{DAY_LO2},{DAY_HI2}] kcal, proteines >= {PROT_MIN} g, "
      f"variete <= {MAX_REPEAT}x/semaine.")

def plan_hebdomadaire_optimal():
    opt = Optimize()
    # Sel[j][i] = True ssi le plat i est servi le jour j (matrice booleenne jours x plats).
    Sel = [[Bool(f"O_{j}_{i}") for i in range(ND2)] for j in range(D2)]
    # (1) 1 plat par categorie et par jour.
    for j in range(D2):
        for cat in ("breakfast", "lunch", "dinner"):
            opt.add(Sum([If(Sel[j][i], 1, 0) for i in range(ND2) if DC2[i] == cat]) == 1)
    # (2) Fenetre kcal par jour.
    for j in range(D2):
        day_cal = Sum([If(Sel[j][i], DK2[i], 0) for i in range(ND2)])
        opt.add(day_cal >= DAY_LO2, day_cal <= DAY_HI2)
    # (3) Apport proteique minimal par jour.
    for j in range(D2):
        day_prot = Sum([If(Sel[j][i], DP2[i], 0) for i in range(ND2)])
        opt.add(day_prot >= PROT_MIN)
    # (4) Variete : chaque plat au plus MAX_REPEAT fois dans la semaine.
    for i in range(ND2):
        opt.add(Sum([If(Sel[j][i], 1, 0) for j in range(D2)]) <= MAX_REPEAT)
    # (5) Objectif : MINIMISER le cout total de la semaine (signature Optimize, Prong-B).
    week_cost = Sum([If(Sel[j][i], DCOST2[i], 0) for j in range(D2) for i in range(ND2)])
    opt.minimize(week_cost)
    t0 = time.perf_counter()
    status = opt.check()
    t1 = time.perf_counter()
    plan = None
    cost = None
    if status == sat:
        m = opt.model()
        plan = [[DN2[i] for i in range(ND2) if m.eval(Sel[j][i])] for j in range(D2)]
        cost = sum(DCOST2[i] for j in range(D2) for i in range(ND2) if m.eval(Sel[j][i]))
    return plan, cost, (t1 - t0) * 1000

plan, cost, ms = plan_hebdomadaire_optimal()
print(f"\n=== Plan hebdomadaire OPTIMAL (D={D2}, minimise le cout, resolu en {ms:.1f} ms) ===")
if plan:
    print(f"Cout total minimal de la semaine : {cost} centimes = {cost/100:.2f} EUR")
    for j, day in enumerate(plan):
        kcal = sum(DK2[DN2.index(d)] for d in day)
        prot = sum(DP2[DN2.index(d)] for d in day)
        print(f"  Jour {j+1} : {', '.join(day)}  ->  {kcal} kcal, {prot} g prot")
else:
    print("  Aucun plan (UNSAT) — relacher une contrainte (fenetre kcal, variete, proteines).")
Corpus elargi : 24 plats (8 bf, 8 lunch, 8 dinner). Plan Optimize sur D=7 jours, fenetre [1400,1900] kcal, proteines >= 40 g, variete <= 2x/semaine.

=== Plan hebdomadaire OPTIMAL (D=7, minimise le cout, resolu en 258.9 ms) ===
Cout total minimal de la semaine : 7940 centimes = 79.40 EUR
  Jour 1 : Pain beurre confiture, Sandwich thon, Chili con carne  ->  1490 kcal, 60 g prot
  Jour 2 : Pain beurre confiture, Riz saute legumes, Risotto champignons  ->  1630 kcal, 40 g prot
  Jour 3 : Smoothie banane, Sandwich thon, Lasagnes  ->  1440 kcal, 58 g prot
  Jour 4 : Fromage blanc miel, Soupe poireaux fromage, Risotto champignons  ->  1460 kcal, 50 g prot
  Jour 5 : Fromage blanc miel, Soupe poireaux fromage, Tarte tatin salee  ->  1420 kcal, 54 g prot
  Jour 6 : Porridge fruits rouges, Riz saute legumes, Tarte tatin salee  ->  1570 kcal, 48 g prot
  Jour 7 : Smoothie banane, Pates pesto, Chili con carne  ->  1550 kcal, 56 g prot

Interpretation 5b — pourquoi le glouton ne trouve pas l’optimum global

Un glouton “jour par jour” choisirait, pour chaque jour, les 3 plats les moins chers satisfaisant la fenetre kcal — mais il ignorerait le couplage hebdomadaire : apres 2 repetitions, les plats les moins chers deviennent indisponibles (contrainte de variete), et le glouton se retrouve bloque ou contraint de prendre des plats chers en fin de semaine, sans avoir anticipe. Le Optimize() de Z3, lui, minimise le cout total sur les 7 jours simultanement : il repartit les repetitions bon marche sur toute la semaine pour minimiser la somme globale.

Capabilite exercee (Prong-B). La matrice booleenne Sel[7][24] (168 variables) est resolue en quelques centaines de millisecondes : l’optimisation SMT reste tractable a cette echelle. La frontiere de convergence est plus loin — un corpus RecipeML a ~11 000 recettes (variables Sel[7][11000] = 77 000 Booleens par jour) sortirait du regime d’un simple Optimize() et demanderait une decomposition (column-generation, Lagrangian relaxation) : c’est la limite honnete de la “couverture bornee” d’un solveur SMT monocall, signalee dans l’Epic #1206.

Lecture chiffree — quatre ordres de grandeur sur le corpus de jouet. Le plan a cout minimal ci-dessus (D=7, 24 plats) se resout en une fraction de seconde dans ce notebook (le temps exact est imprime par la cellule de code ci-dessus) ; le 16 mesure, sur le meme corpus de jouet, l’enumeration des 36 combinaisons 0,06 ms, le plan SMT booleen D=3 2,4 ms et l’Optimize a cout minimal D=1 17,7 ms. L’enumeration gagne partout ou elle reste tractable — mais sa pente est exponentielle en le nombre de variables quand celle du solveur suit la combinatoire contrainte. Passer de 3 a 7 jours avec corpus elargi et contrainte de variete coute environ deux ordres de grandeur (millisecondes -> fraction de seconde) : observation sur cette paire de runs, pas une loi (jours et corpus changent en meme temps). La lecture pratique : le temps du solveur achete l’exactitude a l’echelle ou l’enumeration explose, et la fenetre [1400, 1900] kcal avec 40 g de proteines reste resolue en moins d’une seconde a D=7.

Synthèse — du SAT à l’OPT sur corpus réel

Question Notebook API Réponse
Existe-t-il un menu conforme ? 16c / 16d Solver SAT / UNSAT
Quel est le meilleur menu ? ce notebook Optimize optimum + front de Pareto

Le grain non-miroir de la track Python-large : le corpus réel Ciqual × RecipeML (R=594) est confié pour la première fois à un solveur d’optimisation, en réutilisant l’encodage one-hot PB qui passe à l’échelle (16d). Trois familles font leur entrée dans la track Python :

  1. minimize / maximize — le solveur trouve l’optimum global en un appel (vs dichotomie, vs glouton sous-optimal).
  2. add_soft — MaxSAT pondéré natif (zéro occurrence Python repo-wide auparavant ; Z3-Python-06 l’émulait à la main).
  3. priority='box' (bornes indépendantes en un check, net-new — inutilisé repo-wide) + scalarisation pour le front de Pareto pratique (06 l’émulait par boucle sur toy corpus ; ici sur R=594).

Honnêteté de port. Ce n’est pas un port du C# 14_Optimize_MaxSAT (DSL + toy knapsack/nurse-roster) : l’optimisation est construite à frais nouveaux sur le corpus réel du meal-planner. Le toy 16 faisait déjà minimize(cost) sur 24 plats — matière consolidée ici (§6b) ; ce notebook l’étend à R=594 et ajoute add_soft + Pareto natif, absents du toy. Les timing absolus dépendent de l’encodage (les pools rendent l’optimum tractable en secondes) ; l’enseignement porté est le passage SAT→OPT à l’échelle.

Deep-queue #1206 : G1 (data-layer) → G2 (capstone) → G3 (convergence-scale) → G4 (ce notebook) → G5 (hygiène retrofit, LIGHT/dernier).

7. Exercices

Les variables sel0, selW, opt_*, pool, vint, restr, cats_of_course, SEL/PROT/GLU/LIP restent en portée.

Exercice 1 — Minimiser le coût sous contrainte de variété maximale

On a minimisé le sel. Définissez un « coût » arbitraire (ex. pénaliser les recettes dont le titre contient un mot-clé « cher » ou utiliser la couverture d’appariement cover comme proxy inverse de qualité) et minimisez-le, tout en maximisant la variété (nombre de catégories distinctes dans le menu).

# Exercice 1 -- minimiser un cout en maximisant la variete (multi-objectif).
# TODO: definir une fonction de cout (ex: penaliser mots-cles, ou 1/cover comme proxy),
#       opt.minimize(cout) + opt.maximize(variete), priority='pareto' pour le compromis.
print("Exercice 1 a completer : cout minimal vs variete maximale (front de Pareto).")
Exercice 1 a completer : cout minimal vs variete maximale (front de Pareto).

Exercice 2 — Préférence patient multi-niveaux (MaxSAT hiérarchique)

Le patient a des préférences par ordre de priorité : (1) aucun fruit à coque, (2) préfère le poisson à la viande rouge, (3) aime le chocolat. Modélisez-les avec add_soft à poids croissants (ex. 100 / 10 / 1) — le solveur satisfera d’abord les priorités élevées. Comparez avec priority='lex' (domination lexicographique stricte).

# Exercice 2 -- preferences patient multi-niveaux (MaxSAT hierarchique).
# TODO: 3 add_soft a poids croissants (100/10/1) sur des clauses de preference,
#       puis comparer avec opt.set('priority','lex') pour une domination lexicographique stricte.
print("Exercice 2 a completer : MaxSAT hierarchique (poids croissants) vs priority='lex'.")
Exercice 2 a completer : MaxSAT hierarchique (poids croissants) vs priority='lex'.

Exercice 3 — Optimiser le plan hebdomadaire en protéines (borne box)

Le §6 minimise le sel du plan semaine. Utilisez priority='box' pour obtenir, sur le même encodage, le maximum absolu de protéines (sans égard au sel) ET le minimum absolu de sel — les deux bornes qui cadrent le compromis hebdomadaire.

# Exercice 3 -- bornes box sur le plan hebdomadaire.
# TODO: reutiliser selW, opt.set('priority','box'), opt.minimize(week_sel) + opt.maximize(week_prot),
#       lire h_sel.upper() et h_prot.upper() = les deux bornes independantes.
print("Exercice 3 a completer : bornes independantes (box) sel-min / prot-max du plan semaine.")
Exercice 3 a completer : bornes independantes (box) sel-min / prot-max du plan semaine.
Retour au sommet