diff --git a/MyIA.AI.Notebooks/Sudoku/Sudoku-06-AIMA-CSP-Python.ipynb b/MyIA.AI.Notebooks/Sudoku/Sudoku-06-AIMA-CSP-Python.ipynb index a3caba64a9..4fab5fd758 100644 --- a/MyIA.AI.Notebooks/Sudoku/Sudoku-06-AIMA-CSP-Python.ipynb +++ b/MyIA.AI.Notebooks/Sudoku/Sudoku-06-AIMA-CSP-Python.ipynb @@ -310,6 +310,19 @@ "print(test_grid)" ] }, + { + "cell_type": "markdown", + "id": "52f2096e", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du corpus : 5 puzzles, la grille témoin en tête\n", + "\n", + "La sortie confirme **5 puzzles chargés**, et la grille de test affichée est la **grille témoin de la série** — comptez les indices : 9,2,5,4,3 en ligne 1, puis 1,6,3,2,5, 5,8,4,7,6... soit **45 indices** au total, exactement le même puzzle que Sudoku-04 (recuit), Sudoku-06-C# (MAC) et Sudoku-11 (Choco). Cette uniformité est la colonne vertébrale des comparaisons de la série : quand la section 10 mesurera ici MAC à **62,4 ms / 81 assignations / 0 backtrack**, la comparaison avec les 56 ms du jumeau C# et les 473 ms de Choco sous IKVM portera sur des entrées identiques. Les 51 puzzles faciles du dossier commun nourriront le benchmark de la section suivante." + ] + }, { "cell_type": "markdown", "id": "708f3cdf", @@ -437,6 +450,19 @@ "print(\"Exercice a completer\")" ] }, + { + "cell_type": "markdown", + "id": "10f2f163", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture honnête du domaine affiché : le placeholder de l'exercice\n", + "\n", + "Lisez la sortie avec attention : le domaine affiché `{1, 2, ..., 9}` pour la cellule (0,1) est le **placeholder du stub** — la fonction rend `set(range(1, 10))` tant que l'exercice n'est pas complété, et la ligne « Exercice a completer » le signale (citation exacte de la sortie). Le **vrai** calcul exclurait les valeurs déjà posées dans le voisinage de (0,1) : la ligne 0 contient déjà 9, 2, 5, 4, 3, la colonne 1 contient 1, 5, 2, 9, 4, 8, et le bloc supérieur gauche d'autres valeurs encore — le domaine réel est donc nettement plus petit que 9 valeurs. C'est précisément l'objet de travail du CSP : le **domaine** d'une variable (ici, l'ensemble des valeurs légales d'une cellule) est la donnée que chaque heuristique de ce notebook interrogera — MRV trie par taille de domaine, le forward checking le rogne, AC-3 le vide jusqu'au point fixe." + ] + }, { "cell_type": "markdown", "id": "6c9459a6", @@ -741,7 +767,9 @@ "Heuristique de **sélection de variable** : choisir la variable avec le plus petit domaine restant.\n", "\n", "### LCV (Least Constraining Value)\n", - "Heuristique d'**ordonnancement des valeurs** : essayer d'abord la valeur qui élimine le moins de possibilites chez les voisins." + "Heuristique d'**ordonnancement des valeurs** : essayer d'abord la valeur qui élimine le moins de possibilites chez les voisins.\n", + "\n", + "Dans cette implémentation, les deux heuristiques vivent dans la classe `CSPHeuristics` et sont **orthogonales par construction** : MRV choisit *la prochaine variable à assigner* (celle au domaine le plus petit — révéler tôt les conflits, quand annuler une branche coûte peu), LCV ordonne *les valeurs à essayer* pour la variable choisie (commencer par celle qui contraint le moins les voisines — garder des options ouvertes). Aucune des deux ne réduit l'arbre en soi : elles réordonnent l'exploration. Le benchmark de la section 10 chiffre la hiérarchie complète : le backtracking seul explose à 2 889 322 assignations, MRV+LCV le ramène à 255, et dès lors que la propagation (FC, MAC) entre en jeu, les 81 assignations exactes suffisent." ] }, { @@ -1135,7 +1163,9 @@ "source": [ "## 8. Arc Consistency (AC-3)\n", "\n", - "L'algorithme **AC-3** assure que pour chaque arc (Xi, Xj), toute valeur de Xi a un support dans Xj." + "L'algorithme **AC-3** assure que pour chaque arc (Xi, Xj), toute valeur de Xi a un support dans Xj.\n", + "\n", + "Le moteur d'AC-3 tient en trois pièces : une **file d'arcs** (initialisée avec tous les couples (Xi, Xj) voisins), l'opération **revise** (pour chaque valeur de Di, existerait-il une valeur support dans Dj ? sinon, retirer la valeur de Di), et la détection du **point fixe** (si Di a changé, remettre en file tous les arcs pointant vers Xi — l'élimination se propage). Le pré-traitement complet vide la file une fois pour toutes ; MAC, en section 9, repeuplera une mini-file à chaque assignation. C'est ce même mécanisme que le notebook Sudoku-14-BDD compile sous forme d'automate, et que la propagation de Norvig (Sudoku-07) réalise par paires de cellules." ] }, { @@ -1508,6 +1538,19 @@ " print(\"Pas de solution trouvee\")" ] }, + { + "cell_type": "markdown", + "id": "f3c1b196", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du résultat MAC : 62,4 ms, 81 assignations, 0 backtrack\n", + "\n", + "Le triplet mesuré vaut une lecture ligne à ligne. **81 assignations** : exactement une par cellule — jamais le solveur n'a essayé une valeur qu'il a dû retirer. **0 backtrack** : aucun retour en arrière ; l'inférence (arc-consistance maintenue à chaque assignation) a éliminé les conflits avant même qu'ils surviennent. **62,4 ms** : à comparer au jumeau C# du même notebook, qui résout **la même grille témoin** en 56 ms avec le même profil 81/0 — deux langages, deux implémentations, un même verdict structurel : sur une grille à 45 indices bien contrainte, MAC résout par pure propagation, la recherche ne fait qu'encaisser. La ligne finale « Solution valide : True » referme la boucle : la solution est re-vérifiée indépendamment de l'algorithme qui l'a produite." + ] + }, { "cell_type": "markdown", "id": "142aefae", @@ -2230,6 +2273,19 @@ "solve_graph_coloring(n=15, edge_prob=0.4, num_colors=4)" ] }, + { + "cell_type": "markdown", + "id": "88dc6dd3", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture honnête de la sortie : des en-têtes sans lignes\n", + "\n", + "La sortie affiche les **en-têtes des deux expérimentations** (graphe peu dense / graphe dense) mais **aucune ligne de résultat** — et c'est l'état attendu : la fonction `generate_random_graph` est le TODO de l'exercice (le `pass` du stub ne génère rien), donc le benchmark tourne sur des structures vides. Ce que l'expérience montrera une fois complétée : sur un graphe peu dense à 3 couleurs, Forward Checking et MAC convergent souvent en des temps comparables (peu de conflits à propager) ; sur le graphe dense à 4 couleurs, l'écart se creuse — MAC maintient une consistance plus forte, paie plus cher par nœud mais coupe des sous-arbres entiers que FC laissera explorer. Le squelette est prêt ; les chiffres attendent le générateur." + ] + }, { "cell_type": "markdown", "id": "888465da", diff --git a/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-Python.ipynb b/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-Python.ipynb index 46906eee58..b2e8e88fd8 100644 --- a/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-Python.ipynb +++ b/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-Python.ipynb @@ -323,6 +323,19 @@ "print(f\"Puzzles chargés: {len(easy_puzzles)} faciles, {len(hard_puzzles)} difficiles\")" ] }, + { + "cell_type": "markdown", + "id": "c6a48652", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du corpus : trois fichiers, 10 faciles + 11 difficiles\n", + "\n", + "La sortie énumère le contenu du dossier commun de la série — **Easy51, hardest, top95** — puis la classe de chargement en tire **10 faciles et 11 difficiles**. Ce sont les mêmes corpus que le benchmark du notebook Sudoku-07-Norvig-Python (20 faciles à 3,30 ms, 11 difficiles à 4,45 ms par propagation) : les encodages diffèrent, les terrains de jeu non. Le puzzle difficile affiché en tête de test (8 5 . | . . 2 | 4 . . ...) est l'exemplaire sur lequel le solveur `Int` de la section suivante sera mesuré à 340,86 ms." + ] + }, { "cell_type": "markdown", "id": "e8a142b7e7420aee", @@ -1103,6 +1116,19 @@ " print(\"Pas de solution\")" ] }, + { + "cell_type": "markdown", + "id": "b26f5d4b", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du solveur diagonal : deux contraintes de plus, rien d'autre\n", + "\n", + "Comparez les deux grilles affichées : la grille d'entrée est **clairsemée** (une vingtaine d'indices), et la solution est trouvée avec les **deux diagonales vérifiées toutes-distinctes** — principale `[1, 4, 3, 7, 2, 6, 5, 8, 9]`, secondaire `[3, 7, 1, 9, 2, 8, 6, 5, 4]`, toutes deux `True`. C'est la variante **Sudoku-X**, et la leçon est dans le code : passer du Sudoku standard au Sudoku-X a coûté exactement **deux lignes** — deux `Distinct` supplémentaires sur les diagonales `cells[i][i]` et `cells[i][8-i]`. Aucune heuristique à ré-accorder, aucun solveur à ré-écrire : c'est l'**additivité déclarative** du SMT, la propriété qui le distingue d'un solveur dédié (le backtracking de Sudoku-13 exige de toucher la fonction de validité pour la même variante)." + ] + }, { "cell_type": "markdown", "id": "96e575c4", @@ -1223,6 +1249,19 @@ " print(\"Pas de solution trouvee\")" ] }, + { + "cell_type": "markdown", + "id": "40d111ea", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture honnête : « Pas de solution trouvee » = le stub rendu proprement\n", + "\n", + "La ligne unique de la sortie est la sortie **conventionnelle d'un exercice incomplet** (règle C.1) : la fonction rend `None` proprement au lieu de lever une erreur, et l'énoncé imprime le diagnostic. Le problème attendu — colorier la carte de France à 10 régions avec 4 couleurs via `Int(color_i)` et `color_i != color_j` par arête — est exactement la modélisation du Sudoku transposée : des variables à domaine fini, des contraintes de différence binaire. Le théorème des quatre couleurs garantit qu'une solution existe pour toute carte planaire ; l'exercice, lui, attend sa modélisation." + ] + }, { "cell_type": "markdown", "id": "z3-opt-intro-md", @@ -1334,6 +1373,19 @@ "" ] }, + { + "cell_type": "markdown", + "id": "bf8e8f4d", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du Optimize : sat, reward 178, et la preuve d'optimalité\n", + "\n", + "Quatre lignes, quatre enseignements. **`Statut : sat`** — le contexte `Optimize` de Z3 est d'abord un solveur de satisfaction. **`Reward maximal : 178`** — ce n'est pas un reward *trouvé*, c'est un reward **prouvé maximal** : `Optimize` boucle en résolvant puis en ajoutant la contrainte « objectif > meilleur courant » jusqu'à l'insatisfiabilité — la différence entre « une bonne solution » et « la meilleure » est exactement la différence entre `Solver` et `Optimize`. **Le carré latin 5x5 affiché** — chaque ligne et chaque colonne est une permutation de 1-5, vérifié par la ligne « Carre latin valide : True » (citation de la sortie). La docstring de la cellule le dit : ce démo est le miroir SMT de l'exemple CP-SAT du notebook Sudoku-10-ORTools — deux moteurs, une même capacité signature, la maximisation sous contraintes." + ] + }, { "cell_type": "markdown", "id": "z3-opt-exercise-md", diff --git a/MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb b/MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb index e0734d1d9a..09fe83ddf4 100644 --- a/MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb +++ b/MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb @@ -249,6 +249,19 @@ " print(f\" {s!r:14s} attendu={str(attendu):5s} obtenu={str(obtenu):5s} {statut}\")\n" ] }, + { + "cell_type": "markdown", + "id": "99ec087a", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture de la table : 6/6 OK, et pourquoi les lookaheads suffisent\n", + "\n", + "Les six tests passent, et l'identité qui rend le motif correct est discrète : **pour une chaîne de longueur exactement 9 sur l'alphabet [1-9], « contenir chaque chiffre de 1 à 9 » est équivalent à « tous distincts »** — s'il manque un chiffre, par cardinalité un autre est dédoublé. C'est cette bijection qui permet d'exprimer la contrainte de ligne comme la conjonction de **neuf lookaheads zéro-largeur** `(?=.*1)`...`(?=.*9)` : chaque lookahead affirme une présence sans consommer de caractères, puis `[1-9]{9}$` fixe la longueur et l'alphabet. Les deux faux négatifs attendus (`12345678` trop court, `1234567890` trop long) sont rejetés par la queue ancrée, les deux lignes avec doublon par les lookaheads absents — la table de test couvre chaque clause du motif." + ] + }, { "cell_type": "markdown", "id": "f54df36c", @@ -417,6 +430,19 @@ "print(f\"Les 9 lignes passent la reconnaissance regex : {ok}\")\n" ] }, + { + "cell_type": "markdown", + "id": "abf3b79e", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture de la résolution : sat en 101,8 ms, puis la boucle bouclée\n", + "\n", + "Le témoin passe : **sat en 101,8 ms**, et la grille solution s'affiche. Mais la ligne décisive est la dernière : « **Les 9 lignes passent la reconnaissance regex : True** » — chaque ligne de la solution produite par le solveur est re-vérifiée par le motif `LIGNE_VALIDE` du barreau 2. Le reconnaisseur du barreau précédent devient le **contrôle de validité indépendant** du solveur de ce barreau : deux outils construits séparément, un même verdict. La modélisation elle-même est l'idiome Z3 canonique — 81 `Int`, bornes 1-9, un `Distinct` par ligne, colonne et bloc — exactement celle du notebook Sudoku-12 : les barreaux de l'échelle partagent le socle." + ] + }, { "cell_type": "markdown", "id": "7ff0f87c", @@ -550,6 +576,19 @@ "print(\"L'automate Z3 reconnait ce que le solveur produit (boucle bouclee).\")\n" ] }, + { + "cell_type": "markdown", + "id": "a4461243", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture de la théorie des chaînes : sat, unsat, unsat — le motif devient contrainte\n", + "\n", + "Les trois verdicts se lisent comme une table de vérité du motif du barreau 2 transposé en logique. `'123456789'` est **sat** : la chaîne appartient au langage `InRe(ligne, neuf_digits)` (longueur 9 sur [1-9]) ET satisfait les neuf `Contains`. `'123456788'` est **unsat** : le 9 absent viole un `Contains`. `'12345678'` est **unsat** : la longueur 8 viole `InRe`. La différence avec le barreau 2 est le **sens de la question** : là le regex *teste* une chaîne donnée, ici le solveur *raisonne* sur l'espace des chaînes — `Range` et `Concat` construisent un automate comme terme logique, et le solveur peut composer cette contrainte avec n'importe quelle autre (l'intersecter, la nier, l'exister). La ligne finale de la sortie — « l'automate Z3 reconnait ce que le solveur produit » — boucle le circuit : reconnaissance et résolution échangent leurs rôles." + ] + }, { "cell_type": "markdown", "id": "e5a48069", @@ -795,6 +834,19 @@ "print(f\"Les deux solveurs donnent la meme grille : {identique}\")\n" ] }, + { + "cell_type": "markdown", + "id": "7be2635e", + "metadata": { + "papermill": {}, + "tags": [] + }, + "source": [ + "### Lecture du contre-point : 27,2 ms contre 101,8, et la même grille\n", + "\n", + "Le backtracking récursif naïf — premier appel au tableau, pas d'heuristique, la pile d'appels pour seul contexte — résout **en 27,2 ms** ce que Z3 résout en 101,8 : presque **4x plus vite**, et la sortie le confirme, **sur la même solution** (deux algorithmes indépendants convergent = contrôle de validité gratuit). Faut-il en conclure que l'écriture main est « meilleure » ? Sur cette instance figée, oui — le code spécialisé épouse le substrat (tableaux indexés, aucun parsing, aucune construction de modèle) là où Z3 paie sa générosité. Mais changez l'énoncé — ajoutez des diagonales, une contrainte de somme, une optimisation — et le code spécialisé exigera une ré-écriture quand Z3 exigera **une ligne** (cf. le solveur diagonal de Sudoku-12). C'est le critère Prong B en acte : le SOTA se juge au coût de changement du problème, pas au chronomètre d'une instance figée." + ] + }, { "cell_type": "markdown", "id": "253accad", @@ -811,7 +863,9 @@ "source": [ "## 8. Reconnaissance vs résolution — le tableau comparatif\n", "\n", - "Trois outils, trois rôles distincts. La reconnaissance (regex) certifie en temps linéaire ce qu'elle ne sait pas produire. La résolution (Z3) produit. La récursion (`regex` `(?&rec)`) franchit la frontière du régulier — le seul outil des trois qui puisse exprimer un Sudoku-en-un-regex." + "Trois outils, trois rôles distincts. La reconnaissance (regex) certifie en temps linéaire ce qu'elle ne sait pas produire. La résolution (Z3) produit. La récursion (`regex` `(?&rec)`) franchit la frontière du régulier — le seul outil des trois qui puisse exprimer un Sudoku-en-un-regex.\n", + "\n", + "Le tableau qui s'affiche ci-dessous est la synthèse de l'échelle entière du notebook : **reconnaître** (le motif lookahead, la théorie des chaînes — dire d'une chaîne donnée si elle est valide), **résoudre** (Z3 sur 81 entiers — produire une solution), **optimiser** (le `Optimize` de Sudoku-12 — produire la meilleure). Trois rôles que le folklore PCRE du barreau 1 précisément confond, et que la suite du notebook sépare proprement." ] }, { diff --git a/scripts/notebook_tools/twin_pairs.d/sudoku-06-aima-csp/0008-2026-09-18-myia-po-2026-CoursIA.yaml b/scripts/notebook_tools/twin_pairs.d/sudoku-06-aima-csp/0008-2026-09-18-myia-po-2026-CoursIA.yaml index e4c838e3a0..fe9c5184ce 100644 --- a/scripts/notebook_tools/twin_pairs.d/sudoku-06-aima-csp/0008-2026-09-18-myia-po-2026-CoursIA.yaml +++ b/scripts/notebook_tools/twin_pairs.d/sudoku-06-aima-csp/0008-2026-09-18-myia-po-2026-CoursIA.yaml @@ -1,6 +1,6 @@ date: '2026-09-18' by: myia-po-2026:CoursIA -python_sha: a3caba64a95ad07a58e2496c0db644df26ee0b07 +python_sha: 4fab5fd758a074e118fa77e8ed4030e33e8c9ede csharp_sha: 53b3b16e133d87cd149bc732a31446754d392724 -content_python_sha: a70f935b71b20eb5f9f2456a05581c4cce0ff1888f37c7416b6e756acb825b07 +content_python_sha: f98692081df05208836a9d6a8ae364dde8cf29fafa6795998ca7dacff960a1ec content_csharp_sha: 6e24824e876c8cef02b214874178002c1aa6ce8f36426b62a3e8d16c14a2215d diff --git a/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0009-2026-09-18-myia-po-2026-CoursIA.yaml b/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0009-2026-09-18-myia-po-2026-CoursIA.yaml new file mode 100644 index 0000000000..3abbc5a5b3 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0009-2026-09-18-myia-po-2026-CoursIA.yaml @@ -0,0 +1,6 @@ +date: '2026-09-18' +by: myia-po-2026:CoursIA +python_sha: b2e8e88fd88b283f79031f084309e427e4327d66 +csharp_sha: 556dc0e05867c09834cbae74a1892ca780bceac8 +content_python_sha: e376e098f67c13a3e290647c58c2bc0af8b41243f33f64488fe095a8de48dc9b +content_csharp_sha: b9149a63924e4e645534c78fa4a195ee51bb1569d278074a33a0ddbd5fcc755f diff --git a/scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata/0017-2026-09-18-myia-po-2026-CoursIA.yaml b/scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata/0017-2026-09-18-myia-po-2026-CoursIA.yaml new file mode 100644 index 0000000000..9a07767bf1 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata/0017-2026-09-18-myia-po-2026-CoursIA.yaml @@ -0,0 +1,6 @@ +date: '2026-09-18' +by: myia-po-2026:CoursIA +python_sha: 09fe83ddf4286a54a3810cbc7d2ce56e3eb6838a +csharp_sha: 5c3fed39821b242bb269c1d579c91d2241ef5d33 +content_python_sha: 6da01a1ab91f64d21096a9927aa2e315f9df297ba41b99d20408971c571eed94 +content_csharp_sha: 68b076ef17f9e9a8af10d7c95168edb2a28fba54836af7c8358ad94bf3f07947