← 15 - Tableaux imbriqués et grilles 2D | README Z3-Python

16. Meal-Planner déclaratif : du modèle Z3 au plan hebdomadaire visualisé

Après les puzzles (Sudoku, carré magique) et les grilles 2D, on applique la programmation par contraintes à un problème d’optimisation réaliste : composer un menu équilibré à partir d’une base d’aliments, puis un plan hebdomadaire complet. C’est le saut de la satisfiabilité (« existe-t-il une solution ? ») à l’optimisation sous contraintes (« quelle est la solution la moins chère / la plus variée ? »).

Ce notebook porte le C# 06_Meal_Planner_Modelisation (Z3.Linq) vers z3-py et compare trois approches de modélisation d’un même problème — index-based, énumération, booléenne — puis montre comment Optimize trouve le menu minimal en coût, et comment un modèle à matrice booléenne jours × plats produit un plan hebdomadaire que ne sait pas énumérer une heuristique gloutonne (prong B : le couplage fenêtre-calorique × variété est non compositionnel).

Aller plus loin : la jambe Python-large (corpus réel). Ce notebook pose la modélisation sur un corpus jouet (10 puis 24 plats saisis à la main). La track se poursuit sur un corpus réel Ciqual × RecipeML (R ≈ 594 recettes) : 16b — couche de données · 16c — capstone patient · 16d — convergence à l’échelle · 16e — optimisation.

# Imports : z3 (solveur SMT + Optimize + pseudo-Booleen) + time (mesure de resolution).
from z3 import (Solver, Optimize, Int, Bool, And, Or, Not, Implies, If,
                Sum, PbEq, sat, unsat, set_param)
import time
set_param('parallel.enable', False)

# Base de donnees nutritionnelle : (nom, kcal, proteines_g, cout_centimes, categorie).
FOODS = [
    ("Salade verte",      80,  2,  300, "entree"),
    ("Soupe de legumes", 120,  4,  250, "entree"),
    ("Carpaccio",        150, 15,  600, "entree"),
    ("Poulet roti",      350, 30,  500, "plat"),
    ("Saumon grille",    300, 28,  800, "plat"),
    ("Pates bolognaise", 450, 18,  350, "plat"),
    ("Risotto",          400, 10,  400, "plat"),
    ("Salade de fruits", 100,  1,  200, "dessert"),
    ("Mousse au chocolat",200, 5,  250, "dessert"),
    ("Tiramisu",         250,  7,  350, "dessert"),
]
NAMES, KCALS, PROTS, COSTS, CATS = map(list, zip(*FOODS))
CATS_SET = ("entree", "plat", "dessert")
print(f"Base nutritionnelle : {len(FOODS)} aliments ({sum(c=='entree' for c in CATS)} entrees, "
      f"{sum(c=='plat' for c in CATS)} plats, {sum(c=='dessert' for c in CATS)} desserts).")

Base nutritionnelle : 10 aliments (3 entrees, 4 plats, 3 desserts).

def exactement_un(solver, booleens):
    # Contrainte 'exactement un vrai' parmi une liste de Bool z3.
    # Encode nativement une contrainte pseudo-booleenne : la somme ponderee (coeffs tous 1)
    # egale 1 -- c'est-a-dire 'au moins un' ET 'au plus un' en UNE assertion, au lieu de
    # l'encodage naif (Or + exclusion pairwise en O(n^2)). Idiom PbEq retrouve a l'echelle
    # reelle dans les notebooks 16c/16d (cf. forward-links en conclusion).
    solver.add(PbEq([(b, 1) for b in booleens], 1))

print("Helper exactement_un defini (PbEq natif : exactement-un en 1 assertion, vs O(n^2) pairwise).")

Helper exactement_un defini (PbEq natif : exactement-un en 1 assertion, vs O(n^2) pairwise).

1. Approche index-based : un Int par catégorie

L’encodage le plus direct : une variable Int par catégorie, dont la valeur est l’index de l’aliment choisi. La contrainte de bornes (0 <= idx < taille) suffit à garantir un choix valide. Sans contrainte nutritionnelle, le solveur renvoie la première affectation (souvent les index 0). Cette approche est simple mais mal adaptée aux contraintes nutritionnelles (l’index n’a pas de relation linéaire naturelle avec les kcal/protéines — il faut une table de lookup, moins élégante que l’approche booléenne suivante).

