fix(density,#17040): redressement paquet P18 — SMT/Z3-API + SemanticWeb

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-03-Tactics-Python.ipynb

@@ -652,23 +652,6 @@
     "3. `BitVecVal(255, 8)` créé une constante ; `BitVec('x', 8)` créé une variable symbolique."
    ]
   },
-  {
-   "cell_type": "markdown",
-   "id": "lectz3tac-01",
-   "metadata": {},
-   "source": [
-    "### Lecture chiffree : la paire XOR/AND rendue par le solveur\n",
-    "\n",
-    "La sortie imprime une solution concrete : `a = 254 (binaire : 11111110)` et `b =   1 (binaire : 00000001)`. Ces deux vecteurs sont des complements bit a bit exacts : sur chacune des 8 positions, l'un porte 1 quand l'autre porte 0. La sortie le confirme d'elle-meme : `a XOR b = 11111111` (soit 0xFF, la cible imposee) et `a AND b = 00000000`.\n",
-    "\n",
-    "Deux observations mesurees sur cette sortie :\n",
-    "\n",
-    "1. **La seconde contrainte est redondante** : si chaque bit de `a` differe du bit correspondant de `b` (XOR = 0xFF), alors aucun bit ne peut etre commun (AND = 0). Le solveur satisfait les deux contraintes, mais la seconde n'apporte aucune information nouvelle.\n",
-    "2. **L'espace de solutions compte 256 paires** : `b` est entierement determine par `a` (b = a XOR 0xFF), et `a` est libre sur 8 bits, soit 2^8 = 256 modeles valides. Z3 en rend un seul.\n",
-    "\n",
-    "Non mesure : le critere de choix du modele parmi les 256 (le solveur ne fait pas d'optimisation ici, aucune notion de minimum)."
-   ]
-  },
   {
    "cell_type": "code",
    "execution_count": 7,

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-05-Quantifiers-Proofs-Python.ipynb

@@ -317,31 +317,6 @@
     "    print()"
    ]
   },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "### Lecture des 3 théorèmes (ancre sur code[2])\n",
