Z3-Python-16d — Convergence à l’échelle : l’encodage décide de la tractabilité

Clôture du bloc meal-planner (Epic #4677, jambe Python-large du planificateur #1206). Suite de 16b (couche de données réelles : Ciqual × RecipeML, appariement lexical flou, agrégation pondérée par la masse) et de 16c (capstone patient : 5 familles de contraintes, idiom index + linking). Ce notebook 16d branche enfin le solveur sur le cache réel de 16b, et y rencontre le problème que les corpus jouets masquaient : à l’échelle, l’encodage naïf explose dès la construction, l’encodage le plus compact (théorie des tableaux) devient insoluble, et seul l’encodage one-hot pseudo-booléen se construit et se résout.

Port fidèle du C# 09_Meal_Planner_Convergence_Scale (Z3-Linq2Z3). Le C# utilise l’API Microsoft.Z3 brute (Stack B, car le DSL Z3.Linq n’expose pas les contraintes pseudo-booléennes). Le port Python utilise z3-solver : l’idiome équivalent est PbEq / PbLe / PbGe (liste de paires (booléen, coefficient) + seuil k).

Stack : API brute z3-solver — le cœur de la leçon est l’encodage pseudo-booléen, une famille de contraintes que le DSL Z3.Linq n’expose pas.

Question de convergence. Le problème fidèle reste-t-il tractable quand on remonte à l’échelle réelle (7 menus × 5 créneaux × ~R recettes × constituants Ciqual) ? La puissance brute du solveur Z3 suffit-elle, ou le choix d’encodage décide-t-il seul de la tractabilité ?

Insight clé. Plus de recettes = plus de solutions possibles, pas plus de contraintes : des recettes supplémentaires sont des contraintes enablantes (elles élargissent l’espace des modèles). C’est l’encodage — pas le solveur — qui décide si cet espace est explorable.

Échelle démonstrative. Ce notebook tourne sur le sous-ensemble du corpus produit par 16b (ici R recettes solveur-usables). Les verdicts qualitatifs — naïf qui explose, théorie des tableaux qui reste unknown, one-hot qui se résout — sont reproductibles à cette échelle et se renforcent à R=2387 (mesuré sur le port C#). Le notebook C# 09 fournit l’étalon à l’échelle du corpus plein ; les timing absolus en Python sont plus lents qu’en C# (overhead ctypes par assertion, ~10-20×), mais l’ordre relatif des trois encodages est inchangé.

Navigation : << 16c - Capstone patient | 16e - Optimize >> | README Z3-Python

Objectifs

  1. Constater que l’encodage naïf (index + disjonction, celui de 16c) explose dès la construction à l’échelle réelle.
  2. Constater que l’encodage le plus compact à écrire — la théorie des tableaux (Select/Store) — est insoluble (unknown).
  3. Maîtriser l’encodage qui passe à l’échelle : le one-hot pseudo-booléen (PbEq / PbLe / PbGe).
  4. Comprendre pourquoi : les recettes sont des contraintes enablantes, et la somme pondérée de booléens est du ressort du solveur pseudo-booléen natif de Z3, pas de l’arithmétique linéaire générale.

Prérequis : 16 (modélisation, corpus jouet), 16b (cache réel), 16c (idiom index + linking).

1. Données : le cache solveur-usable produit par 16b

Le notebook 16b a construit un cache data/meals/mealplan_cache.json : recettes RecipeML appariées à Ciqual, agrégation pondérée par la masse, sous-ensemble gaté par qualité (couverture d’appariement ≥ 80%). Chaque recette porte un vecteur de C=5 constituants à l’échelle de la recette entière (kJ, g) — pas per-100g. On charge ce cache : c’est le seul corpus qui rende la question de tractabilité non triviale.

# Chargement du cache solveur-usable produit par 16b (le seul corpus non-jouet).
import json, time
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"
assert CACHE.exists(), (
    f"Cache absent : {CACHE}. Executez d'abord le notebook 16b (couche de donnees) de bout en bout."
)
doc = json.loads(CACHE.read_text(encoding="utf-8"))
constituants = doc["constituants"]          # [str x C]
C = len(constituants)
# plats : (title tronque, vec de C floats a l'echelle recette entiere, cats RecipeML)
plats = [(r["title"].strip()[:40], [float(v) for v in r["vec"]], list(r["cats"]))
         for r in doc["recipes"]]
R = len(plats)
N_TOTAL = doc["n_total"]
print(f"Cache charge : R={R} recettes solveur-usables (sur {N_TOTAL} brutes), C={C} constituants.")

# --- contract assertif : le cache respecte le schema attendu par les notebooks C# 08/09 ---
assert C == 5, f"C={C} (attendu 5 : Energie, Proteines, Glucides, Lipides, Sel)"
assert all(len(p[1]) == C for p in plats), "chaque vec doit avoir C=5 constituants"
assert isinstance(N_TOTAL, int) and N_TOTAL >= R

def pq(c, q):
    # quantile TRONQUE (index dans la liste triee), pas interpole -- ne pas utiliser numpy.percentile
    vals = sorted(p[1][c] for p in plats)
    return vals[int(q * (len(vals) - 1))]

print("Quartiles par constituant (echelle : recette ENTIERE, agregation ponderee par la masse) :")
for c in range(C):
    nom = (constituants[c])[:38]
    print(f"   [{c}] {nom:<38} P25={round(pq(c,0.25),1):>8}  mediane={round(pq(c,0.5),1):>8}  P75={round(pq(c,0.75),1):>8}")
Cache charge : R=712 recettes solveur-usables (sur 1465 brutes), C=5 constituants.
Quartiles par constituant (echelle : recette ENTIERE, agregation ponderee par la masse) :
   [0] Energie, Règlement UE N° 1169/2011 (kJ P25=  5052.1  mediane=  9995.7  P75= 16417.6
   [1] Protéines, N x facteur de Jones (g/100 P25=    20.6  mediane=    47.8  P75=    76.3
   [2] Glucides (g/100 g)                     P25=    54.9  mediane=   196.4  P75=   397.6
   [3] Lipides (g/100 g)                      P25=    38.1  mediane=   119.1  P75=   245.8
   [4] Sel chlorure de sodium (g/100 g)       P25=     0.8  mediane=     2.6  P75=     6.6

Les quartiles calibrent les fenêtres nutritionnelles patient : les vecteurs étant à l’échelle de la recette entière (et non per-100g), des constantes héritées d’un autre encodage n’auraient aucun sens. La bande d’énergie [P20, P80] × 5 plats couvre l’IQR ; les protéines ont un plancher P30 × 5 ; le sel un plafond contraignant P70 × 5.

# Parametres du theoreme, partages par les trois encodages.
NMENUS, NPLATS = 7, 5
# valeurs entieres par constituant (banker's rounding : Python round() = ties-to-even, = C# Math.Round)
vint = [[int(round(p[1][c])) for p in plats] for c in range(C)]
# restrictions patient CALIBREES sur les quartiles mesures ci-dessus.
loE = NPLATS * int(pq(0, 0.20))   # energie/menu : bande large autour de l'IQR
hiE = NPLATS * int(pq(0, 0.80))
loP = NPLATS * int(pq(1, 0.30))   # proteines/menu : plancher realiste
hiS = max(1, NPLATS * int(pq(4, 0.70)))   # sel/menu : plafond contraignant
# CONVENTION : restr = [(constituantIndex, lo, hi)] avec -1 = "pas de borne sur ce cote".
# Chaque encodage branche sur lo >= 0 / hi >= 0.
restr = [(0, loE, hiE), (1, loP, -1), (4, -1, hiS)]
print(f"Theoreme : {NMENUS} menus x {NPLATS} plats, sur R={R} recettes (vecteurs recette entiere).")
print(f"   energie/menu in [{loE},{hiE}] kJ, proteines/menu >= {loP} g, sel/menu <= {hiS} g.")
Theoreme : 7 menus x 5 plats, sur R=712 recettes (vecteurs recette entiere).
   energie/menu in [20515,91485] kJ, proteines/menu >= 135 g, sel/menu <= 25 g.

2. Trois encodages du même théorème, trois comportements

Le théorème est fixe : 7 menus × 5 plats, chaque plat distinct sur la semaine (variété), chaque menu dans une fenêtre nutritionnelle. Seul l’encodage SMT change. On va voir trois comportements radicalement différents sur le même corpus réel.

2.1 Encodage naïf (disjonction) — explose dès la construction

L’encodage naïf (celui de 16c) introduit une variable de nutrition par créneau et, pour chaque recette, la disjonction créneau ≠ r OU nutrition == ligne[r]. Le nombre d’assertions croît en menus × plats × R × constituants : on ne mesure même pas la résolution, juste la construction.

# Encodage A -- naif : sonde de temps de CONSTRUCTION (la resolution ne demarre meme pas a l'echelle).
from z3 import Int, Solver, And, Or
def build_naive(rcap):
    s = Solver()
    pid = [[Int(f"q_{m}_{p}") for p in range(NPLATS)] for m in range(NMENUS)]   # index de recette par creneau
    na = 0
    t0 = time.perf_counter()
    for m in range(NMENUS):
        for p in range(NPLATS):
            s.add(And(pid[m][p] >= 0, pid[m][p] < rcap))
            for rr in range(rcap):
                for (cc, lo, hi) in restr:
                    nutr = Int(f"n_{m}_{p}_{cc}")    # meme nom => meme const Z3
                    s.add(Or(pid[m][p] != rr, nutr == vint[cc][rr]))   # linking disjunction
                    na += 1
    dt = time.perf_counter() - t0
    print(f"  naif R={rcap:>5} : {na:>8} disjonctions construites en {dt:.2f}s (CONSTRUCTION seule, sans resolution)")
    return na
for rcap in (100, 300, min(R, 1000)):
    build_naive(rcap)
print("  -> le cout de construction croit lineairement en R x menus x plats x contraintes :")
print("     a l'echelle reelle, le solveur n'a meme pas commence a chercher une solution.")
  naif R=  100 :    10500 disjonctions construites en 1.08s (CONSTRUCTION seule, sans resolution)
  naif R=  300 :    31500 disjonctions construites en 3.35s (CONSTRUCTION seule, sans resolution)
  naif R=  712 :    74760 disjonctions construites en 8.18s (CONSTRUCTION seule, sans resolution)
  -> le cout de construction croit lineairement en R x menus x plats x contraintes :
     a l'echelle reelle, le solveur n'a meme pas commence a chercher une solution.

2.2 Théorie des tableaux — compact à écrire, mais insoluble

La théorie des tableaux de Z3 (Select/Store, axiomes de McCarthy intégrés) exprime le mapping recette→nutrition de façon R-indépendante : un tableau par constituant, construit comme une chaîne de R Store concrets, lu par un index symbolique pid[m][p]. Compact à écrire… mais Z3 ne tranche pas les chaînes de Store symboliques empilées.

# Encodage B -- theorie des tableaux : compact, mais Z3 -> unknown sur de longues chaines de Store.
from z3 import IntSort, IntVal, K, Store, Select, Distinct, Sum, unknown
sb = Solver()
sb.set("timeout", 15000)    # plafond 15s : on attend unknown
arrs = []
for (cc, lo, hi) in restr:
    a = K(IntSort(), IntVal(0))                 # tableau constant 0
    for r in range(R):                          # chaine de R Store concrets
        a = Store(a, r, vint[cc][r])
    arrs.append((cc, lo, hi, a))
pid = [[Int(f"a_{m}_{p}") for p in range(NPLATS)] for m in range(NMENUS)]
flat = [pid[m][p] for m in range(NMENUS) for p in range(NPLATS)]
for v in flat:
    sb.add(v >= 0); sb.add(v < R)
sb.add(Distinct(flat))                          # variete : indices distincts
for m in range(NMENUS):
    for (cc, lo, hi, a) in arrs:
        tot = Sum([Select(a, pid[m][p]) for p in range(NPLATS)])
        if lo >= 0: sb.add(tot >= lo)
        if hi >= 0: sb.add(tot <= hi)
t0 = time.perf_counter(); res = sb.check(); dt = time.perf_counter() - t0
print(f"theorie des tableaux ({NMENUS*NPLATS} index, chaines de Store de longueur {R}) : {res} en {dt:.1f}s")
if res == unknown:
    print(f"   (reason_unknown: {sb.reason_unknown()})")
print("  -> compact a ECRIRE, mais insoluble : Z3 ne tranche pas les Store symboliques empiles. Compacite != resolubilite.")
theorie des tableaux (35 index, chaines de Store de longueur 712) : unknown en 15.1s
   (reason_unknown: timeout)
  -> compact a ECRIRE, mais insoluble : Z3 ne tranche pas les Store symboliques empiles. Compacite != resolubilite.

2.3 One-hot pseudo-booléen — l’encodage qui passe à l’échelle

L’encodage one-hot introduit un booléen sel[m][p][r] (« la recette r occupe le créneau p du menu m »). Trois familles de contraintes, toutes pseudo-booléennes natives de Z3 :

  • PbEq(.,1) par créneau : exactement une recette par créneau.
  • PbLe(.,1) par recette sur toute la semaine : chaque recette au plus une fois (= variété).
  • PbGe / PbLe pondérés par menu et par constituant : la fenêtre nutritionnelle devient une somme pondérée de booléens (coefficient = valeur de la recette), traitée par le solveur pseudo-booléen de Z3 — pas par l’arithmétique linéaire générale.

C’est cet encodage qui passe à l’échelle : les recettes sont des contraintes enablantes, le solveur trouve un modèle sans énumérer.

Idiome z3-py. PbEq([(b1,c1), (b2,c2), ...], k) = la somme pondérée des booléens (coefficients c_i) égale k. La signature C# prend deux tableaux parallèles (coeffs[], args[], k) ; z3-py fusionne en une liste de paires (booléen, coefficient).

# Encodage C -- one-hot pseudo-booleen : exactly-one + variete + bandes ponderees.
from z3 import Bool, PbEq, PbLe, PbGe, sat, is_true
s = Solver()
tB = time.perf_counter()
# sel[m][p][r] : la recette r occupe le creneau p du menu m.
sel = [[[Bool(f"s_{m}_{p}_{r}") for r in range(R)] for p in range(NPLATS)] for m in range(NMENUS)]
# exactement 1 recette / creneau  (PbEq, coeffs tous 1, k=1)
for m in range(NMENUS):
    for p in range(NPLATS):
        s.add(PbEq([(sel[m][p][r], 1) for r in range(R)], 1))
# variete : chaque recette <= 1x / semaine  (PbLe sur la colonne des menus x plats, pour un r fixe)
for r in range(R):
    s.add(PbLe([(sel[m][p][r], 1) for m in range(NMENUS) for p in range(NPLATS)], 1))
# fenetre nutritionnelle = somme ponderee de booleens (PB native), coeff = valeur de la recette
for m in range(NMENUS):
    for (cc, lo, hi) in restr:
        pairs = [(sel[m][p][r], int(vint[cc][r])) for p in range(NPLATS) for r in range(R)]
        if hi >= 0: s.add(PbLe(pairs, hi))
        if lo >= 0: s.add(PbGe(pairs, lo))
dtB = time.perf_counter() - tB
tS = time.perf_counter(); res = s.check(); dtS = time.perf_counter() - tS
print(f"one-hot R={R} ({NMENUS*NPLATS*R} booleens) : construction {dtB:.1f}s, resolution {dtS:.1f}s -> {res}")
if res == sat:
    mo = s.model()
    for m in range(NMENUS):
        names = []
        for p in range(NPLATS):
            for r in range(R):
                if is_true(mo.eval(sel[m][p][r], model_completion=True)):
                    names.append(plats[r][0])
        print(f"  Menu {m+1} : " + "  |  ".join(n[:18] for n in names))
one-hot R=712 (24920 booleens) : construction 2.5s, resolution 0.8s -> sat
  Menu 1 : 16th-Street Stew  |  (Sort of Light) Bo  |  Almond Crecents  |  1990 2nd Place Mom  |  Almond Biscotti
  Menu 2 : Almond Torte Desse  |  African Vegetable   |  1986 Winner Impati  |  African Vegetable   |  8 in One Sugar Coo
  Menu 3 : Almond Roca  |  African Vegetable   |  1,2,3,4 Cake  |  75-Minute Pizza Do  |  1995 1st Place Swe
  Menu 4 : Almond Praline Che  |  Albondigas (Spanis  |  30 Minute Chili  |  Addictive Cream of  |  Acorn Squash Souff
  Menu 5 : Almond Torte (Mozu  |  Alfredo  |  Alicia's Flour Tor  |  Almond Bread  |  1-2-3 Cookies
  Menu 6 : African Vegetable   |  1-Pot Mushroom and  |  Almond Chicken  |  Aggression Cookies  |  Almond Date Shake
  Menu 7 : Almendradas Almond  |  7 Up Cake--Charlot  |  Almond Cake  |  24 Hour Green Sala  |  3 Minute Bbq Sauce

Bilan des trois encodages

Encodage Taille Comportement à l’échelle réelle
Naïf (disjonction) menus × plats × R × C assertions explose à la construction
Théorie des tableaux compact (R-indépendant) unknown — Store symboliques insolubles
One-hot pseudo-booléen menus × plats × R booléens construction + résolu

Nuance (jusqu’au choix de la contrainte). Même au sein du one-hot, le détail compte : exprimer la fenêtre nutritionnelle comme une contrainte pseudo-booléenne native (PbGe / PbLe, somme pondérée de booléens, traitée par le solveur PB) plutôt que comme une somme d’If-then-else routée vers l’arithmétique linéaire générale change la résolution d’un facteur ~150× (mesuré sur le port C# lors d’une itération précédente à ~1 000 recettes : ~0,7 s contre ~110 s — non reproduit dans ce notebook Python ; le bon outil SMT pour une somme pondérée de booléens est le solveur pseudo-booléen, pas le solveur LIA).

Honnêteté de port. Les timing absolus en Python sont plus lents qu’en C# (overhead ctypes par assertion marshalling, ~10-20×) : la « construction quasi-instantanée » du C# (~0,9 s) devient « quelques secondes » en Python. L’ordre relatif des trois encodages (A ≫ B > C en coût de construction ; B unknown vs C sat) est inchangé, ce qui est l’enseignement porté.

3. Partitionner par catégorie : un pool de recettes par créneau

Le one-hot plat ci-dessus peut empiler cinq desserts dans un même menu (il n’impose aucune structure de cours). En partitionnant les recettes en 5 pools (Entrée, Plat principal, Accompagnement, Pain, Dessert) — un pool par créneau — on réduit R par créneau et la variété devient triviale (une recette ne peut apparaître qu’à un seul créneau).

# Encodage C' -- partitionnement par categorie : un pool de recettes par creneau.
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):   # 1er <cat> reconnu gagne ; defaut = plat principal (index 1)
    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)   # chaque recette -> exactement un pool
print("Pools par creneau : " + ", ".join(f"{COURSES[k]}={len(pool[k])}" for k in range(5)))
assert sum(len(pool[k]) for k in range(5)) == R, "les pools doivent partitionner R"
s3 = Solver()
tB3 = time.perf_counter()
# sel3[m][p][j] : le creneau p du menu m prend la j-eme recette DE pool[p]
sel3 = [[[Bool(f"c_{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 / creneau
        s3.add(PbEq([(sel3[m][p][j], 1) for j in range(len(pool[p]))], 1))
for p in range(NPLATS):       # variete : chaque recette <= 1x / semaine (colonne sur les menus)
    for j in range(len(pool[p])):
        s3.add(PbLe([(sel3[m][p][j], 1) for m in range(NMENUS)], 1))
for m in range(NMENUS):       # memes bandes PB ponderees
    for (cc, lo, hi) in restr:
        pairs = [(sel3[m][p][j], int(vint[cc][pool[p][j]])) for p in range(NPLATS) for j in range(len(pool[p]))]
        if hi >= 0: s3.add(PbLe(pairs, hi))
        if lo >= 0: s3.add(PbGe(pairs, lo))
dtB3 = time.perf_counter() - tB3
total3 = NMENUS * sum(len(pool[p]) for p in range(NPLATS))   # = NMENUS x R (partition)
tS3 = time.perf_counter(); res3 = s3.check(); dtS3 = time.perf_counter() - tS3
print(f"course-onehot : {total3} booleens (contre {NMENUS*NPLATS*R} en one-hot plat) -- construction {dtB3:.1f}s, resolution {dtS3:.1f}s -> {res3}")
if res3 == sat:
    mo3 = s3.model()
    for m in range(3):
        names = []
        for p in range(NPLATS):
            for j in range(len(pool[p])):
                if is_true(mo3.eval(sel3[m][p][j], model_completion=True)):
                    names.append(f"{COURSES[p]} : {plats[pool[p][j]][0]}")
        print(f"  Menu {m+1} -> " + "  |  ".join(n[:30] for n in names))
Pools par creneau : Entree=52, Plat principal=370, Accompagnement=47, Pain=65, Dessert=178
course-onehot : 4984 booleens (contre 24920 en one-hot plat) -- construction 0.5s, resolution 0.2s -> sat
  Menu 1 -> Entree : 24-Hour Lettuce Salad  |  Plat principal : Almond Pralin  |  Accompagnement : Almond Rice C  |  Pain : Abadoo's Walnut Bread f  |  Dessert : Almond Cookie Shells
  Menu 2 -> Entree : Abondigas Venezolanas  |  Plat principal : All American   |  Accompagnement : Almonnaise  |  Pain : Almond Poppy Seed Muffi  |  Dessert : Almond-Praline Choco
  Menu 3 -> Entree : African Vegetable Ste  |  Plat principal : Almond Horns  |  Accompagnement : Acorn Squash   |  Pain : Abm Foolproof Cheese an  |  Dessert : Almond Cookies

4. Restriction patient : le menu végétarien

Même encodage que §3 (pools + one-hot PB), avec une contrainte patient en sus : interdire toute recette viande/poisson. En one-hot, « interdire » = nier le booléen (Not(sel[m][p][j])). C’est l’avantage de l’encodage déclaratif : la restriction est une ligne, pas une re-construction.

# Encodage C'' -- restriction patient : menu vegetarien (exclusion categorielle).
from z3 import Not
BANNED_VEG = {"meats", "beef", "poultry", "seafood", "fish", "pork", "chicken", "stews"}
def is_meat(cats):
    return any(c.lower() in BANNED_VEG for c in cats)
n_forbidden = sum(1 for r in range(R) if is_meat(plats[r][2]))
s5 = Solver()
sel5 = [[[Bool(f"v_{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):
        s5.add(PbEq([(sel5[m][p][j], 1) for j in range(len(pool[p]))], 1))
for p in range(NPLATS):
    for j in range(len(pool[p])):
        s5.add(PbLe([(sel5[m][p][j], 1) for m in range(NMENUS)], 1))
for m in range(NMENUS):
    for (cc, lo, hi) in restr:
        pairs = [(sel5[m][p][j], int(vint[cc][pool[p][j]])) for p in range(NPLATS) for j in range(len(pool[p]))]
        if hi >= 0: s5.add(PbLe(pairs, hi))
        if lo >= 0: s5.add(PbGe(pairs, lo))
# LA restriction : interdire toute recette viande/poisson dans chaque creneau ou elle pourrait apparaitre.
for m in range(NMENUS):
    for p in range(NPLATS):
        for j in range(len(pool[p])):
            if is_meat(plats[pool[p][j]][2]):
                s5.add(Not(sel5[m][p][j]))
tS5 = time.perf_counter(); res5 = s5.check(); dtS5 = time.perf_counter() - tS5
print(f"vegetarien : {n_forbidden} recettes viande/poisson interdites -- resolution {dtS5:.1f}s -> {res5}")
if res5 == sat:
    mo5 = s5.model()
    names = []
    for p in range(NPLATS):
        for j in range(len(pool[p])):
            if is_true(mo5.eval(sel5[0][p][j], model_completion=True)):
                names.append(f"{COURSES[p]} : {plats[pool[p][j]][0]}")
    print("  Menu vegetarien 1 -> " + "  |  ".join(n[:30] for n in names))
vegetarien : 46 recettes viande/poisson interdites -- resolution 0.1s -> sat
  Menu vegetarien 1 -> Entree : Ajoblanco De Malaga (  |  Plat principal : Aduki, Orzo a  |  Accompagnement : Almond Rice P  |  Pain : 1-2-3 Meurbeteig Dough   |  Dessert : 14-Carat Cake

5. Exercices

Quatre exercices prolongent l’étude des encodages. Chacun manipule l’encodage C (one-hot pseudo-booléen) ou ses variantes C' / C''. Les variables s, sel, vint, restr, plats, pool restent en portée.

Exercice 1 — Serrer le plafond d’énergie jusqu’à UNSAT

On a calibré hiE sur P80(énergie). Que se passe-t-il si on resserre ce plafond (vers P20, puis P10) ? L’espace des modèles se vide : à partir d’un seuil, le théorème devient insatisfiable. Construisez l’encodage C avec un hiE paramétrique et tracez la frontière SAT → UNSAT.

# Exercice 1 -- serrer hiE jusqu'a UNSAT.
# TODO: boucler sur des hiE decroissants (ex: P80, P50, P30, P20, P10), reconstruire l'encodage C,
#       enregistrer le verdict (sat/unsat) et le temps, tracer la frontiere.
print("Exercice 1 a completer : frontiere SAT -> UNSAT quand hiE diminue.")
Exercice 1 a completer : frontiere SAT -> UNSAT quand hiE diminue.

Exercice 2 — Plancher de glucides

Le constituant glucides (index 2) est chargé mais non contraint dans restr. Ajoutez un plancher PbGe(pairs, GLUCIDES_MIN) sur les glucides par menu (calibre sur P30 des glucides).

# Exercice 2 -- plancher de glucides (constituant index 2, non contraint dans restr).
# TODO: definir GLUCIDES_MIN = NPLATS * int(pq(2, 0.30)), ajouter a l'encodage C la contrainte
#       PbGe([(sel[m][p][r], int(vint[2][r])) for p in range(NPLATS) for r in range(R)], GLUCIDES_MIN).
print("Exercice 2 a completer : plancher de glucides par menu via PbGe.")
Exercice 2 a completer : plancher de glucides par menu via PbGe.

Exercice 3 — Exclusion d’allergène (mot-clé)

Sur le modèle de l’encodage C’’ (végétarien), interdisez les recettes dont un ingrédient contient un mot-clé d’allergène (ex : "gluten", "dairy", "peanut"). En one-hot, cela se ramène à Not(sel[m][p][j]) pour chaque recette touchée.

# Exercice 3 -- exclusion d'allergene (mot-cle sur les cats / titre).
# TODO: definir ALLERGENS = {"gluten", "dairy", "peanut"}, identifier les recettes touchees
#       (plats[r][2] cats ou plats[r][0] titre), ajouter Not(sel[m][p][j]) comme en C''.
print("Exercice 3 a completer : exclusion d'allergenes via Not(sel).")
Exercice 3 a completer : exclusion d'allergenes via Not(sel).

Exercice 4 — Mesurer l’explosion

L’encodage A « explose à la construction » ; le C « passe à l’échelle ». Mesurez-le : balayez R sur {100, 300, R} pour les deux encodages et tracez le coût de construction (naïf) vs résolution (one-hot) en fonction de R.

# Exercice 4 -- mesurer l'explosion (sweep R pour A et C).
# TODO: pour rcap dans (100, 300, R): mesurer build_naive(rcap) [construction] et un build+check
#       one-hot sur rcap premieres recettes ; tracer R vs temps pour les deux encodages.
print("Exercice 4 a completer : sweep R, tracer construction (naif) vs resolution (one-hot).")
Exercice 4 a completer : sweep R, tracer construction (naif) vs resolution (one-hot).

Synthèse — l’encodage décide de la tractabilité

Le même théorème (7 menus × 5 plats, variété, fenêtre nutritionnelle), sur le même corpus réel, donne trois comportements radicalement différents selon l’encodage SMT :

  • l’index + disjonction naïf explose dès la construction (O(menus × plats × R × C)) ;
  • la théorie des tableaux, si compacte à écrire, reste unknown ;
  • le one-hot pseudo-booléen se construit et se résout, parce que la somme pondérée de booléens est traitée par le solveur pseudo-booléen natif de Z3.

Leçon : à l’échelle, ce n’est pas la puissance brute du solveur qui décide — c’est le choix d’encodage. Les recettes sont des contraintes enablantes ; l’encodage décide si l’espace qu’elles ouvrent est explorable. C’est la clôture du bloc meal-planner : de la modélisation jouet (16) à la donnée réelle (16b), au capstone patient (16c), jusqu’à la tractabilité à l’échelle (ce notebook).

Honnêteté de port. Ce notebook Python reproduit les verdicts qualitatifs du port C# 09 (A explose, B unknown, C sat) sur le sous-ensemble de corpus produit par 16b. Les timing absolus diffèrent (overhead ctypes Python ~10-20×), l’ordre relatif non. Le pseudo-booléen (PbEq / PbLe / PbGe) fait ici son entrée dans la jambe Python-large.

Retour au sommet