def menu_index():
    s = Solver()
    ie = Int("idx_entree")   # index de l'entree
    ip = Int("idx_plat")
    id_ = Int("idx_dessert")
    # bornes : 3 entrees, 4 plats, 3 desserts
    s.add(ie >= 0, ie <= 2, ip >= 0, ip <= 3, id_ >= 0, id_ <= 2)
    assert s.check() == sat
    m = s.model()
    # resolution des index vers les aliments (lookup Python hors solveur)
    entrees = [i for i in range(len(FOODS)) if CATS[i] == "entree"]
    plats   = [i for i in range(len(FOODS)) if CATS[i] == "plat"]
    desserts= [i for i in range(len(FOODS)) if CATS[i] == "dessert"]
    e, p, d = entrees[m.eval(ie).as_long()], plats[m.eval(ip).as_long()], desserts[m.eval(id_).as_long()]
    cal = KCALS[e] + KCALS[p] + KCALS[d]
    return NAMES[e], NAMES[p], NAMES[d], cal

e, p, d, cal = menu_index()
print(f"Menu index-based (sans contrainte nutritionnelle) :")
print(f"  Entree  : {e}")
print(f"  Plat    : {p}")
print(f"  Dessert : {d}")
print(f"  Total   : {cal} kcal")

Menu index-based (sans contrainte nutritionnelle) :
  Entree  : Salade verte
  Plat    : Poulet roti
  Dessert : Salade de fruits
  Total   : 530 kcal

Interprétation 1 — index vs caractéristiques

L’index est un handle opaque : le solveur ne « sait » pas que l’index 0 (Salade) a 80 kcal et l’index 2 (Carpaccio) en a 150. Pour ajouter une contrainte « total entre 600 et 900 kcal », il faut relier l’index aux caractéristiques, ce qui demande une table de lookup ou un grand If/elif — verbeux. L’approche booléenne (§3) rend cette relation native.

2. Approche par énumération + filtrage

Avant Z3, on résoudrait ce problème par énumération exhaustive : générer tous les triples (entree, plat, dessert), filtrer ceux qui satisfont les contraintes nutritionnelles, puis prendre le moins cher. Cela marche pour 3×4×3 = 36 combinaisons, mais explose avec la taille (un plan hebdomadaire à 9 plats³/jour × 5 jours = ~59000 milliards de combinaisons). Cette approche sert de baseline de complexité pour mesurer ce que Z3 évite.

from itertools import product

def menu_enumeration():
    entrees = [i for i in range(len(FOODS)) if CATS[i] == "entree"]
    plats   = [i for i in range(len(FOODS)) if CATS[i] == "plat"]
    desserts= [i for i in range(len(FOODS)) if CATS[i] == "dessert"]
    valides = []
    for e, p, d in product(entrees, plats, desserts):
        cal = KCALS[e] + KCALS[p] + KCALS[d]
        prot = PROTS[e] + PROTS[p] + PROTS[d]
        cost = COSTS[e] + COSTS[p] + COSTS[d]
        if 600 <= cal <= 900 and prot >= 25 and cost <= 1200:
            valides.append((e, p, d, cal, prot, cost))
    return valides

t0 = time.perf_counter()
valides = menu_enumeration()
t1 = time.perf_counter()
print(f"Enumeration : {len(valides)} menus valides sur 36 combinaisons en {(t1-t0)*1000:.2f} ms")
if valides:
    # menu le moins cher par enumeration
    best = min(valides, key=lambda x: x[5])
    e, p, d, cal, prot, cost = best
    print(f"Menu le moins cher : {NAMES[e]} + {NAMES[p]} + {NAMES[d]}")
    print(f"  -> {cal} kcal, {prot}g prot, {cost/100:.2f} EUR")

Enumeration : 11 menus valides sur 36 combinaisons en 0.04 ms
Menu le moins cher : Soupe de legumes + Pates bolognaise + Mousse au chocolat
  -> 770 kcal, 27g prot, 8.50 EUR

Interprétation 2 — la malédiction de la dimension

36 combinaisons, c’est instantané. Mais chaque dimension supplémentaire multiplie le coût : passer à 4 catégories de 10 aliments = 10⁴ = 10000 ; un plan sur 5 jours avec 3 choix/jour = ~1.7×10⁷. L’énumération est en O(produit des domaines) — exponentiel en le nombre de variables. Z3, lui, raisonne sur les contraintes symboliquement (propagation + apprentissage de clauses), sans énumérer — c’est tout l’intérêt de l’approche booléenne suivante.

3. Approche booléenne : une variable Bool par aliment