-    "\n",
-    "La sortie verbatim de code[2] montre 3 lignes de vérification pour 3 théorèmes distincts :\n",
-    "\n",
-    "```\n",
-    "Identite multiplicative : x * 1 == x   => VALIDE (negation = unsat)\n",
-    "Commutativite de l'addition : x + y == y + x   => VALIDE (negation = unsat)\n",
-    "Neutre additif a droite : 0 + x == x   => VALIDE (negation = unsat)\n",
-    "```\n",
-    "\n",
-    "**Trois théorèmes, trois domaines d'usage** :\n",
-    "\n",
-    "- L'identité multiplicative est un test du **neutre de la multiplication**. C'est l'axiome qui distingue `*` (opération binaire) de `+` (autre opération binaire) -- si `x * 1 = x` tient, l'element `1` est bien l'unité multiplicative.\n",
-    "- La commutativité de l'addition (`x + y = y + x`) est un test de **symetrie** -- une propriété qu'on tient souvent pour évidente, mais que la machine doit prouver, pas supposer.\n",
-    "- Le neutre additif à droite (`0 + x = x`) est un test du **neutre additif à droite** spécifiquement ; le symétrique `x + 0 = x` est la section 2. Les deux sont équivalents mais éprouvent des chemins d'analyse différents.\n",
-    "\n",
-    "**Pourquoi Z3 les ferme tous en `unsat` tres vite** : les corps reels ont des algorithmes dedies pour l'arithmétique linéaire (Fourier-Motzkin, simplex). Ces 3 théorèmes sont triviaux pour ces algorithmes -- ils ne demandent aucune backtracking de Z3.\n",
-    "\n",
-    "**Implication pédagogique** : ces trois exemples servent de **canary tests**. Si demain une mise a jour de Z3 casse l'un d'eux, on saura immédiatement que la théorie de l'arithmétique reelle est cassée. C'est la meme logique que les canaries dans une mine de charbon."
-   ]
-  },
   {
    "cell_type": "markdown",
    "id": "nb05-forall-examples-interp",
@@ -718,7 +693,7 @@
     "\n",
     "Ecrivez une fonction `prouver_identite_additive` qui prend en entrée un symbolic `x = Real('x')` et rend la formule Z3 `ForAll([x], x + 0 == x)`. Retournez le résultat du solveur.\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "Utilisez le pattern de la cellule code[1] directement, mais parametrize par `x` (au lieu de créer le `x = Real('x')` à l'intérieur). Pour rendre la preuve indépendante de la valeur concrète de `x`, le type doit etre declare en amont.\n",
     "\n",
@@ -1013,7 +988,7 @@
     "\n",
     "Ecrivez une fonction `existe_carre_negatif` qui declare `x = Real('x')` et demande a Z3 si `Exists([x], x*x < 0)` est satisfiable. Retournez le verdict de Z3 sous forme de `sat` / `unsat` / `unknown`.\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "Utilisez directement le pattern de la cellule code[4]. L'énoncé est trivial sur les reels : `x*x >= 0` pour tout `x` reel (par définition du carre), donc `x*x < 0` est `unsat`. Mais la logique de la preuve est moins évidente : Z3 doit éliminer le quantificateur sur les corps reels ordonnés.\n",
     "\n",
@@ -1028,7 +1003,7 @@
     "\n",
     "Verdict `unsat` (formule FAUSSE : il n'existe PAS de carre reel strictement negatif). En logique Z3 : `Exists([x], x*x < 0)` n'a pas de temoin.\n",
     "\n",
-    "> **Note pédagogique :**",
+    "> **Note pédagogique :**\n",
     "\n",
     "Cet exercice inverse l'Exercice 1 : on démontre maintenant l'**impossibilité** d'une propriété (vs la vérification d'une loi universelle). Les deux patterns sont complémentaires :\n",
     "- Exercice 1 : `ForAll` valide (preuve par `unsat` de la négation).\n",
@@ -1228,7 +1203,7 @@
     "\n",
     "Ecrivez une fonction `prouver_pas_de_plus_grand_reel` qui prouve `ForAll([x], Exists([y], y > x))` -- pour tout reel `x`, il existe un reel strictement supérieur. C'est l'**axiome d'Archimede** simplifie (la verison archimedienne est plus forte : pour tout `x`, il existe `n` entier tel que `1/n < x`).\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "C'est exactement la cellule code[7] reformulée en fonction. Le pattern est `ForAll([x], Exists([y], y > x))`, et la vérification est `Not(Exists([x], ForAll([y], y <= x)))` -- la négation affirme qu'il existe un plus grand reel, que Z3 refute.\n",
     "\n",
@@ -1451,35 +1426,6 @@
     "**Application** : un test d'intégration sur Z3 peut utiliser `proof=True` pour **verifier** qu'un certificat est effectivement produit. Sans cette vérification, un solveur pourrait rendre `unsat` par accident (bug, confusion, integer overflow) et l'utilisateur ne le saurait pas."
    ]
   },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "### Lecture des règles de preuve (ancre sur code[12])\n",
-    "\n",
-    "La sortie verbatim de code[12] énumère 15 règles distinctes utilisees par Z3 dans la preuve de l'identité additive. Les plus fréquentes sont :\n",
-    "\n",
-    "```\n",
-    "== : 11 fois        (propagation d'egalites)\n",
-    "opaque : 4 fois     (termes opaques, e.g. constantes symboliques)\n",
-    "trans : 3 fois      (transitivite)\n",
-    "rewrite : 3 fois    (reecriture de termes)\n",
-    "Not : 2 fois        (elimination de la negation)\n",
-    "monotonicite : 2 fois\n",
-    "```\n",
-    "\n",
-    "**Quatre roles distincts dans la preuve** :\n",
-    "\n",
-    "1. **`==` (égalité)** : 11 applications -- la règle la plus utilisee parce que la preuve repose sur la propagation d'égalités comme `(x + 0) = x`.\n",
-    "2. **`opaque` (termes opaques)** : 4 applications -- concerne les termes qui ne peuvent pas etre unfolds (comme les `def` non unfolds). Z3 les laisse tels quels et raisonne sur leur identité.\n",
-    "3. **`trans` (transitivité)** : 3 applications -- utilisee pour combiner des chaines d'égalités (`a = b`, `b = c` -> `a = c`).\n",
-    "4. **`monotonicite`** : 2 applications -- la règle si `a == b` alors `f(a) == f(b)`, utilisee pour propager l'égalité dans le contexte de la fonction `+`.\n",
-    "\n",
-    "**Histogramme attendu pour une preuve arithmétique** : les preuves linéaires utilisent massivement `==` et `trans`, peu de `monotonicite` complexe. Les preuves non-linéaires utilisent `monotonicite` plus intensément, et peuvent avoir besoin de `cad` (cylindrical algebraic décomposition) pour les quotients polynomiaux.\n",
-    "\n",
-    "**Implication pour le pédagogue** : si on veut enseigner le pattern de Z3 a un étudiant, les **règles les plus fréquentes** (`==`, `trans`, `rewrite`) sont les premières a apprendre. Les règles rares (`cad`, `monotonicite_complexe`) n'apparaissent que dans des cas particuliers."
-   ]
-  },
   {
    "cell_type": "markdown",
    "id": "nb05-recap",

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-11-Graph-Coloring-Python.ipynb

@@ -181,7 +181,7 @@
     "\n",
     "Sortie verbatim : definition de N=10 sommets, edges=15 aretes (5 pentagone externe + 5 pentagramme interne + 5 rayons).\n",
     "\n",
-    "### Lecture approfondie\n",
+    "### Lecture approfondie — la liste d'aretes du Petersen\n",
     "\n",
     "La liste des aretes est explicite :\n",
     "- **Pentagone externe** : (0,1), (1,2), (2,3), (3,4), (4,0)\n",
@@ -334,40 +334,6 @@
     "print(\"Meme graphe, meme algorithme : %d couleurs vs %d couleurs selon l'ordre.\" % (greedy_natural_colors, greedy_bad_colors))\n"
    ]
   },
