[jsboige]

Grain: MED/readme -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/notebook-python #24361

Ce que fait cette PR

Elle confirme les mappings « carnet <-> livre » que les deux README de la famille SMT laissaient a a_confirmer :

• l'index chapitre de Z3-API/README.md : lignes Z3-15 et Z3-16 ;
• le tableau de mapping des carnets Z3-Linq2Z3, dans les deux README (section + folio desormais en colonne) ;
• l'avertissement « defaut biblio » du README Z3-Linq2Z3, leve : il etait propre au siege qui l'avait constate.

Elle precise en outre ce que le mapping ne dit pas : il relie chaque carnet a la section de l'ouvrage qui traite le meme sujet, il n'affirme pas que le carnet reprend l'instance de l'ouvrage.

Mesures (firsthand)

• Copie archivee lue : G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2023 - SAT_SMT_by_example.pdf, instrument PyMuPDF 1.27.2.3.
• Folio = index PDF − 1 : le folio imprime est la premiere ligne de texte de la page (en pied de page pour les ouvertures de chapitre, ou la page s'ouvre sur une table de matieres). Releve sur une vingtaine de reperes : index 12 -> folio 11 (« Chapter 1 / Introduction »), index 15 -> 14 (« Chapter 2 / Basics »), index 206 -> 205 (« 8.1 Sudoku »), index 213 -> 212 (« 8.1.2 »), index 233 -> 232 (« 8.2 Zebra puzzle »), index 277 -> 276 (« 8.10 Alphametics »), index 347 -> 346 (« 12.1 A simple Latin square »), index 362 -> 361 (« 12.4 »), index 398 -> 397 (« 14.5 »), index 406 -> 405 (« 14.8 »), index 634 -> 633 (« 22.8 »), index 91 -> 90 (« 3.13.2 »), index 93 -> 92 (« 3.13.3 »), index 114 -> 113 (« 4.5 »), index 133 -> 132 (« 5.1 »), index 333 -> 332 (« Chapter 10 / Knapsack problems »), index 384 -> 383 (« Chapter 14 / MaxSAT/MaxSMT »).
• Numeros de section releves sur la page, jamais dans le sommaire imprime : 8.1.2 Simple sudoku in SMT using functions and array, 12.1 A simple Latin square, 12.4 Magic/Latin square of Knut Vik design, 14.5 Assignment problem, 14.8 Packing students into a dorm, 22.8 Job Shop Scheduling/Problem, 3.13.2 Unsat core, 4.5 Simplifying long and messy expressions using Z3, 5.1 Integer overflow, 8.10 Alphametics. Le sommaire imprime et le corps ne portent pas la meme pagination (mesure du 23/10/2026 sur cette meme copie).
• Le PDF s'ouvre normalement depuis ce poste : fitz.open() rend le document entier. Le defaut constate le 05/10/2026 ne vaut que pour le siege qui l'a constate.

Deux points de fond

• Z3-16 (Meal-Planner) : le livre lui-meme formule le §22.8 en termes de restaurant (« each dish is a job », « each stage/task require specific kitchen appliance and/or chef ») : l'ancrage du plan hebdomadaire est dans l'ouvrage, pas une analogie forcee. Le §14.5 (probleme d'affectation, Optimize + Distinct) couvre la partie « choix des plats par categorie ».
• Z3-15 (tableaux imbriques 2D) : l'ouvrage n'a pas de section « nested arrays » ; l'ancrage reel est Ch. 12 Latin squares (§12.1, §12.4 et son §12.4.1 « Using Z3Py ») et §8.1.2 (Sudoku encode par tableaux). Le mapping le dit ainsi, sans section inventee.

Ce que le mapping ne dit pas

La confrontation instance par instance des trois carnets dont l'exemple est le plus directement l'image du livre :

• 13_Cryptarithmetic_SMT reprend bien l'alphametique du livre (§8.10, p. 276 — SEND + MORE = MONEY, memes lettres S E N D M O R Y et meme equation positionnelle).
• 02_Sudoku_Theorem_vs_Array en reprend le cadre d'encodage (§8.1.2, p. 212), pas la grille : celle du livre (§8.1, p. 205) est le « world's hardest sudoku » a 23 indices, et la grille du carnet est celle de Norvig a 30 indices, absente de l'ouvrage.
• 18_Einsteins_Riddle en reprend le cadre d'encodage (§8.2, p. 232), pas le puzzle : l'instance du livre a pour reponse que le Japonais possede le zebre, le carnet resout une variante renommee dont la reponse est « l'Allemand qui possede le poisson ».

La note « Portee du mapping » ajoute cette precision aux deux tableaux.

Portee

• Markdown pur, deux fichiers de README. Aucune cellule de carnet touchee -> pas de re-execution due (C.2 sans objet).
• python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD : rc=0.
• Controle REST sur les fichiers de toutes les PRs ouvertes : aucune ne touche ces deux README -> pas de collision au merge.
• Les credits explicites dans les cellules d'introduction (travail 3 de Referencement SMT/Solvers (2/4) : Yurichev SAT/SMT by Example comme ouvrage-ancrage des series Z3-API et Z3-Linq2Z3 #19278) ne font pas partie de cette PR : ils touchent des cellules de carnet et font l'objet d'une tranche separee.

Fichiers

• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md
• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/README.md

See #19278

🤖 Generated with Claude Code

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre readme dans la famille META (docs/guard/ledger/readme/test) + diff de 61 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.