L’encodage idiomatique : une variable booléenne par aliment (sel_i = « l’aliment i est choisi »). Les contraintes deviennent naturelles :

• Exactement 1 entrée/plat/dessert : Or(...) + exclusion pairwise (helper exactement_un).
• Total calorique : Sum(If(sel_i, kcal_i, 0)) — la table de lookup disparaît, chaque aliment porte ses caractéristiques dans l’expression.

Le solveur explore l’espace des affectations booléennes par propagation, sans énumérer.

def menu_booleen():
    s = Solver()
    sel = [Bool(f"sel_{i}") for i in range(len(FOODS))]
    # exactement 1 par categorie
    for cat in CATS_SET:
        exactement_un(s, [sel[i] for i in range(len(FOODS)) if CATS[i] == cat])
    # contraintes nutritionnelles : If(sel_i, val_i, 0) relie nativement selection et caracteristique
    total_cal  = Sum([If(sel[i], KCALS[i], 0)  for i in range(len(FOODS))])
    total_prot = Sum([If(sel[i], PROTS[i], 0)  for i in range(len(FOODS))])
    total_cost = Sum([If(sel[i], COSTS[i], 0)  for i in range(len(FOODS))])
    s.add(total_cal >= 600, total_cal <= 900)
    s.add(total_prot >= 25)
    s.add(total_cost <= 1200)
    if s.check() == sat:
        m = s.model()
        choisi = [(NAMES[i], CATS[i], KCALS[i], PROTS[i], COSTS[i])
                  for i in range(len(FOODS)) if m.eval(sel[i])]
        return choisi
    return None

menu = menu_booleen()
print("Menu equilibre (approche booleenne) :")
cal = prot = cost = 0
for nom, cat, k, pr, co in menu:
    print(f"  [{cat:8s}] {nom:20s} {k:4d} kcal, {pr:2d}g prot, {co/100:.2f} EUR")
    cal += k; prot += pr; cost += co
print(f"  --- Total : {cal} kcal, {prot}g proteines, {cost/100:.2f} EUR ---")

Menu equilibre (approche booleenne) :
  [entree  ] Salade verte           80 kcal,  2g prot, 3.00 EUR
  [plat    ] Poulet roti           350 kcal, 30g prot, 5.00 EUR
  [dessert ] Mousse au chocolat    200 kcal,  5g prot, 2.50 EUR
  --- Total : 630 kcal, 37g proteines, 10.50 EUR ---

Interprétation 3 — If(bool, val, 0) comme table de lookup symbolique

La expression If(sel_i, kcal_i, 0) est l’équivalent symbolique d’une table de lookup : elle « active » la caractéristique de l’aliment i si et seulement s’il est sélectionné. Le solveur propage ces sommes linéaires sans énumération — c’est ce qui rend l’approche booléenne passage à l’échelle là où l’énumération explose.

4. Optimisation : le menu équilibré le moins cher

Solver répond sat/unsat ; Optimize ajoute un objectif (minimiser ou maximiser) sous les mêmes contraintes. On demande ici le menu équilibré (600-900 kcal, ≥25g prot) de coût minimal. Optimize.minimize(cout) pousse le solveur vers le coût le plus bas en un seul appel — là où une recherche dichotomique manuelle nécessiterait N appels Solver.

def menu_min_cout():
    opt = Optimize()
    sel = [Bool(f"sel_{i}") for i in range(len(FOODS))]
    for cat in CATS_SET:
        exactement_un(opt, [sel[i] for i in range(len(FOODS)) if CATS[i] == cat])
    total_cal  = Sum([If(sel[i], KCALS[i], 0) for i in range(len(FOODS))])
    total_prot = Sum([If(sel[i], PROTS[i], 0) for i in range(len(FOODS))])
    total_cost = Sum([If(sel[i], COSTS[i], 0) for i in range(len(FOODS))])
    opt.add(total_cal >= 600, total_cal <= 900, total_prot >= 25)
    opt.minimize(total_cost)   # un seul appel, pas de dichotomie manuelle
    assert opt.check() == sat
    m = opt.model()
    choisi = [(NAMES[i], KCALS[i], PROTS[i], COSTS[i])
              for i in range(len(FOODS)) if m.eval(sel[i])]
    return choisi

t0 = time.perf_counter()
menu_opt = menu_min_cout()
t1 = time.perf_counter()
cost = sum(c for _, _, _, c in menu_opt)
print(f"Menu MIN-COUT (Optimize.minimize, {(t1-t0)*1000:.1f} ms) :")
for nom, k, pr, co in menu_opt:
    print(f"  {nom:20s} {k:4d} kcal, {pr:2d}g prot, {co/100:.2f} EUR")