-  {
-   "cell_type": "markdown",
-   "id": "",
-   "metadata": {},
-   "source": [
-    "### Verbatim code[2] : glouton first-fit\n",
-    "\n",
-    "Sortie verbatim : `Coloration gloutonne : 3 couleurs` (dans le bon ordre, par exemple 0,1,2,3,4,5,6,7,8,9).\n",
-    "\n",
-    "### Lecture approfondie\n",
-    "\n",
-    "Le glouton assigne a chaque sommet la plus petite couleur non utilisee par ses voisins déjà colores. Pour le Petersen avec ordre 0,1,2,3,4,5,6,7,8,9 :\n",
-    "- Sommet 0 : couleur 0\n",
-    "- Sommet 1 : voisin de 0 (couleur 0), couleur 1\n",
-    "- Sommet 2 : voisin de 1 (couleur 1), couleur 0\n",
-    "- Sommet 3 : voisin de 2 (couleur 0) et 4 (couleur 1), couleur 2\n",
-    "- ...\n",
-    "\n",
-    "Résultat : couleurs = [0, 1, 0, 2, ?, ...] en 3 couleurs.\n",
-    "\n",
-    "### Cout computationnel\n",
-    "\n",
-    "O(N + M) = O(10 + 15) = 25 operations, < 1 ms.\n",
-    "\n",
-    "### Variante : Welsh-Powell\n",
-    "\n",
-    "Ordonner les sommets par degré decroissant avant le glouton. Pour Petersen, tous les sommets ont degré 3 -- donc Welsh-Powell équivaut au glouton standard.\n",
-    "\n",
-    "### Implementation alternative : DSATUR\n",
-    "\n",
-    "DSATUR (Brélaz 1979) colore en prioritant le sommet avec le plus de couleurs différentes parmi ses voisins. Souvent optimal en pratique.\n",
-    ""
-   ]
-  },
   {
    "cell_type": "markdown",
    "id": "b55c722a",
@@ -377,7 +343,7 @@
     "\n",
     "Le glouton trouve **3 couleurs** dans le bon ordre mais **4 dans l'ordre par defaut**.\n",
     "\n",
-    "### Lecture\n",
+    "### Lecture — l'ordre de parcours fait varier le glouton\n",
     "\n",
     "Cela illustre une propriete cle : **l'ordre de parcours** peut modifier significativement le résultat du glouton. Pour un même graphe, l'ordre de parcours peut faire varier le nombre de couleurs de chi(G) a chi(G) + 1, voire plus pour certains graphes.\n",
     "\n",
@@ -588,7 +554,7 @@
     "\n",
     "Sortie verbatim : `Nombre chromatique chi(Petersen) = 3` + la 3-coloration trouvee.\n",
     "\n",
-    "### Lecture approfondie\n",
+    "### Lecture approfondie — le verdict k=1, k=2, k=3 du solveur\n",
     "\n",
     "Pour k=1, Z3 retourne UNSAT (UNSATISFIABLE) : impossible de colorier avec 1 seule couleur car il y a des aretes.\n",
     "\n",
@@ -622,7 +588,7 @@
     "  Solveur Z3 (optimalite) : chi = 3\n",
     "```\n",
     "\n",
-    "### Lecture\n",
+    "### Lecture — glouton vs solveur, trois resultats a comparer\n",
     "\n",
     "Trois résultats a comparer :\n",
     "1. **Glouton bon ordre** : 3 couleurs (optimal par chance).\n",
@@ -830,8 +796,7 @@
     "\n",
     "### Interet pédagogique\n",
     "\n",
-    "La visualisation permet de voir immediatement la structure du Petersen : un cycle externe et un cycle interne (pentagramme) relies par 5 rayons. La 3-coloration est evidente visuellement.\n",
-    ""
+    "La visualisation permet de voir immediatement la structure du Petersen : un cycle externe et un cycle interne (pentagramme) relies par 5 rayons. La 3-coloration est evidente visuellement.\n"
    ]
   },
   {
@@ -942,7 +907,7 @@
     "\n",
     "Generalisation : pour tout graphe G, `chi(G) >= omega(G)` (taille de la plus grande clique). Pour Petersen modifie, omega = 4 et chi = 4 -- optimal.\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "Vérifier que 5-6, 0-6 et 1-5 ne sont pas déjà des aretes du Petersen (elles ne le sont pas : le pentagramme interne relie 5-7, 7-9, 9-6, 6-8, 8-5).\n",
     ""
@@ -1017,7 +982,7 @@
     "\n",
     "Cas reel : 200 examens, 5000 étudiants, degré moyen 12. Le solveur Z3 trouve le nombre minimum de créneaux en quelques secondes.\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "Construire un graphe avec 5 sommets et toutes les paires (10 aretes = K_5).\n",
     ""
@@ -1075,7 +1040,7 @@
     "\n",
     "Le **polynome chromatique** P(G, k) donne le nombre exact de k-colorations pour chaque k. Pour Petersen, P(G, k) = k(k-1)(k-2)(k^7 - 12k^6 + 67k^5 - 230k^4 + 529k^3 - 814k^2 + 775k - 352). Vérifie : P(G, 3) = 3 x 2 x 1 x 20 = **120**, conforme au compte attendu.\n",
     "\n",
-    "> **Indice :**",
+    "> **Indice :**\n",
     "\n",
     "La commande `s.add(Or([Color[v] != sol[v] for v in range(N)]))` exclut la solution trouvée (et elle seule) -- les 6 permutations d'une même coloration sont énumérées séparément, d'où la division finale par 3! = 6.\n",
     "\n",
@@ -1144,43 +1109,6 @@
     "**Verdict** : 120 colorations distinctes, soit 120 / 6 = **20 classes** à permutation des 3 couleurs près — conforme au stub (`attendu : 120 total, 20 a permutation pres`)."
    ]
   },
