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
14 changes: 7 additions & 7 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-10-ORTools-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -709,15 +709,15 @@
"source": [
"### Interpretation : Résultat OR-Tools CP-SAT\n",
"\n",
"Le solveur OR-Tools a resolu un puzzle difficile en quelques dizaines de millisecondes (temps exact affiche par la cellule de resolution ci-dessus ; CP-SAT etant non-deterministe, la valeur varie d'une execution a l'autre et selon la machine).\n",
"Le solveur OR-Tools a resolu un puzzle difficile en quelques dizaines de millisecondes (temps exact affiche par la cellule de resolution ci-dessus ; CP-SAT etant non-déterministe, la valeur varie d'une exécution a l'autre et selon la machine).\n",
"\n",
"| Aspect | Valeur | Signification |\n",
"|--------|--------|---------------|\n",
"| **Temps de resolution** | (cellule ci-dessus) | Performance excellente |\n",
"| **Statut** | FEASIBLE | Solution trouvee |\n",
"| **Approche** | Declarative | Modèle de contraintes, pas d'algorithme a ecrire |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **Simplicite du code** : Seuls 30 lignes pour définir le modèle complet\n",
"2. **Contrainte AllDifferent** : OR-Tools l'implemente de maniere très efficace\n",
"3. **Pas de parametrage** : L'heuristique par defaut fonctionne très bien\n",
Expand Down Expand Up @@ -1339,13 +1339,13 @@
"source": [
"### Exemple miroir : Minimiser un cout pondere avec CP-SAT\n",
"\n",
"Miroir de l'exemple precedent (`solve_max_reward_latin_square`) : meme espace de carres latins realisables, meme variables booleennes `x[i,j,v]`, mais on **minimise** un cout dependant de `(i, j, v)` au lieu de maximiser un reward. Cela demontre `model.Minimize(...)` -- le pendant exact de `model.Maximize(...)`.\n",
"Miroir de l'exemple précédent (`solve_max_reward_latin_square`) : même espace de carres latins realisables, même variables booleennes `x[i,j,v]`, mais on **minimise** un cout dependant de `(i, j, v)` au lieu de maximiser un reward. Cela demontre `model.Minimize(...)` -- le pendant exact de `model.Maximize(...)`.\n",
"\n",
"> **Piege de degenerescence (Prong-B, EPIC #3801).** Une version anterieure de cet exemple minimisait la *somme des valeurs sur la diagonale*. C'etait un objectif **degenere** : chaque cellule diagonale `val[i][i]` appartient a `1..n`, donc le minorant trivial est `n` (somme de `n` fois la valeur `1`), atteignable en plaçant `1` sur chaque case diagonale -- ce qu'**aucune contrainte du carre latin n'interdit**. Le solveur renvoyait bien `OPTIMAL`, mais ce statut ne prouvait **rien** : l'optimum etait le minorant evident, trouvable de tete sans aucune recherche. La capacite d'optimisation distinctive de CP-SAT (branch-and-bound, relaxation lineaire) y etait **invisible** -- exactement le symptome d'un cas trop trivial pour mettre le moteur en valeur.\n",
"\n",
"Avec un cout **pondere aleatoire** `cost[i][j][v]`, l'optimum n'est plus devinable : la solution bon-marche cellule par cellule (prendre la valeur de cout minimal dans chaque case) viole les contraintes de carre latin. CP-SAT doit alors **chercher** parmi tous les carres latins realisables celui de cout total minimal. On rend cette recherche **visible** dans la sortie en comparant l'optimum au *minorant naif* (somme des couts minima par cellule, en ignorant les contraintes) : l'ecart `OPTIMAL - minorant_naif > 0` prouve que les contraintes mordent et que l'optimisation est non-triviale.\n",
"Avec un cout **pondere aléatoire** `cost[i][j][v]`, l'optimum n'est plus devinable : la solution bon-marche cellule par cellule (prendre la valeur de cout minimal dans chaque case) viole les contraintes de carre latin. CP-SAT doit alors **chercher** parmi tous les carres latins realisables celui de cout total minimal. On rend cette recherche **visible** dans la sortie en comparant l'optimum au *minorant naif* (somme des couts minima par cellule, en ignorant les contraintes) : l'ecart `OPTIMAL - minorant_naif > 0` prouve que les contraintes mordent et que l'optimisation est non-triviale.\n",
"\n",
"**Question** : pourquoi le meme piege (optimum = borne triviale) guetterait-il aussi un objectif « maximiser la somme des valeurs sur la diagonale » ? *(Indice : le majorant trivial serait `n^2`, atteint en plaçant `n` sur chaque case diagonale -- la encore completable en carre latin.)*\n"
"**Question** : pourquoi le même piege (optimum = borne triviale) guetterait-il aussi un objectif « maximiser la somme des valeurs sur la diagonale » ? *(Indice : le majorant trivial serait `n^2`, atteint en plaçant `n` sur chaque case diagonale -- la encore completable en carre latin.)*\n"
]
},
{
Expand Down Expand Up @@ -1488,7 +1488,7 @@
"| **Puzzles difficiles** | (benchmark ci-dessus) | Pas de degradation significative |\n",
"| **Taux de succes** | 100% | Solveur complet |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **Performance consistante** : Les puzzles difficiles ne prennent pas beaucoup plus de temps que les faciles\n",
"2. **Solveur complet** : Tous les puzzles sont resolus\n",
"3. **Simplicité** : Le code est concis et lisible\n",
Expand Down Expand Up @@ -1522,7 +1522,7 @@
"- Bin packing et cutting stock\n",
"- Emploi du temps et allocation de ressources\n",
"\n",
"Le Sudoku est un excellent problème pedagogique car il est facile a comprendre mais assez complexe pour illustrer les concepts cles de la programmation par contraintes.\n",
"Le Sudoku est un excellent problème pedagogique car il est facile a comprendre mais assez complexe pour illustrer les concepts clés de la programmation par contraintes.\n",
"\n",
"***\n",
"\n",
Expand Down
28 changes: 14 additions & 14 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-11-Choco-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@
"| **Version JPype** | 1.5.0 (dernière) | Compatible avec Java 8-17 et Python 3.7-3.11 |\n",
"| **Sortie silencieuse** | Pas de details | Le flag `-q` supprime les messages de progression |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. JPype permet d'instancier des classes Java et d'appeler leurs méthodes depuis Python\n",
"2. L'installation automatique évite a l'utilisateur de lancer `pip install` manuellement\n",
"3. La fonction `check_call` leve une exception si l'installation echoue (gestion d'erreur)\n",
Expand Down Expand Up @@ -308,7 +308,7 @@
"| **Statut JVM** | Demarree | La machine virtuelle Java est prete a executer Choco |\n",
"| **Mode JPype** | Import active | L'API Java est accessible depuis Python |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. Le JAR avec dépendances évite de télécharger séparément toutes les bibliotheques Choco\n",
"2. La vérification `choco_path.exists()` évite de télécharger le fichier a chaque exécution\n",
"3. La méthode `jpype.startJVM(classpath=[...])` initialise la JVM avec le classpath Choco\n",
Expand Down Expand Up @@ -411,7 +411,7 @@
"| **IntVar** | org.chocosolver.solver.variables.IntVar | Variable entière avec domaine [min, max] |\n",
"| **allDifferent** | Méthode de Model | Contrainte globale : toutes les variables doivent etre différentes |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. L'importation reussie prouve que la JVM est demarree et que le JAR Choco est charge\n",
"2. L'API Java de Choco est accessible directement depuis Python via JPype\n",
"3. La notation `org.chocosolver.solver.Model` suit les conventions Java (packages)\n",
Expand Down Expand Up @@ -512,7 +512,7 @@
"| **Sudoku_hardest.txt** | 11 puzzles très difficiles | Collection d'Arto Inkala (Sudokus les plus durs) |\n",
"| **Sudoku_top95.txt** | 95 puzzles difficiles | Collection de référence pour benchmarking |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. L'utilisation d'un chemin absolu (`Path` avec `r\"...\"`) évite les problèmes de repertoire courant\n",
"2. La méthode `glob('*.txt')` liste tous les fichiers .txt de maniere robuste\n",
"3. Les fichiers sont organises par niveau de difficulte pour les tests progressifs\n",
Expand Down Expand Up @@ -667,7 +667,7 @@
"- **Colonnes 1-3** : Premier bloc vertical (colonnes 1,2,3 du Sudoku)\n",
"- **Separateurs** : Lignes `---` et colonnes `|` tous les 3 caractères\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. Le format texte 81-caractères est standard pour les puzzles Sudoku (competitions, echanges)\n",
"2. La fonction `puzzle_to_grid` convertit ce format lineaire en grille 9x9 pour le traitement\n",
"3. La fonction `print_grid` ajoute des séparateurs visuels pour faciliter la lecture\n",
Expand Down Expand Up @@ -877,7 +877,7 @@
"- **Blocs 3x3** : Chaque bloc contient exactement les chiffres 1-9 sans répétition\n",
"- **Cohérence** : Les 45 valeurs initiales sont preservees dans la solution\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. La classe `ChocoSudokuSolver` encapsule toute la logique de modélisation CSP\n",
"2. L'API Choco 4.10+ est intuitive : `Model` -> `intVar` -> `allDifferent` -> `solve()`\n",
"3. Le temps de résolution quasi-instantané montre que Choco est parfaitement adéquat pour Sudoku\n",
Expand Down Expand Up @@ -1130,7 +1130,7 @@
"| **Taux de succes** | 3/3 (100%) | Choco resout tous les puzzles faciles testes |\n",
"| **Temps moyen** | quelques ms (cf. benchmark ci-dessus) | Performance excellente pour des puzzles faciles |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. Les temps de résolution restent très faibles, ce qui est quasi-instantané pour l'utilisateur\n",
"2. La variation entre les puzzles (cf. mesures de la cellule ci-dessus) montre que même les puzzles \"faciles\" ont des structures différentes\n",
"3. La contrainte `allDifferent` globale de Choco est très efficace pour reduire l'espace de recherche\n",
Expand Down Expand Up @@ -1237,7 +1237,7 @@
"| **Taux de succes** | 2/2 (100%) | Choco resout tous les puzzles difficiles testes |\n",
"| **Temps moyen** | fraction de seconde (cf. ci-dessus) | Performance acceptable pour un usage général |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. La variation importante entre les puzzles (cf. mesures de la cellule ci-dessus) montre que la difficulte d'un Sudoku dépend grandement de sa structure\n",
"2. Les temps de résolution restent sous la seconde, ce qui est excellent pour un solveur CP générique\n",
"3. Choco avec la stratégie par defaut (InputOrder) est déjà efficace sur les puzzles difficiles\n",
Expand Down Expand Up @@ -1478,10 +1478,10 @@
"\n",
"| Puzzle | Choco (DomWDEG) | OR-Tools | python-constraint |\n",
"|--------|-----------------|----------|-------------------|\n",
"| Facile | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) |\n",
"| Moyen | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) |\n",
"| Difficile | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) | Timeout (valeur de configuration) |\n",
"| Hardest | (mesure, voir cellule precedente) | (mesure, voir cellule precedente) | Echec |\n",
"| Facile | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) |\n",
"| Moyen | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) |\n",
"| Difficile | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) | Timeout (valeur de configuration) |\n",
"| Hardest | (mesure, voir cellule précédente) | (mesure, voir cellule précédente) | Echec |\n",
"\n",
"\n",
"> **Note (mandat #9377/#9434)** : les **durées wall-clock** de cette table comparative sont **machine-dépendantes** par construction (JVM Java startup + JPype bridge Python↔Java + overhead Graphe Choco, charge CPU du runner) et **drainées**. Le **rapport d'ordres de grandeur** (Choco ≈ 5× OR-Tools ≪ python-constraint sur ce puzzle, Timeout pour python-constraint sur les plus difficiles) est **reproductible d'une exécution à l'autre** et **conservé**. Les **mesures exactes** restent **visibles** dans les cellules de mesure amont (cellule de banc d'essai du notebook Sudoku-11-Choco-Python ou notebooks Sudoku-10-OR-Tools-Python / Sudoku-09-python-constraint pour les mesures comparatives). La synthèse pédagogique **tient sur la discrimination qualitative** (production vs pédagogie vs apprentissage), pas sur les valeurs quantitatives ponctuelles.\n"
Expand Down Expand Up @@ -1590,7 +1590,7 @@
"| **Grilles 3x3** | Separees par lignes épaisses | Structure du Sudoku respectee |\n",
"| **Positionnement** | Coordonnees (c+0.5, 8.5-r) | Inversion de l'axe Y pour affichage correct |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. La distinction visuelle permet de vérifier rapidement que le solveur n'a pas modifie les valeurs initiales\n",
"2. L'inversion de l'axe Y (`8.5-r`) est nécessaire car matplotlib origin est en bas alors que les matrices ont l'origine en haut\n",
"3. Les lignes épaisses (`lw=2`) marquent les blocs 3x3, facilitant la vérification visuelle\n",
Expand Down Expand Up @@ -1789,7 +1789,7 @@
"3. **Exploite** différentes stratégies de recherche (DomOverWDeg > InputOrder)\n",
"4. **Compare** Choco avec d'autres solveurs (OR-Tools, python-constraint)\n",
"\n",
"### Points Cles\n",
"### Points Clés\n",
"\n",
"- **Choco est ideal pour l'enseignement** et la recherche en CP\n",
"- **DomOverWDeg** est la stratégie recommandée pour Sudoku\n",
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-CSharp.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -1781,7 +1781,7 @@
"| Z3 Bit Vector Substitution | Substitution | Réutilise les contraintes génériques | Plus complexe à mettre en oeuvre |\n",
"| Z3 Bit Vector Tactic | Tactiques | Simplification automatique | Overhead potentiel |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"\n",
"1. **Vecteurs de bits** : representer chaque case sur 4 bits (valeurs 1-9) suffit et donne des variables plus compactes que les entiers ; c'est aussi l'encodage le plus stable sur les grilles difficiles dans le banc d'essai ci-dessus.\n",
"\n",
Expand Down
18 changes: 9 additions & 9 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-Python.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@
"source": [
"## 1. Solveur Z3 SMT\n",
"\n",
"**Z3** est un solveur **SMT** (*Satisfiability Modulo Theories*) developpe a l'origine par **Microsoft Research** (Leonardo de Moura et Nikolaj Bjorner), desormais publie en **open-source sous licence MIT** dans le depot [`Z3Prover/z3`](https://github.com/Z3Prover/z3). Il combine la puissance des solveurs SAT avec des theories mathematiques (arithmetique, tableaux, bitvectors, etc.)."
"**Z3** est un solveur **SMT** (*Satisfiability Modulo Theories*) developpe a l'origine par **Microsoft Research** (Leonardo de Moura et Nikolaj Bjorner), desormais publie en **open-source sous licence MIT** dans le depot [`Z3Prover/z3`](https://github.com/Z3Prover/z3). Il combine la puissance des solveurs SAT avec des théories mathematiques (arithmetique, tableaux, bitvectors, etc.)."
]
},
{
Expand Down Expand Up @@ -518,14 +518,14 @@
"| **Statut** | sat | Solution trouvee |\n",
"| **Type de variables** | Int | Entiers symboliques |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **API simple** : La contrainte `Distinct` est très expressive\n",
"2. **Théorie des entiers** : Z3 utilise QF_LIA (Linear Integer Arithmetic)\n",
"3. **Flexibilite** : Z3 peut facilement etendre le modèle avec d'autres contraintes\n",
"\n",
"> **Note technique** : La contrainte `Distinct` de Z3 est plus puissante que l'inegalite binaire car elle permet au solveur d'utiliser des algorithmes specialised pour la propagation.\n",
">\n",
"> **Regle #9434** : le temps de resolution (machine-dependant) est mesure dynamiquement par la cellule de code ci-dessus ; il n'est pas fige ici."
"> **Règle #9434** : le temps de resolution (machine-dependant) est mesure dynamiquement par la cellule de code ci-dessus ; il n'est pas fige ici."
]
},
{
Expand Down Expand Up @@ -797,14 +797,14 @@
"| Puzzle 4 | ~3x plus rapide |\n",
"| Puzzle 5 | ~2x plus rapide |\n",
"\n",
"**Points cles** :\n",
"**Points clés** :\n",
"1. **BitVectors sont plus proches du hardware** : Z3 peut utiliser des opérations bit-level\n",
"2. **Domaine restreint** : 4 bits = 16 valeurs, exactement ce qu'il faut pour 1-9\n",
"3. **Propagation plus efficace** : Les contraintes bit-level sont plus simples a propager\n",
"\n",
"> **Note technique** : Les BitVectors sont representes en precision fixe (4 bits ici), ce qui permet a Z3 d'utiliser des algorithmes de propagation plus efficaces. Les entiers symboliques en Z3 ont une precision arbitraire, ce qui ajoute de la complexite.\n",
">\n",
"> **Regle #9434** : les temps absolus (machine-dependants) sont mesures dynamiquement par la cellule de benchmark ci-dessus ; seuls les ordres de grandeur du speedup (structurels, stables cross-machine) sont conserves ici."
"> **Règle #9434** : les temps absolus (machine-dependants) sont mesures dynamiquement par la cellule de benchmark ci-dessus ; seuls les ordres de grandeur du speedup (structurels, stables cross-machine) sont conserves ici."
]
},
{
Expand Down Expand Up @@ -1324,16 +1324,16 @@
"`Optimize()` resout des problemes ou l'on **maximise** (ou **minimise**) un\n",
"objectif sous contraintes -- c'est le moteur de la programmation **MaxSMT**\n",
"(maximisation sat-modulo-theories, utilise en verification, scheduling,\n",
"allocation de ressources, debug de modeles).\n",
"allocation de ressources, debug de modèles).\n",
"\n",
"**Demonstration** : un « carre latin a bonus » -- chaque cellule (i, j) offre un\n",
"*reward* dependant de la valeur placee. Parmi tous les carres latins 5x5\n",
"valides, `Optimize()` + `maximize()` trouve celui qui **maximise le reward\n",
"total**. Le statut `sat` certifie que l'optimum est atteint (preuve\n",
"non-vacuous).\n",
"\n",
"> Miroir de la demo CP-SAT du notebook `Sudoku-10-ORTools-Python` (meme\n",
"> probleme, meme reward 178), mais avec l'API SMT `z3.Optimize()` au lieu de\n",
"> Miroir de la demo CP-SAT du notebook `Sudoku-10-ORTools-Python` (même\n",
"> problème, même reward 178), mais avec l'API SMT `z3.Optimize()` au lieu de\n",
"> `cp_model.CpModel.Maximize()`.\n"
]
},
Expand Down Expand Up @@ -1483,7 +1483,7 @@
"lieu de maximiser le reward.\n",
"\n",
"**Indices** :\n",
"1. Gardez les memes contraintes (carre latin : `PbEq` one-value-per-cell,\n",
"1. Gardez les mêmes contraintes (carre latin : `PbEq` one-value-per-cell,\n",
" latin rows/cols).\n",
"2. Remplacez `opt.maximize(reward_total)` par :\n",
" ```python\n",
Expand Down
Loading
Loading