print(f"  --- Cout total minimal : {cost/100:.2f} EUR ---")

Menu MIN-COUT (Optimize.minimize, 6.9 ms) :
  Soupe de legumes      120 kcal,  4g prot, 2.50 EUR
  Pates bolognaise      450 kcal, 18g prot, 3.50 EUR
  Mousse au chocolat    200 kcal,  5g prot, 2.50 EUR
  --- Cout total minimal : 8.50 EUR ---

Interprétation 4 — minimize vs dichotomie

Optimize.minimize encapsule la recherche d’optimum : le solveur combine la satisfiabilité des contraintes avec la poursuite de l’objectif, en utilisant des algorithmes spécialisés (OBBTP, maxres selon la théorie). L’alternative manuelle — une dichotomie sur le coût (Solver avec cost <= mid, resserrer mid jusqu’à unsat) — marche mais demande N appels et une logique de boucle. Optimize le fait en un appel, et généralise (maximize, objectifs multiples, front de Pareto — cf. notebook 06).

Lecture chiffrée — le prix de l’équilibre et l’optimum confirmé deux fois. Trois menus se lisent ensemble : le moins cher (énumération §2 et Optimize §4) rend 8,50 EUR pour 770 kcal et 27 g de protéines ; le menu équilibré (§3) rend 10,50 EUR pour 630 kcal et 37 g ; le menu libre sans contrainte (§1) tombe à 530 kcal. L’équilibre nutritionnel se facture : +2,00 EUR/jour et l’abandon de 140 kcal par rapport au menu le moins cher, en échange de +10 g de protéines — un solveur ne « préfère » pas l’équilibre, il le facture. Et l’optimum de coût se lit en croisant deux méthodes indépendantes : l’énumération exhaustive (36 combinaisons filtrées sur 36) et l’Optimize SMT rendent le même minimum 8,50 EUR avec le même menu (soupe de légumes + pâtes à la bolognaise + mousse au chocolat). Deux algorithmes sans aucune ligne de code en commun qui convergent vers le même chiffre : c’est la validation la plus forte disponible sur un petit domaine — et la raison pour laquelle l’énumération reste le témoin de référence tant qu’elle reste tractable.

5. Plan hebdomadaire : la matrice booléenne jours × plats (prong B)

Le morceau de résistance : composer un plan sur D jours où chaque jour a 1 petit-déjeuner, 1 déjeuner, 1 dîner, chaque plat servi au plus une fois dans la semaine (variété), et chaque jour dans une fenêtre calorique [DAY_LO, DAY_HI]. L’encodage : une matrice booléenne Sel[j][i] (jour j, plat i).

Pourquoi c’est le prong B : une heuristique gloutonne (remplir jour par jour avec le premier trio valide restant) se bloque — la combinatoire « fenêtre × variété » n’est pas compositionnelle (un choix local optimal rend le lendemain infaisable). Z3, lui, raisonne sur tous les jours simultanément et trouve un plan global. C’est là que le solveur démontre sa valeur par rapport à une heuristique naïve.

# Corpus de plats : (nom, categorie, kcal, proteines_g, cout_centimes).
DISHES = [
    ("Porridge fruits rouges", "breakfast", 300, 12, 180),
    ("Yaourt granola",         "breakfast", 350, 18, 220),
    ("Oeufs brouilles",        "breakfast", 400, 22, 280),
    ("Salade cesar",           "lunch",     500, 25, 650),
    ("Wrap poulet",            "lunch",     550, 30, 580),
    ("Quiche epinards",        "lunch",     600, 20, 520),
    ("Poulet curry",           "dinner",    650, 35, 700),
    ("Saumon four",            "dinner",    700, 32, 850),
    ("Risotto champignons",    "dinner",    750, 18, 600),
]
DN = [d[0] for d in DISHES]
DC = [d[1] for d in DISHES]
DK = [d[2] for d in DISHES]
DCAT_SET = ("breakfast", "lunch", "dinner")
ND = len(DISHES)
D = 3                      # 3 jours (lundi..mercredi) — borne pour un runtime notebook
DAY_LO, DAY_HI = 1500, 1700  # fenetre kcal/jour (3 plats)
print(f"Corpus : {ND} plats ({sum(c=='breakfast' for c in DC)} bf, {sum(c=='lunch' for c in DC)} lunch, "
      f"{sum(c=='dinner' for c in DC)} dinner). Plan sur D={D} jours, fenetre [{DAY_LO},{DAY_HI}] kcal/jour.")