-  {
-   "cell_type": "markdown",
-   "id": "",
-   "metadata": {},
-   "source": [
-    "### Verbatim code[9] : exercice comptage 3-colorations\n",
-    "\n",
-    "Sortie verbatim : `Exercice 3 a completer` (stub, ne pas remplir la solution).\n",
-    "\n",
-    "### Lecture approfondie\n",
-    "\n",
-    "L'exercice demande de compter les **3-colorations distinctes** du graphe de Petersen. La technique :\n",
-    "1. Resoudre avec k=3, obtenir une solution.\n",
-    "2. Ajouter une contrainte qui exclut cette solution.\n",
-    "3. Re-resoudre, obtenir une autre solution.\n",
-    "4. Repeter jusqu'a UNSAT.\n",
-    "\n",
-    "Chaque appel `s.check()` trouve une nouvelle solution, et le total est le nombre de colorations.\n",
-    "\n",
-    "### Cout computationnel\n",
-    "\n",
-    "Z3 énumère les 120 solutions en quelques secondes.\n",
-    "\n",
-    "### Verdict attendu\n",
-    "\n",
-    "120 colorations distinctes (toutes permutations des 3 couleurs confondues) ; à permutation près (3! = 6) : 120 / 6 = **20 classes**.\n",
-    "\n",
-    "### Pour aller plus loin\n",
-    "\n",
-    "On peut utiliser `AllDifferent` ou des contraintes symetriques pour reduire l'espace de recherche.\n",
-    "\n",
-    "> **Indice :**",
-    "\n",
-    "La commande `s.add(Or([Color[v] != sol[v] for v in range(N)]))` exclut la solution trouvée (et elle seule) -- chaque nouvelle résolution donne une coloration différente, jusqu'à UNSAT.\n",
-    ""
-   ]
-  },
   {
    "cell_type": "markdown",
    "id": "8d1e30c1",