Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -973,12 +973,12 @@
"## 9. L'automate symbolique en Python — diagrammes de decision binaires (BDD)\n",
"\n",
"Le titre de ce notebook parle d'**automates symboliques**, mais jusqu'ici la\n",
"« symbolique » reste abstraite : Z3 manipule des entiers et des chaines sans\n",
"« symbolique » reste abstraite : Z3 manipule des entiers et des chaînes sans\n",
"montrer la structure d'automate. Le twin C# (Annexe S10) construit un tel\n",
"automate via `Microsoft.Z3` ; voici l'equivalent Python avec la librairie `dd`,\n",
"automate via `Microsoft.Z3` ; voici l'équivalent Python avec la librairie `dd`,\n",
"qui implemente les **diagrammes de decision binaires** (BDD).\n",
"\n",
"Un BDD est un **automate deterministe acyclique** : chaque variable booleenne\n",
"Un BDD est un **automate déterministe acyclique** : chaque variable booleenne\n",
"est un niveau de branchement (vrai/faux), et les feuilles sont 0 (rejet) ou\n",
"1 (acceptation). C'est exactement la structure d'un automate compile une fois\n",
"pour toutes, puis parcourue en lecture seule. La vertu : un BDD **factorise**\n",
Expand Down Expand Up @@ -1093,15 +1093,15 @@
"**Le plafond honnete.** Cet exemple tient en 6 variables. La contrainte\n",
"« tous-distincts » est en fait connue comme **dure pour les BDD** : sur la\n",
"vraie ligne Sudoku (9 cellules, 4 bits chacune = 36 variables), le BDD\n",
"explose a plusieurs millions de noeuds. C'est precisement pour cela que Z3\n",
"n'utilise PAS un BDD brut pour le Sudoku : il dispose d'une **theorie\n",
"explose a plusieurs millions de noeuds. C'est précisément pour cela que Z3\n",
"n'utilise PAS un BDD brut pour le Sudoku : il dispose d'une **théorie\n",
"specialisee** des entiers (Distinct, arithmetique) bien plus compacte qu'une\n",
"explosion booleenne. Le BDD reste l'outil de choix pour la logique purement\n",
"booleenne (circuits, model-checking) ; le solveur SMT regne sur l'arithmetique.\n",
"\n",
"> **Pont avec le twin C#.** L'Annexe S10 construit le meme genre d'automate\n",
"> symbolique via `Microsoft.Z3` ; ici `dd` (PyPI) joue ce role cote Python.\n",
"> Les deux instancient la meme idee : compiler une contrainte en un graphe\n",
"> **Pont avec le twin C#.** L'Annexe S10 construit le même genre d'automate\n",
"> symbolique via `Microsoft.Z3` ; ici `dd` (PyPI) joue ce rôle cote Python.\n",
"> Les deux instancient la même idee : compiler une contrainte en un graphe\n",
"> de decision parcourable en temps lineaire.\n"
]
},
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Sudoku/Sudoku-14-BDD-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -710,7 +710,7 @@
"### Lecture des tests : des tautologies réduites à un seul nœud\n",
"\n",
"Trois résultats, trois leçons. **Test 1** : `x AND NOT x` s'évalue en `False` avec **1 nœud** — l'application de l'opérateur détecte la contradiction au niveau des terminaux et renvoie directement la feuille : à aucun moment un arbre n'est développé, c'est du calcul **symbolique**, pas de l'énumération. **Test 2** : `x OR NOT x`, symétriquement, donne `True` sur 1 nœud. **Test 3** (distributivité) : les deux expressions de la loi distributive occupent **7 nœuds chacune** et sont vérifiées équivalentes — d'abord sur une assignation témoin, puis **sur les 8 assignations** exhaustives des trois variables. Notez la limite de cette vérification : l'équivalence par évaluation est exponentielle en le nombre de variables — praticable à 3 variables, pas à 81 cellules de Sudoku ; l'équivalence **structurelle** (DAG identiques après canonisation) est ce qui la remplacera à grande échelle.\n",
" L'equivalence structurelle est aussi ce qui rendra le comptage de noeuds significatif : deux formules equivalentes, deux DAG de meme taille canonique."
" L'equivalence structurelle est aussi ce qui rendra le comptage de noeuds significatif : deux formules equivalentes, deux DAG de même taille canonique."
]
},
{
Expand Down
46 changes: 23 additions & 23 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-15-Infer-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
"\n",
"## Introduction : Programmation Probabiliste et Sudoku\n",
"\n",
"Ce notebook implemente l'equivalent Python du **RobustProbabilisticSolver** du notebook C# Infer.NET. Les deux approches utilisent des distributions **Dirichlet** pour modeliser les probabilites des cellules.\n",
"Ce notebook implemente l'équivalent Python du **RobustProbabilisticSolver** du notebook C# Infer.NET. Les deux approches utilisent des distributions **Dirichlet** pour modeliser les probabilites des cellules.\n",
"\n",
"### Comparaison des approches\n",
"\n",
Expand Down Expand Up @@ -142,15 +142,15 @@
"source": [
"### Interpretation : Environnement NumPyro/JAX\n",
"\n",
"**Résultats obtenus** : L'environnement est correctement configure : la cellule ci-dessus imprime les versions de JAX et NumPyro (execution sur CPU).\n",
"**Résultats obtenus** : L'environnement est correctement configure : la cellule ci-dessus imprime les versions de JAX et NumPyro (exécution sur CPU).\n",
"\n",
"| Composant | Rôle |\n",
"|-----------|------|\n",
"| JAX | Calcul differenciable et compilation JIT |\n",
"| NumPyro | Programmation probabiliste sur JAX |\n",
"| Device (CPU) | Exécution sur CPU (pas de GPU requis) |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **JAX comme backend** : JAX fournit la differenciation automatique et la compilation JIT necessaires a NumPyro\n",
"2. **Exécution CPU** : Ce notebook fonctionne sur CPU, pas besoin de GPU (contrairement au Deep Learning)\n",
"3. **Version recente** : NumPyro (version stable recente) offre un SVI bien optimise\n",
Expand Down Expand Up @@ -336,7 +336,7 @@
"| Cellules initiales | ~25-35 | Puzzles Easy ont ~30% de cases pre-remplies |\n",
"| Encodage | Chiffres 0-9 | 0 = vide, 1-9 = valeurs connues |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **Stratégie de chargement robuste** : Le code essaie deux chemins possibles (relatif et absolu)\n",
"2. **Fallback** : Si aucun fichier n'est trouve, un puzzle de test par defaut est utilise\n",
"3. **Format compact** : 81 caractères suffisent pour representer un grille 9x9\n",
Expand All @@ -359,9 +359,9 @@
"tags": []
},
"source": [
"## 3. Modèle NumPyro avec Dirichlet (Equivalent RobustProbabilisticSolver)\n",
"## 3. Modèle NumPyro avec Dirichlet (Équivalent RobustProbabilisticSolver)\n",
"\n",
"Ce modèle est l'equivalent Python du `RobustSudokuModel` du notebook C# Infer.NET. Il utilise :\n",
"Ce modèle est l'équivalent Python du `RobustSudokuModel` du notebook C# Infer.NET. Il utilise :\n",
"\n",
"1. **Distributions Dirichlet** pour les probabilites des cellules (comme Infer.NET)\n",
"2. **Contraintes douces** via `numpyro.factor` (au lieu de `ConstrainFalse`)\n",
Expand Down Expand Up @@ -490,9 +490,9 @@
"tags": []
},
"source": [
"## 4. Solveur Probabiliste Pur (Equivalent RobustProbabilisticSolver)\n",
"## 4. Solveur Probabiliste Pur (Équivalent RobustProbabilisticSolver)\n",
"\n",
"Ce solveur est l'equivalent Python direct du `RobustProbabilisticSolver` C# :\n",
"Ce solveur est l'équivalent Python direct du `RobustProbabilisticSolver` C# :\n",
"- Une seule passe d'inference\n",
"- Recupere le mode de chaque distribution Dirichlet\n",
"- Pas de propagation déterministe"
Expand Down Expand Up @@ -711,15 +711,15 @@
"\n",
"**Résultats obtenus** : Une seule passe d'inference SVI (300 itérations) suffit pour resoudre ce puzzle Easy avec succes.\n",
"\n",
"| Metrique | Valeur | Analyse |\n",
"| Métrique | Valeur | Analyse |\n",
"|----------|--------|---------|\n",
"| Itérations SVI | 300 | Equivalent a ~50 EP itérations Infer.NET |\n",
"| Itérations SVI | 300 | Équivalent a ~50 EP itérations Infer.NET |\n",
"| Temps inference | ~6 s | ~180x plus lent que C# (~34ms) |\n",
"| Convergence | True | Solution valide obtenue |\n",
"| Erreurs | 0 | Toutes les contraintes respectees |\n",
"| Cellules initiales | 45 | 36 cellules a determiner |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **Mode des distributions** : Le solveur selectionne la valeur la plus probable de chaque distribution Dirichlet (argmax)\n",
"2. **Contraintes douces** : Les penalites `numpyro.factor` encouragent la cohérence sans garantir les contraintes Sudoku\n",
"3. **Performance acceptable** : ~6 secondes pour un puzzle Easy est raisonnable pour un prototype pedagogique\n",
Expand Down Expand Up @@ -750,7 +750,7 @@
"1. `entropy(probs)` : calculer l'entropie d'une distribution (mesure d'incertitude)\n",
"2. `analyze_confidence(grid, probs)` : identifier les cellules les plus certaines et les plus incertaines\n",
"\n",
"**Concepts cles** :\n",
"**Concepts clés** :\n",
"- **Entropie** : quantifie l'incertitude d'une distribution. Valeur faible = modèle certain, valeur elevee = modèle hesitant\n",
"- **Confiance** : probabilite maximale de la distribution pour une cellule\n",
"- **Distribution uniforme** : 9 valeurs equiprobables, entropie = ln(9) ~ 2.20 nats\n",
Expand Down Expand Up @@ -995,9 +995,9 @@
"tags": []
},
"source": [
"## 5. Solveur Iteratif (Equivalent IterativeSudokuModel)\n",
"## 5. Solveur Iteratif (Équivalent IterativeSudokuModel)\n",
"\n",
"Ce solveur est l'equivalent Python du `IterativeSudokuModel` C# qui fixe iterativement les cellules les plus certaines."
"Ce solveur est l'équivalent Python du `IterativeSudokuModel` C# qui fixe iterativement les cellules les plus certaines."
]
},
{
Expand Down Expand Up @@ -1213,7 +1213,7 @@
"\n",
"**Résultats obtenus** : Le solveur iteratif fixe progressivement les cellules avec une confiance superieure au seuil de 0.25, en re-injectant les valeurs fixees dans le modèle.\n",
"\n",
"| Metrique | Puzzle 1 | Puzzle 2 | Moyenne |\n",
"| Métrique | Puzzle 1 | Puzzle 2 | Moyenne |\n",
"|----------|----------|----------|---------|\n",
"| Étapes requises | 36 | 49 | 42.5 |\n",
"| Cellules fixees | 36 | 49 | 42.5 |\n",
Expand All @@ -1222,7 +1222,7 @@
"| Temps par étape | ~5s | ~5s | ~5s |\n",
"| Statut final | OK | OK | 100% succes |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **Processus iteratif** : Chaque étape fixe 1 cellule (paramètre `cells_per_iteration=1`) et relance l'inference\n",
"2. **Convergence garantie** : Les deux puzzles convergent vers une solution valide, contrairement au solveur robuste\n",
"3. **Cout temporel** : ~200 secondes par puzzle, soit ~30x plus lent que le solveur robuste (~6 s)\n",
Expand Down Expand Up @@ -1842,26 +1842,26 @@
"source": [
"### Interpretation : le message passing domine le SVI, la relaxation par paires cale\n",
"\n",
"Trois constats sur ces mesures (run de ce notebook, meme machine que les\n",
"Trois constats sur ces mesures (run de ce notebook, même machine que les\n",
"cellules SVI ci-dessus) :\n",
"\n",
"1. **Vitesse** : le BP decimation resout Easy51 a ~0,5 s par grille, contre ~5-8 s\n",
" pour le SVI pur et ~3 minutes pour le SVI iteratif (qui re-execute 300\n",
" iterations a chaque cellule fixee). Messages exacts par facteur, warm start\n",
" itérations a chaque cellule fixee). Messages exacts par facteur, warm start\n",
" entre decisions, pas de taux d'apprentissage ni de poids de contrainte a regler.\n",
"2. **Couverture Easy** : 36/51 pour la decimation pure, contre 1/3 pour le SVI pur\n",
" sur sa propre selection. Le repli borne n'ajoute rien ici (35/51) : sur les\n",
" sur sa propre sélection. Le repli borne n'ajoute rien ici (35/51) : sur les\n",
" grilles faciles, quand la decimation echoue, c'est la *croyance* qui est\n",
" fausse, pas l'irrevocabilite de la decision.\n",
"3. **Le mur des corpus durs** : 0/15 sur top95, 3-4/11 sur hardest. Ce n'est pas\n",
" un defaut d'implementation mais une limite structurelle : avec 810 facteurs\n",
" binaires `!=`, deux cellules d'une meme unite cantonnees a {3,7} s'envoient des\n",
" binaires `!=`, deux cellules d'une même unite cantonnees a {3,7} s'envoient des\n",
" messages symetriques qui s'annulent (ensemble de Hall de taille 2 invisible\n",
" pour la relaxation par paires). La v3 C# franchit ce mur en hybrident avec de\n",
" la propagation de contraintes (la \"voie facile\") ; la suite principielle est\n",
" la v4 (section 7) : des facteurs AllDiff d'arite 9 dont les messages exacts\n",
" (permanente ou affectation hongroise sur une matrice 9x9) capturent les\n",
" ensembles de Hall sans aucun apport deterministe externe."
" ensembles de Hall sans aucun apport déterministe externe."
]
},
{
Expand Down Expand Up @@ -3141,7 +3141,7 @@
"\n",
"### Ce que nous avons implemente\n",
"\n",
"| Classe Python | Equivalent C# | Description |\n",
"| Classe Python | Équivalent C# | Description |\n",
"|---------------|---------------|-------------|\n",
"| `RobustProbabilisticSolverPy` | `RobustProbabilisticSolver` | Une seule inference, mode des Dirichlet |\n",
"| `IterativeProbabilisticSolverPy` | `IterativeSudokuModel` | Fixation iterative des cellules certaines |\n",
Expand All @@ -3154,7 +3154,7 @@
"1. **Infer.NET reste superieur pour les CSP** : Expectation Propagation + contraintes dures\n",
"2. **NumPyro fonctionne avec des limitations** : Contraintes douces moins efficaces\n",
"3. **L'arité 9 franchit Medium sans propagation déterministe** : 9/11 (82 %) sur hardest en décimation max-product randomisée\n",
"4. **Le BP vectorise domine le SVI sur ce probleme** : messages exacts par facteur, ~10x plus rapide que le SVI pur (0,5 s vs 5-8 s) et ~350x que le SVI iteratif (0,5 s vs ~3 min), et la decimation couvre 71% de Easy51 la ou le SVI pur resout 1/3 de sa selection -- mais la relaxation **par paires** cale sur les corpus durs (top95, hardest) : les ensembles de Hall sont invisibles pour des facteurs binaires\n",
"4. **Le BP vectorise domine le SVI sur ce problème** : messages exacts par facteur, ~10x plus rapide que le SVI pur (0,5 s vs 5-8 s) et ~350x que le SVI iteratif (0,5 s vs ~3 min), et la decimation couvre 71% de Easy51 la ou le SVI pur resout 1/3 de sa sélection -- mais la relaxation **par paires** cale sur les corpus durs (top95, hardest) : les ensembles de Hall sont invisibles pour des facteurs binaires\n",
"5. **Un cran sur le graphe, pas sur l'outil** : la v4 (facteurs AllDiff d'arité 9, messages exacts permanente/hongrois + restarts randomisés) franchit le même mur que la propagation de contraintes en restant purement probabiliste — là où la v3 C# payait ce mur avec du déterminisme externe\n",
"\n",
"> **Recommandation** : Pour resoudre des Sudokus en production, utiliser OR-Tools, Z3 ou Choco. La programmation probabiliste est un outil pedagogique pour comprendre l'inference bayesienne."
Expand Down
Loading
Loading