Corpus : 9 plats (3 bf, 3 lunch, 3 dinner). Plan sur D=3 jours, fenetre [1500,1700] kcal/jour.

def plan_hebdomadaire():
    s = Solver()
    # Sel[j][i] = True ssi le plat i est servi le jour j.
    Sel = [[Bool(f"S_{j}_{i}") for i in range(ND)] for j in range(D)]
    # (1) 1 plat par categorie et par jour.
    for j in range(D):
        for cat in DCAT_SET:
            exactement_un(s, [Sel[j][i] for i in range(ND) if DC[i] == cat])
    # (2) Variete globale : chaque plat au plus 1 fois dans la semaine.
    for i in range(ND):
        s.add(Sum([If(Sel[j][i], 1, 0) for j in range(D)]) <= 1)
    # (3) Fenetre kcal par jour.
    for j in range(D):
        day_cal = Sum([If(Sel[j][i], DK[i], 0) for i in range(ND)])
        s.add(day_cal >= DAY_LO, day_cal <= DAY_HI)
    t0 = time.perf_counter()
    status = s.check()
    t1 = time.perf_counter()
    plan = None
    if status == sat:
        m = s.model()
        plan = [[DN[i] for i in range(ND) if m.eval(Sel[j][i])] for j in range(D)]
    return plan, (t1 - t0) * 1000

plan, ms = plan_hebdomadaire()
print(f"\n=== Plan hebdomadaire SMT (D={D} jours, resolu en {ms:.1f} ms) ===")
if plan:
    for j, day in enumerate(plan):
        kcal = sum(DK[DN.index(d)] for d in day)
        print(f"  Jour {j+1} : {', '.join(day)}  ->  {kcal} kcal")
else:
    print("  Aucun plan (UNSAT) — relacher les contraintes.")

=== Plan hebdomadaire SMT (D=3 jours, resolu en 1.4 ms) ===
  Jour 1 : Oeufs brouilles, Salade cesar, Poulet curry  ->  1550 kcal
  Jour 2 : Yaourt granola, Wrap poulet, Saumon four  ->  1600 kcal
  Jour 3 : Porridge fruits rouges, Quiche epinards, Risotto champignons  ->  1650 kcal

Interprétation 5 — pourquoi le glouton échoue là où Z3 réussit

Le glouton remplit le jour 1 avec le premier trio (breakfast+ lunch + dinner) qui tombe dans la fenêtre kcal, marque ces plats comme « utilisés », puis passe au jour 2. Le problème : ce trio local peut consommer les seuls plats qui rendraient le jour 3 faisable. La combinatoire (fenêtre × variété) n’est pas compositionnelle — optimiser jour par jour ne garantit pas la faisabilité globale. Z3, en revanche, considère simultanément les D jours : il peut « sacrifier » l’optimum local du jour 1 pour préserver la faisabilité des jours suivants. C’est précisément la capacité distinctive d’un solveur SMT face à une heuristique gloutonne — l’argument central (prong B) pour la programmation par contraintes.

Variante optimisée : le même plan, mais à coût minimal et à l’échelle (corpus de 24 plats, D=7), est consolidé dans 16e — optimisation (§6b).

6. Exercices

Exercice 1 — Ajouter une contrainte de macro-nutriments (glucides + lipides)

Étendez la base nutritionnelle avec des champs carbs (glucides) et fat (lipides), puis ajoutez au modèle booléen (§3) une contrainte « 45-65 % des kcal en glucides » (4 kcal/g). Combien de menus valides restent ?

Indice : total_carbs_g = Sum([If(sel_i, carbs_i, 0) ...]), puis total_carbs_g * 4 >= 0.45 * total_cal et <= 0.65 * total_cal. Multipliez par 100 pour rester en arithmétique entière.

# Exercice 1 : contrainte macro glucides (45-65% des kcal, 4 kcal/g).
# TODO etudiant :
# Etape 1 : ajouter carbs_g a chaque aliment de FOODS.
# Etape 2 : calculer total_carbs_g via Sum(If(sel_i, carbs_i, 0)).
# Etape 3 : ajouter total_carbs_g*4 >= 0.45*total_cal ET <= 0.65*total_cal (x100 pour entiers).
# Etape 4 : compter les solutions (negation du modele + boucle).
print("Exercice 1 a completer : contrainte macro glucides (45-65%).")

Exercice 1 a completer : contrainte macro glucides (45-65%).

Exercice 2 — Plan hebdomadaire à variété maximale

Reconstruisez la matrice booléenne Sel[j][i] du §5 (9 plats, D = 3, variété ≤ 1), puis changez l’objectif : au lieu de la faisabilité, maximisez le nombre de plats distincts servis sur la semaine. Combien des 9 plats le solveur parvient-il à utiliser au moins une fois ? Pourquoi la contrainte « 1 plat par catégorie et par jour » fixe-t-elle un plafond théorique à cette variété ?

Indice : distinct_count = Sum([If(Or([Sel[j][i] for j in range(D)]), 1, 0) for i in range(ND)]), puis opt.maximize(distinct_count). Trois usages du même encodage booléen : faisabilité (§5), coût minimal (§4), variété maximale (ici). La version à l’échelle de cette question (corpus élargi, D=7) est traitée dans 16e.

# Exercice 2 : plan hebdomadaire a VARIETE MAXIMALE (Optimize.maximize).
# TODO etudiant :
# Etape 1 : reconstruire la matrice Sel[j][i] du §5 (9 plats, D=3, variete <= 1).
# Etape 2 : distinct_count = Sum(If(Or(Sel[j][i] pour tout j), 1, 0) pour tout i).
# Etape 3 : opt.maximize(distinct_count) ; afficher le plan + le nombre de plats distincts.
print("Exercice 2 a completer : variete maximale sur la matrice du S5 (maximiser les plats distincts).")

Exercice 2 a completer : variete maximale sur la matrice du S5 (maximiser les plats distincts).

Exercice 3 — Démontrer l’échec du glouton (prong B)

Implémentez le glouton décrit au §5 (remplir jour par jour avec le premier trio valide restant) sur le corpus à 9 plats avec D = 3. Montrez qu’il échoue (se bloque avant le jour 3) là où Z3 trouve un plan. Que se passe-t-il si vous changez l’ordre des plats dans le corpus ?

Indice : boucle for j in range(D), à chaque jour parcourir les plats dans l’ordre, prendre le premier breakfast+lunch+dinner dont la somme kcal est dans [DAY_LO, DAY_HI] et qui n’est pas déjà utilisé. Si aucun trio — échec. Comparer au plan SMT.

# Exercice 3 : glouton sequential sur D=3 jours, demontrer qu'il se bloque.
# TODO etudiant :
# Etape 1 : parcourir les jours en sequence.
# Etape 2 : pour chaque jour, premier trio (bf+ lunch+dinner) valide et non-utilise.
# Etape 3 : si aucun trio -> echec (print). Comparer au plan SMT de la cellule precedente.
print("Exercice 3 a completer : demontrer l'echec du glouton vs SMT.")

Exercice 3 a completer : demontrer l'echec du glouton vs SMT.

Conclusion

Ce notebook a porté le meal-planner déclaratif du C# Z3.Linq vers z3-py, en montrant trois encodages du même problème (index / énumération / booléen), l’optimisation du coût via Optimize.minimize, et un plan hebdomadaire à matrice booléenne qui démontre la supériorité du solveur sur une heuristique gloutonne (prong B : la combinatoire fenêtre × variété n’est pas compositionnelle).

Leçons clés :

1. L’encodage booléen (If(sel_i, val_i, 0)) rend la relation sélection-caractéristique native, là où l’index demande une table de lookup.
2. Optimize sous-traite la recherche d’optimum (un appel) là où la dichotomie manuelle en demanderait N.
3. Le couplage multi-jours (variété globale + fenêtre par jour) est exactement le genre de problème où un solveur SMT bat une heuristique : la décision locale optimale n’est pas globalement faisable.

Ce notebook est le premier d’une série appliquée : les C# 07-09 (données externes, capstone patient, convergence à l’échelle) étendent ce socle vers des données réelles et la passage-à-l’échelle.

← 15 - Tableaux imbriqués et grilles 2D | README Z3-Python

---

Suite de la track (corpus réel). Ce notebook reste sur un corpus jouet. L’idiom PbEq (pseudo-booléen natif) utilisé ici pour exactement_un est la clé qui rend le meal-planner tractable à l’échelle réelle (~594 recettes) : cf. 16b (données), 16c (capstone patient), 16d (convergence : l’encodage décide), 16e (optimisation + MaxSAT + Pareto).