diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md
index acfd9acd96..84e7bc8d66 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md
+++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md
@@ -66,6 +66,7 @@ Une série sœur existe en C# : [SymbolicAI/Z3-Linq2Z3/](../Z3-Linq2Z3/README.md
 | 11 | [Coloration de graphe (Petersen)](Z3-11-Graph-Coloring-Python.ipynb) | `Int` par sommet, contraintes d'arêtes `!=`, recherche linéaire du nombre chromatique, `unsat` = preuve d'optimalité | ~30 min | PRODUCTION |
 | 12 | [Arithmétique réelle](Z3-12-Real-Arithmetic-Python.ipynb) | Théorie `Real`, solution rationnelle exacte, irrationnel algébrique (racine de 2 comme `root-obj`), preuve d'absence sur R (`unsat`) | ~25 min | PRODUCTION |
 | 13 | [UNSAT cores](Z3-13-UnsatCores-Python.ipynb) | `assert_and_track`, `unsat_core()`, noyau minimal d'insatisfiabilité, diagnostic des contraintes conflictuelles | ~25 min | PRODUCTION |
+| 13b | [UNSAT cores : le MUS](Z3-13b-UnsatCores-MUS-Python.ipynb) | Compagnon du 13 : core invisible à l'inspection (chaîne de précédences), minimalité non garantie par Z3, MUS (Minimal Unsatisfiable Subset) par algorithme deletion-based, deux preuves du même UNSAT | ~20 min | BETA |
 | 14 | [Bit-vectors](Z3-14-BitVectors-Overflow-Python.ipynb) | Théorie `BitVec`, débordement arithmétique (`ULT`/`UGE`), preuve d'inévitabilité/sécurité, extraction de champ bit-à-bit | ~30 min | PRODUCTION |
 | 15 | [Tableaux imbriqués et grilles 2D](Z3-15-Nested-Arrays-2D-Python.ipynb) | Grille 2D déclarative (`Distinct`/`Sum`) vs brute (`Array` de `Array`, `Store`/`Select`), carré latin, Sudoku 4×4, carré magique | ~30 min | PRODUCTION |
 | 16 | [Meal-Planner déclaratif](Z3-16-Meal-Planner-Python.ipynb) | Menu équilibré (index / énumération / booléen), `Optimize.minimize` du coût, plan hebdomadaire matriciel `jours × plats` vs glouton | ~35 min | PRODUCTION |
diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb
index a5fb05e76f..499b195283 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb
@@ -5,10 +5,10 @@
    "id": "de430bb4",
    "metadata": {
     "papermill": {
-     "duration": 0.003423,
-     "end_time": "2026-08-12T23:06:15.166604+00:00",
+     "duration": 0.002149,
+     "end_time": "2026-09-28T11:04:51.901525",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.163181+00:00",
+     "start_time": "2026-09-28T11:04:51.899376",
      "status": "completed"
     },
     "tags": []
@@ -27,16 +27,16 @@
    "id": "71e1306a",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.173767Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.173512Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.205291Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.204611Z"
+     "iopub.execute_input": "2026-09-28T11:04:51.906745Z",
+     "iopub.status.busy": "2026-09-28T11:04:51.906436Z",
+     "iopub.status.idle": "2026-09-28T11:04:51.929915Z",
+     "shell.execute_reply": "2026-09-28T11:04:51.929389Z"
     },
     "papermill": {
-     "duration": 0.083537,
-     "end_time": "2026-08-12T23:06:15.253368+00:00",
+     "duration": 0.026781,
+     "end_time": "2026-09-28T11:04:51.930769",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.169831+00:00",
+     "start_time": "2026-09-28T11:04:51.903988",
      "status": "completed"
     },
     "tags": []
@@ -60,10 +60,10 @@
    "id": "95e47844",
    "metadata": {
     "papermill": {
-     "duration": 0.002743,
-     "end_time": "2026-08-12T23:06:15.259805+00:00",
+     "duration": 0.001832,
+     "end_time": "2026-09-28T11:04:51.934523",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.257062+00:00",
+     "start_time": "2026-09-28T11:04:51.932691",
      "status": "completed"
     },
     "tags": []
@@ -80,16 +80,16 @@
    "id": "53ee7428",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.266567Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.266321Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.339940Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.339297Z"
+     "iopub.execute_input": "2026-09-28T11:04:51.939000Z",
+     "iopub.status.busy": "2026-09-28T11:04:51.938666Z",
+     "iopub.status.idle": "2026-09-28T11:04:51.986575Z",
+     "shell.execute_reply": "2026-09-28T11:04:51.986145Z"
     },
     "papermill": {
-     "duration": 0.078083,
-     "end_time": "2026-08-12T23:06:15.340669+00:00",
+     "duration": 0.051477,
+     "end_time": "2026-09-28T11:04:51.987779",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.262586+00:00",
+     "start_time": "2026-09-28T11:04:51.936302",
      "status": "completed"
     },
     "tags": []
@@ -118,7 +118,16 @@
   {
    "cell_type": "markdown",
    "id": "052d9b83",
-   "metadata": {},
+   "metadata": {
+    "papermill": {
+     "duration": 0.004274,
+     "end_time": "2026-09-28T11:04:51.994549",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:51.990275",
+     "status": "completed"
+    },
+    "tags": []
+   },
    "source": [
     "**Lecture chiffree — un systeme ou le core serait TOUT.** `' a->b, a, !b ' : unsat` : le verdict brut tombe en une ligne. Mais ce petit systeme a une propriete que les exemples suivants n'auront pas : aucune de ses trois contraintes n'est superflue. Chaque paire prise seule est satisfiable — `{a->b, a}` tient avec `b` vrai, `{a->b, !b}` tient avec `a` faux, `{a, !b}` tient sans l'implication. Autrement dit, un core etiquete de ce systeme contiendrait les TROIS contraintes : le conflit nait de la combinaison complete, pas d'une paire. C'est la frontiere utile a connaitre avant la section suivante — l'etiquetage `assert_and_track` ne reduit que ce qui peut l'etre : quand chaque contrainte participe a la refutation, le core egale le systeme, et l'explication reste a ecrire a la main.\n"
    ]
@@ -128,10 +137,10 @@
    "id": "58f66f80",
    "metadata": {
     "papermill": {
-     "duration": 0.002739,
-     "end_time": "2026-08-12T23:06:15.346361+00:00",
+     "duration": 0.001846,
+     "end_time": "2026-09-28T11:04:51.998277",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.343622+00:00",
+     "start_time": "2026-09-28T11:04:51.996431",
      "status": "completed"
     },
     "tags": []
@@ -148,16 +157,16 @@
    "id": "cdd127a9",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.352980Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.352813Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.359504Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.358729Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.002874Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.002640Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.022419Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.021879Z"
     },
     "papermill": {
-     "duration": 0.010925,
-     "end_time": "2026-08-12T23:06:15.360107+00:00",
+     "duration": 0.02327,
+     "end_time": "2026-09-28T11:04:52.023340",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.349182+00:00",
+     "start_time": "2026-09-28T11:04:52.000070",
      "status": "completed"
     },
     "tags": []
@@ -200,7 +209,16 @@
   {
    "cell_type": "markdown",
    "id": "137659cb",
-   "metadata": {},
+   "metadata": {
+    "papermill": {
+     "duration": 0.001837,
+     "end_time": "2026-09-28T11:04:52.027211",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:52.025374",
+     "status": "completed"
+    },
+    "tags": []
+   },
    "source": [
     "**Lecture chiffree — la minimalite verifiee dans les DEUX sens.** Core rendu : `x_le_5`, `x_eq_10` — la section 3 montrera que la paire suffit. L'autre sens est tout aussi testable et complete la definition : chaque membre du core pris individuellement est NECESSAIRE. Retirer `x_le_5` : `{x>=3, x=10}` est satisfiable (`x = 10` verifie les deux). Retirer `x_eq_10` : `{x>=3, x<=5}` est satisfiable (tout `x` de 3 a 5). Aucune des deux ne peut partir — le core est irreductible dans les deux directions : suffisant (paire UNSAT) et necessaire (chaque retrait redevient SAT). C'est la definition complete du MUS que la section 7 formalisera, deja realisee ici sur un exemple ou l'ecart se voit a l'oeil nu : `x = 10` est a 5 unites de la borne `x <= 5`.\n"
    ]
@@ -210,10 +228,10 @@
    "id": "09c603eb",
    "metadata": {
     "papermill": {
-     "duration": 0.002956,
-     "end_time": "2026-08-12T23:06:15.366144+00:00",
+     "duration": 0.001764,
+     "end_time": "2026-09-28T11:04:52.030754",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.363188+00:00",
+     "start_time": "2026-09-28T11:04:52.028990",
      "status": "completed"
     },
     "tags": []
@@ -230,16 +248,16 @@
    "id": "a6875fcb",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.373250Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.372949Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.378486Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.377557Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.035315Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.035097Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.039730Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.039191Z"
     },
     "papermill": {
-     "duration": 0.010007,
-     "end_time": "2026-08-12T23:06:15.379137+00:00",
+     "duration": 0.007793,
+     "end_time": "2026-09-28T11:04:52.040432",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.369130+00:00",
+     "start_time": "2026-09-28T11:04:52.032639",
      "status": "completed"
     },
     "tags": []
@@ -276,10 +294,10 @@
    "id": "00135bd6",
    "metadata": {
     "papermill": {
-     "duration": 0.002851,
-     "end_time": "2026-08-12T23:06:15.385163+00:00",
+     "duration": 0.001865,
+     "end_time": "2026-09-28T11:04:52.044557",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.382312+00:00",
+     "start_time": "2026-09-28T11:04:52.042692",
      "status": "completed"
     },
     "tags": []
@@ -296,16 +314,16 @@
    "id": "54308055",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.392627Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.392385Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.399875Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.398975Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.049228Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.048945Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.054603Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.054201Z"
     },
     "papermill": {
-     "duration": 0.012231,
-     "end_time": "2026-08-12T23:06:15.400544+00:00",
+     "duration": 0.009211,
+     "end_time": "2026-09-28T11:04:52.055672",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.388313+00:00",
+     "start_time": "2026-09-28T11:04:52.046461",
      "status": "completed"
     },
     "tags": []
@@ -359,7 +377,16 @@
   {
    "cell_type": "markdown",
    "id": "8fad7629",
-   "metadata": {},
+   "metadata": {
+    "papermill": {
+     "duration": 0.002109,
+     "end_time": "2026-09-28T11:04:52.059871",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:52.057762",
+     "status": "completed"
+    },
+    "tags": []
+   },
    "source": [
     "**Lecture chiffree — les deux relachements ne coutent pas le meme prix.** `Sur 5 contraintes, 2 seulement sont en conflit` — mais les deux manieres de guerir ne sont pas equivalentes, et le systeme restant les chiffre. Les trois contraintes innocentes bornent `h` dans l'intervalle [9, 17], soit 17 - 9 + 1 = 9 valeurs entieres. Relacher `h=12` (garder la pause dejeuner) : 9 - 1 = 8 solutions restent. Relacher `h!=12` (garder la demande de l'animateur) : exactement 1 solution, `h = 12`. Le core dit QUELLES contraintes sont en conflit ; compter ce que chaque relachement laisse voir est le pas supplementaire qui transforme le diagnostic en decision — ici, l'option pause dejeuner preserve 8 des 9 plannings possibles, l'option animateur en fige un seul.\n"
    ]
@@ -369,10 +396,10 @@
    "id": "a578ceff",
    "metadata": {
     "papermill": {
-     "duration": 0.003235,
-     "end_time": "2026-08-12T23:06:15.407292+00:00",
+     "duration": 0.001798,
+     "end_time": "2026-09-28T11:04:52.063598",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.404057+00:00",
+     "start_time": "2026-09-28T11:04:52.061800",
      "status": "completed"
     },
     "tags": []
@@ -389,16 +416,16 @@
    "id": "fce97350",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.414974Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.414661Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.421779Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.420792Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.068190Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.067896Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.072824Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.072334Z"
     },
     "papermill": {
-     "duration": 0.011979,
-     "end_time": "2026-08-12T23:06:15.422498+00:00",
+     "duration": 0.00819,
+     "end_time": "2026-09-28T11:04:52.073601",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.410519+00:00",
+     "start_time": "2026-09-28T11:04:52.065411",
      "status": "completed"
     },
     "tags": []
@@ -429,239 +456,21 @@
     "print(\"UnsatCore = { %s }   (x>=0 exclu du core)\" % '  '.join(str(c) for c in core))\n"
    ]
   },
-  {
-   "cell_type": "markdown",
-   "id": "3d4c302c",
-   "metadata": {
-    "papermill": {
-     "duration": 0.003995,
-     "end_time": "2026-08-12T23:06:15.430017+00:00",
-     "exception": false,
-     "start_time": "2026-08-12T23:06:15.426022+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
-   "source": [
-    "## 6. Le vrai test : un core invisible a l'inspection\n",
-    "Les exemples precedents (sections 2 a 5) partagent une limite : dans chacun, le conflit est **visible a l'oeil nu** -- deux contraintes se contredisent textuellement (`h == 12` vs `h != 12`, `x == 1` vs `x == 2`). On n'a pas vraiment besoin de Z3 pour les isoler.\n",
-    "C'est la que `unsat_core()` devient precieux : sur un systeme ou **aucune paire** de contraintes ne se contredit, mais ou l'insatisfiabilite **emerge d'une combinaison**. Cas concret, un projet de planification : quatre taches $T_0, T_1, T_2, T_3$ s'enchainent (chacune doit finir avant que la suivante commence), chacune dure 2 unites, et tout doit etre termine avant la date 7. Aucune contrainte prise isolement n'est absurde -- et pourtant le systeme est insatisfiable. Lequel des 11 ingredients faut-il relacher ?"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 7,
-   "id": "991f21a8",
-   "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.438464Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.438080Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.447933Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.447243Z"
-    },
-    "papermill": {
-     "duration": 0.015145,
-     "end_time": "2026-08-12T23:06:15.448841+00:00",
-     "exception": false,
-     "start_time": "2026-08-12T23:06:15.433696+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Check : unsat\n",
-      "Core minimal = { release_T0  deadline_T3  precedence_T0_vers_T1  precedence_T1_vers_T2  precedence_T2_vers_T3 }\n",
-      "Taille du core : 5 contraintes sur 11\n",
-      "Contraintes innocentes ecartees (6) : deadline_T0, release_T1, deadline_T1, release_T2, deadline_T2, release_T3\n"
-     ]
-    }
-   ],
-   "source": [
-    "# Planification surcontrainte : 4 taches enchainees (T0->T1->T2->T3), duree 2 chacune,\n",
-    "# a finir avant la date 7. Aucune contrainte isolee n'est absurde -> conflit structurel.\n",
-    "s_start = [Int(f\"start_{i}\") for i in range(4)]\n",
-    "DUREE = 2\n",
-    "DATE_LIMITE = 7\n",
-    "s5 = Solver()\n",
-    "s5.set(\"unsat_core\", True)\n",
-    "labels = []\n",
-    "\n",
-    "def ajouter(constraint, nom):\n",
-    "    b = Bool(nom)\n",
-    "    s5.assert_and_track(constraint, b)\n",
-    "    labels.append(b)\n",
-    "    return b\n",
-    "\n",
-    "# Chaque tache : demarre apres 0 et finit avant la date limite\n",
-    "for i in range(4):\n",
-    "    ajouter(s_start[i] >= 0, f\"release_T{i}\")\n",
-    "    ajouter(s_start[i] + DUREE <= DATE_LIMITE, f\"deadline_T{i}\")\n",
-    "# Enchainement : Ti finit avant que Ti+1 commence\n",
-    "for i in range(3):\n",
-    "    ajouter(s_start[i] + DUREE <= s_start[i + 1], f\"precedence_T{i}_vers_T{i + 1}\")\n",
-    "\n",
-    "print(\"Check : %s\" % s5.check())\n",
-    "core = s5.unsat_core()\n",
-    "print(\"Core minimal = { %s }\" % \"  \".join(str(c) for c in core))\n",
-    "print(\"Taille du core : %d contraintes sur %d\" % (len(core), len(labels)))\n",
-    "innocentes = [str(b) for b in labels if b not in core]\n",
-    "print(\"Contraintes innocentes ecartees (%d) : %s\" % (len(innocentes), \", \".join(innocentes)))"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "21a44b5d",
-   "metadata": {},
-   "source": [
-    "### Lecture : le core isole la chaine, pas une paire\n",
-    "Le core minimal contient **5 contraintes sur 11** : le `release_T0` (point de depart), les **trois precedences** qui enchainent $T_0 \\to T_1 \\to T_2 \\to T_3$, et le `deadline_T3` (echeance finale). Les **6 autres** -- les bornes et echeances intermediaires `deadline_T0`, `release_T1`/`T2`/`T3`, `deadline_T1`/`T2` -- sont ecartees : la chaine les implique deja, elles ne sont pas necessaires au conflit.\n",
-    "Pourquoi ce core est **invisible a l'inspection** : aucune des 5 contraintes coupables ne contredit une autre textuellement. Il faut **tracer la chaine** -- `start_T0 >= 0`, puis `+2` a chaque precedence, donc `start_T1 >= 2`, `start_T2 >= 4`, `start_T3 >= 6`, puis `+2` de duree = `8 > 7` (la deadline) -- pour voir le conflit. Et ce core de 5 est le **SEUL possible** : retirer `release_T0` et la chaine flotte librement, retirer une precedence et la chaine se coupe, retirer `deadline_T3` et chaque echeance restante est tenable -- le core rendu n'est pas un choix parmi d'autres, c'est l'unique sous-ensemble irreductible, et les 6 contraintes ecartees le sont a bon droit.\n",
-    "C'est precisement le travail fastidieux qu'evite `unsat_core()` : parmi 11 contraintes, il isole chirurgicalement les 5 qui forment la preuve d'insatisfiabilite.\n"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "ce9a1526",
-   "metadata": {
-    "papermill": {
-     "duration": 0.003341,
-     "end_time": "2026-08-12T23:06:15.462975+00:00",
-     "exception": false,
-     "start_time": "2026-08-12T23:06:15.459634+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
-   "source": [
-    "## 7. Au-dela du core : le MUS (Minimal Unsatisfiable Subset)\n",
-    "\n",
-    "Jusqu'ici, on a fait confiance a `unsat_core()` pour renvoyer un sous-ensemble\n",
-    "**minimal** de contraintes. Mais Z3 ne le **garantit pas** : le core est\n",
-    "*un sous-ensemble responsable du conflit*, pas necessairement le plus petit.\n",
-    "Sur l'arithmetique lineaire simple, Z3 minimise souvent bien ; sur des modeles\n",
-    "plus riches (graphe de precedences, contraintes transitives), il peut laisser\n",
-    "des contraintes **redundantes** dans le core.\n",
-    "\n",
-    "Le **MUS** (Minimal Unsatisfiable Subset) est le sous-ensemble *irreductible* :\n",
-    "retirer n'importe laquelle de ses contraintes rend le systeme **satisfiable**.\n",
-    "L'algorithme **deletion-based** est simple et garantit cette irreductibilite :\n",
-    "on retire les contraintes une a une, et si le systeme reste UNSAT sans l'une\n",
-    "d'elles, c'est qu'elle etait superflue — on la supprime definitivement.\n"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 8,
-   "id": "0fb398d7",
-   "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.471562Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.471339Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.485281Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.484463Z"
-    },
-    "papermill": {
-     "duration": 0.019092,
-     "end_time": "2026-08-12T23:06:15.485857+00:00",
-     "exception": false,
-     "start_time": "2026-08-12T23:06:15.466765+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "Ordonnancement : unsat\n",
-      "Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5\n",
-      "MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3\n",
-      "Contraintes redundantes eliminees : ['e01', 'e12', 'e23']\n",
-      "-> Le core de Z3 (taille 5) n'etait PAS minimal : le MUS est de taille 3.\n"
-     ]
-    }
-   ],
-   "source": [
-    "from z3 import *\n",
-    "\n",
-    "def compute_mus(constraints):\n",
-    "    \"\"\"MUS deletion-based : sous-ensemble irreductible rendant le systeme UNSAT.\n",
-    "\n",
-    "    constraints : liste de couples (formule, etiquette Bool).\n",
-    "    Renvoie le plus petit sous-ensemble tel qu'aucune contrainte ne puisse\n",
-    "    etre retiree sans rendre le systeme satisfiable.\"\"\"\n",
-    "    mus = list(constraints)\n",
-    "    i = 0\n",
-    "    while i < len(mus):\n",
-    "        candidat = mus[:i] + mus[i+1:]          # mus sans la contrainte i\n",
-    "        s = Solver(); s.set(\"unsat_core\", True)\n",
-    "        for formule, etiquette in candidat:\n",
-    "            s.assert_and_track(formule, etiquette)\n",
-    "        if s.check() == unsat:\n",
-    "            mus = candidat                       # reste UNSAT -> i etait superflue\n",
-    "        else:\n",
-    "            i += 1                                # i est essentielle -> on la garde\n",
-    "    return mus\n",
-    "\n",
-    "# Ordonnancement de taches : 5 taches t0..t4 avec precedences (durees) + deadline.\n",
-    "# Les aretes transitives (ex. t0 -> t3) rendent certaines contraintes redondantes.\n",
-    "t = [Int('t%d' % k) for k in range(5)]\n",
-    "precedences = [\n",
-    "    (t[1] >= t[0] + 5,  Bool('e01')),   # t0 -> t1 (duree 5)\n",
-    "    (t[2] >= t[1] + 3,  Bool('e12')),   # t1 -> t2 (duree 3)\n",
-    "    (t[3] >= t[2] + 4,  Bool('e23')),   # t2 -> t3 (duree 4)\n",
-    "    (t[3] >= t[0] + 12, Bool('e03')),   # t0 -> t3 transitif (5+3+4 = 12)\n",
-    "    (t[4] >= t[3] + 2,  Bool('e34')),   # t3 -> t4 (duree 2)\n",
-    "    (t[4] <= t[0] + 10, Bool('dead')),  # deadline : chemin total = 14 > 10 -> UNSAT\n",
-    "]\n",
-    "\n",
-    "# Core brut de Z3\n",
-    "s_core = Solver(); s_core.set(\"unsat_core\", True)\n",
-    "for f, e in precedences:\n",
-    "    s_core.assert_and_track(f, e)\n",
-    "print(\"Ordonnancement :\", s_core.check())\n",
-    "core_z3 = [str(c) for c in s_core.unsat_core()]\n",
-    "print(\"Core Z3 (brut) :\", sorted(core_z3), \"- taille\", len(core_z3))\n",
-    "\n",
-    "# MUS irreductible\n",
-    "mus = compute_mus(precedences)\n",
-    "mus_labels = sorted(str(e) for f, e in mus)\n",
-    "print(\"MUS (irreductible) :\", mus_labels, \"- taille\", len(mus_labels))\n",
-    "print(\"Contraintes redundantes eliminees :\", sorted(set(core_z3) - set(mus_labels)))\n",
-    "print(\"-> Le core de Z3 (taille %d) n'etait PAS minimal : le MUS est de taille %d.\" % (len(core_z3), len(mus_labels)))\n"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "3c987bed",
-   "metadata": {},
-   "source": [
-    "**Lecture chiffree — deux preuves differentes du meme UNSAT.** `Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5` puis `MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3`. Regarder les etiquettes, pas seulement les tailles : le core brut contient le chemin DETAILLE t0->t1->t2->t3, le MUS contient l'arete TRANSITIVE `e03` — absente du core. Z3 refute en descendant la chaine (5+3+4 = 12, puis +2 = 14, contre la borne de 10) ; l'algorithme deletion-based trouve le raccourci et rend une preuve 40 % plus courte (3 contraintes contre 5).\n",
-    "**Pourquoi le core n'etait pas minimal.** Les aretes `e01`, `e12`, `e23` (le chemin t0->t1->t2->t3) sont **impliquees** par l'arete transitive `e03` (t0->t3, de duree cumulee 12). Z3 les a inclues dans son core parce qu'elles participent a la refutation, mais elles sont *logiquement superflues* des que `e03` est presente. Le MUS les ecarte et ne garde que l'irreductible : `e03` + `e34` + `dead` (la deadline que les 14 unites de chemin total violent).\n",
-    "**Le MUS n'est pas forcement unique — et le core depend du chemin de refutation.** Un systeme peut contenir **plusieurs** sous-ensembles minimaux distincts. Si l'on a trois paires de contraintes independantes chacune contradictoire (`{A,B}`, `{C,D}`, `{E,F}`), chacune est un MUS valide de taille 2. `unsat_core()` en renvoie **un** ; l'algorithme deletion-based en renvoie un **autre** selon l'ordre de suppression — avant de s'appuyer sur UN core pour relacher une contrainte, savoir qu'un autre existait, plus petit. C'est la limite du core unique : il diagnostique **un** conflit, pas **tous** les conflits minimaux (les enumerer tous est un probleme distinct, dit *MUS enumeration*, nettement plus couteux).\n",
-    "**Pont avec les sections precedentes.** Le `unsat_core()` (sections 2-6) repond : *ces contraintes suffisent au conflit*. Le MUS repond plus fort : *aucune d'elles ne peut etre retiree*. Sur un modele ou l'on veut **corriger** la specification (relacher la bonne contrainte), c'est le MUS — pas le core brut — qui indique exactement les frontieres du conflit irreductible.\n"
-   ]
-  },
   {
    "cell_type": "markdown",
    "id": "f30db165",
    "metadata": {
     "papermill": {
-     "duration": 0.003089,
-     "end_time": "2026-08-12T23:06:15.499456+00:00",
+     "duration": 0.001988,
+     "end_time": "2026-09-28T11:04:52.077621",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.496367+00:00",
+     "start_time": "2026-09-28T11:04:52.075633",
      "status": "completed"
     },
     "tags": []
    },
    "source": [
-    "## 8. Ce que ce notebook a demontre\n",
+    "## 6. Ce que ce notebook a demontre\n",
     "\n",
     "Trois lecons sur le noyau d'insatisfiabilite :\n",
     "1. **Du verdict a l'explication** - `unsat` dit *qu'il n'y a pas* de solution ; `unsat_core()` dit *pourquoi* (lesquelles contraintes conflictuent).\n",
@@ -672,8 +481,6 @@
     "\n",
     "\n",
     "\n",
-    "4. **La ou ca compte** - sur un systeme ou aucun conflit n'est visible a l'oeil (section 6), le core isole la combinaison coupable parmi de nombreuses contraintes innocentes -- c'est la que le diagnostic devient indispensable, pas decoratif.\n",
-    "\n",
     "\n",
     "\n",
     "Cette capacite d'explication distingue un solveur d'un simple oracle booléen : il ne dit pas seulement *non*, il dit *a cause de quoi*."
@@ -684,16 +491,16 @@
    "id": "0a3b9d82",
    "metadata": {
     "papermill": {
-     "duration": 0.00342,
-     "end_time": "2026-08-12T23:06:15.505894+00:00",
+     "duration": 0.001871,
+     "end_time": "2026-09-28T11:04:52.081489",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.502474+00:00",
+     "start_time": "2026-09-28T11:04:52.079618",
      "status": "completed"
     },
     "tags": []
    },
    "source": [
-    "## 9. Exercices\n",
+    "## 7. Exercices\n",
     "\n",
     "Les trois exercices ci-dessous vous font manipuler le UNSAT core sur des variantes : conflit cache parmi 4 contraintes (1), planning avec relachement (2), core minimal parmi 10 (3). Chaque stub est self-contained : les fonctions (`Int`, `Bool`, `Solver`, `assert_and_track`) sont définies dans les sections précédentes."
    ]
@@ -703,10 +510,10 @@
    "id": "b2f2760f",
    "metadata": {
     "papermill": {
-     "duration": 0.002983,
-     "end_time": "2026-08-12T23:06:15.512100+00:00",
+     "duration": 0.002167,
+     "end_time": "2026-09-28T11:04:52.085514",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.509117+00:00",
+     "start_time": "2026-09-28T11:04:52.083347",
      "status": "completed"
     },
     "tags": []
@@ -720,20 +527,20 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 7,
    "id": "0ce4d320",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.519645Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.519348Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.523243Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.522514Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.090537Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.090170Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.093428Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.093004Z"
     },
     "papermill": {
-     "duration": 0.00855,
-     "end_time": "2026-08-12T23:06:15.523821+00:00",
+     "duration": 0.006933,
+     "end_time": "2026-09-28T11:04:52.094479",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.515271+00:00",
+     "start_time": "2026-09-28T11:04:52.087546",
      "status": "completed"
     },
     "tags": []
@@ -762,10 +569,10 @@
    "id": "c5ee334f",
    "metadata": {
     "papermill": {
-     "duration": 0.003084,
-     "end_time": "2026-08-12T23:06:15.530212+00:00",
+     "duration": 0.00201,
+     "end_time": "2026-09-28T11:04:52.098641",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.527128+00:00",
+     "start_time": "2026-09-28T11:04:52.096631",
      "status": "completed"
     },
     "tags": []
@@ -779,20 +586,20 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 8,
    "id": "b81d82df",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.538000Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.537800Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.541607Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.540893Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.103533Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.103315Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.106543Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.105983Z"
     },
     "papermill": {
-     "duration": 0.008936,
-     "end_time": "2026-08-12T23:06:15.542218+00:00",
+     "duration": 0.006679,
+     "end_time": "2026-09-28T11:04:52.107322",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.533282+00:00",
+     "start_time": "2026-09-28T11:04:52.100643",
      "status": "completed"
     },
     "tags": []
@@ -821,10 +628,10 @@
    "id": "7a7d11cd",
    "metadata": {
     "papermill": {
-     "duration": 0.003167,
-     "end_time": "2026-08-12T23:06:15.548622+00:00",
+     "duration": 0.002016,
+     "end_time": "2026-09-28T11:04:52.111444",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.545455+00:00",
+     "start_time": "2026-09-28T11:04:52.109428",
      "status": "completed"
     },
     "tags": []
@@ -838,20 +645,20 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 9,
    "id": "784a1255",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-08-12T23:06:15.556423Z",
-     "iopub.status.busy": "2026-08-12T23:06:15.556200Z",
-     "iopub.status.idle": "2026-08-12T23:06:15.560164Z",
-     "shell.execute_reply": "2026-08-12T23:06:15.559482Z"
+     "iopub.execute_input": "2026-09-28T11:04:52.116341Z",
+     "iopub.status.busy": "2026-09-28T11:04:52.116143Z",
+     "iopub.status.idle": "2026-09-28T11:04:52.119390Z",
+     "shell.execute_reply": "2026-09-28T11:04:52.118985Z"
     },
     "papermill": {
-     "duration": 0.008892,
-     "end_time": "2026-08-12T23:06:15.560862+00:00",
+     "duration": 0.006694,
+     "end_time": "2026-09-28T11:04:52.120135",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.551970+00:00",
+     "start_time": "2026-09-28T11:04:52.113441",
      "status": "completed"
     },
     "tags": []
@@ -880,10 +687,10 @@
    "id": "c1c75dde",
    "metadata": {
     "papermill": {
-     "duration": 0.003437,
-     "end_time": "2026-08-12T23:06:15.567645+00:00",
+     "duration": 0.002147,
+     "end_time": "2026-09-28T11:04:52.124578",
      "exception": false,
-     "start_time": "2026-08-12T23:06:15.564208+00:00",
+     "start_time": "2026-09-28T11:04:52.122431",
      "status": "completed"
     },
     "tags": []
@@ -892,7 +699,9 @@
     "## Conclusion\n",
     "Le UNSAT core transforme le solveur d'oracle binaire en **outil de diagnostic**. La ou `unsat` dit seulement ' impossible ', `unsat_core()` dit ' impossible **a cause de ces contraintes-la** ' - le sous-ensemble minimal responsible du conflit. Sur une specification surcontrainte, ce diagnostic est directement actionnable : il pointe la contrainte a relacher.\n",
     "\n",
-    "Cette serie Z3-Python (notebooks 01 a 13) couvre maintenant les **trois postures** du solveur : **decider** (sat/unsat, 01-11), **optimiser** (Optimize, 06/08), et ici **expliquer** (unsat_core, 13). La ou l'ingenieur classique debug a l'aveugle un système insatisfiable, le solveur SMT isole chirurgicalement la cause - la différence entre un oracle et un partenaire de raisonnement."
+    "Cette serie Z3-Python (notebooks 01 a 13) couvre maintenant les **trois postures** du solveur : **decider** (sat/unsat, 01-11), **optimiser** (Optimize, 06/08), et ici **expliquer** (unsat_core, 13). La ou l'ingenieur classique debug a l'aveugle un système insatisfiable, le solveur SMT isole chirurgicalement la cause - la différence entre un oracle et un partenaire de raisonnement.\n",
+    "\n",
+    "Le compagnon [Z3-13b - le MUS](Z3-13b-UnsatCores-MUS-Python.ipynb) approfondit ce langage : core invisible a l'inspection, minimalite non garantie par Z3, et l'algorithme deletion-based qui calcule le sous-ensemble irreductible.\n"
    ]
   }
  ],
@@ -930,21 +739,21 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.13.7"
+   "version": "3.13.3"
   },
   "papermill": {
    "default_parameters": {},
-   "duration": 3.790079,
-   "end_time": "2026-08-12T23:06:15.815585+00:00",
+   "duration": 2.346237,
+   "end_time": "2026-09-28T11:04:52.367363",
    "environment_variables": {},
    "exception": null,
    "input_path": "Z3-13-UnsatCores-Python.ipynb",
    "output_path": "Z3-13-UnsatCores-Python.ipynb",
    "parameters": {},
-   "start_time": "2026-08-12T23:06:12.025506+00:00",
+   "start_time": "2026-09-28T11:04:50.021126",
    "version": "2.7.0"
   }
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}
\ No newline at end of file
diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb
new file mode 100644
index 0000000000..60263cdffd
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb
@@ -0,0 +1,589 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "nav-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001844,
+     "end_time": "2026-09-28T11:04:55.546515",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.544671",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "← [13 - UNSAT cores](Z3-13-UnsatCores-Python.ipynb) | [README Z3-Python](README.md)\n",
+    "\n",
+    "# Z3-Python-13b — UNSAT cores : le MUS (sous-ensemble irréductible)\n",
+    "\n",
+    "*Compagnon « preuve minimale » du module [Z3-Python-13 — UNSAT cores](Z3-13-UnsatCores-Python.ipynb).*\n",
+    "\n",
+    "Le notebook [13](Z3-13-UnsatCores-Python.ipynb) a établi le **noyau d'insatisfiabilité** (core) : `assert_and_track` étiquette chaque contrainte, `unsat_core()` isole celles qui conflitent. Ce compagnon 13b pousse là où le 13 s'arrête : d'abord un système où le conflit est **invisible à l'inspection** (aucune paire ne se contredit, l'insatisfiabilité émerge d'une combinaison), ensuite la limite de `unsat_core()` — Z3 ne garantit **pas** la minimalité — et l'algorithme **deletion-based** qui calcule le **MUS** (Minimal Unsatisfiable Subset) : le sous-ensemble *irréductible*, dont retirer n'importe quelle contrainte rend le système satisfiable.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "imports-13b",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.550229Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.550007Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.576326Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.575835Z"
+    },
+    "papermill": {
+     "duration": 0.029259,
+     "end_time": "2026-09-28T11:04:55.577274",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.548015",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [],
+   "source": [
+    "from z3 import *\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "s1-md-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001589,
+     "end_time": "2026-09-28T11:04:55.580489",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.578900",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "## 1. Le vrai test : un core invisible a l'inspection\n",
+    "\n",
+    "Les exemples du notebook [13 - UNSAT cores](Z3-13-UnsatCores-Python.ipynb) (sections 2 a 5) partagent une limite : dans chacun, le conflit est **visible a l'oeil nu** -- deux contraintes se contredisent textuellement (`h == 12` vs `h != 12`, `x == 1` vs `x == 2`). On n'a pas vraiment besoin de Z3 pour les isoler.\n",
+    "\n",
+    "C'est la que `unsat_core()` devient precieux : sur un systeme ou **aucune paire** de contraintes ne se contredit, mais ou l'insatisfiabilite **emerge d'une combinaison**. Cas concret, un projet de planification : quatre taches $T_0, T_1, T_2, T_3$ s'enchainent (chacune doit finir avant que la suivante commence), chacune dure 2 unites, et tout doit etre termine avant la date 7. Aucune contrainte prise isolement n'est absurde -- et pourtant le systeme est insatisfiable. Lequel des 11 ingredients faut-il relacher ?"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "991f21a8",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.584384Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.584140Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.600253Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.599747Z"
+    },
+    "papermill": {
+     "duration": 0.018992,
+     "end_time": "2026-09-28T11:04:55.601042",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.582050",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Check : unsat\n",
+      "Core minimal = { release_T0  deadline_T3  precedence_T0_vers_T1  precedence_T1_vers_T2  precedence_T2_vers_T3 }\n",
+      "Taille du core : 5 contraintes sur 11\n",
+      "Contraintes innocentes ecartees (6) : deadline_T0, release_T1, deadline_T1, release_T2, deadline_T2, release_T3\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Planification surcontrainte : 4 taches enchainees (T0->T1->T2->T3), duree 2 chacune,\n",
+    "# a finir avant la date 7. Aucune contrainte isolee n'est absurde -> conflit structurel.\n",
+    "s_start = [Int(f\"start_{i}\") for i in range(4)]\n",
+    "DUREE = 2\n",
+    "DATE_LIMITE = 7\n",
+    "s5 = Solver()\n",
+    "s5.set(\"unsat_core\", True)\n",
+    "labels = []\n",
+    "\n",
+    "def ajouter(constraint, nom):\n",
+    "    b = Bool(nom)\n",
+    "    s5.assert_and_track(constraint, b)\n",
+    "    labels.append(b)\n",
+    "    return b\n",
+    "\n",
+    "# Chaque tache : demarre apres 0 et finit avant la date limite\n",
+    "for i in range(4):\n",
+    "    ajouter(s_start[i] >= 0, f\"release_T{i}\")\n",
+    "    ajouter(s_start[i] + DUREE <= DATE_LIMITE, f\"deadline_T{i}\")\n",
+    "# Enchainement : Ti finit avant que Ti+1 commence\n",
+    "for i in range(3):\n",
+    "    ajouter(s_start[i] + DUREE <= s_start[i + 1], f\"precedence_T{i}_vers_T{i + 1}\")\n",
+    "\n",
+    "print(\"Check : %s\" % s5.check())\n",
+    "core = s5.unsat_core()\n",
+    "print(\"Core minimal = { %s }\" % \"  \".join(str(c) for c in core))\n",
+    "print(\"Taille du core : %d contraintes sur %d\" % (len(core), len(labels)))\n",
+    "innocentes = [str(b) for b in labels if b not in core]\n",
+    "print(\"Contraintes innocentes ecartees (%d) : %s\" % (len(innocentes), \", \".join(innocentes)))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "21a44b5d",
+   "metadata": {
+    "papermill": {
+     "duration": 0.00157,
+     "end_time": "2026-09-28T11:04:55.604345",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.602775",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "### Lecture : le core isole la chaine, pas une paire\n",
+    "\n",
+    "Le core minimal contient **5 contraintes sur 11** : le `release_T0` (point de depart), les **trois precedences** qui enchainent $T_0 \\to T_1 \\to T_2 \\to T_3$, et le `deadline_T3` (echeance finale). Les **6 autres** -- les bornes et echeances intermediaires `deadline_T0`, `release_T1`/`T2`/`T3`, `deadline_T1`/`T2` -- sont ecartees : la chaine les implique deja, elles ne sont pas necessaires au conflit.\n",
+    "\n",
+    "Pourquoi ce core est **invisible a l'inspection** : aucune des 5 contraintes coupables ne contredit une autre textuellement. Il faut **tracer la chaine** -- `start_T0 >= 0`, puis `+2` a chaque precedence, donc `start_T1 >= 2`, `start_T2 >= 4`, `start_T3 >= 6`, puis `+2` de duree = `8 > 7` (la deadline) -- pour voir le conflit. Et ce core de 5 est le **SEUL possible** : retirer `release_T0` et la chaine flotte librement, retirer une precedence et la chaine se coupe, retirer `deadline_T3` et chaque echeance restante est tenable -- le core rendu n'est pas un choix parmi d'autres, c'est l'unique sous-ensemble irreductible, et les 6 contraintes ecartees le sont a bon droit.\n",
+    "\n",
+    "C'est precisement le travail fastidieux qu'evite `unsat_core()` : parmi 11 contraintes, il isole chirurgicalement les 5 qui forment la preuve d'insatisfiabilite.\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "s2-md-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.00141,
+     "end_time": "2026-09-28T11:04:55.607184",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.605774",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "## 2. Au-dela du core : le MUS (Minimal Unsatisfiable Subset)\n",
+    "\n",
+    "Jusqu'ici, on a fait confiance a `unsat_core()` pour renvoyer un sous-ensemble\n",
+    "**minimal** de contraintes. Mais Z3 ne le **garantit pas** : le core est\n",
+    "*un sous-ensemble responsable du conflit*, pas necessairement le plus petit.\n",
+    "Sur l'arithmetique lineaire simple, Z3 minimise souvent bien ; sur des modeles\n",
+    "plus riches (graphe de precedences, contraintes transitives), il peut laisser\n",
+    "des contraintes **redundantes** dans le core.\n",
+    "\n",
+    "Le **MUS** (Minimal Unsatisfiable Subset) est le sous-ensemble *irreductible* :\n",
+    "retirer n'importe laquelle de ses contraintes rend le systeme **satisfiable**.\n",
+    "L'algorithme **deletion-based** est simple et garantit cette irreductibilite :\n",
+    "on retire les contraintes une a une, et si le systeme reste UNSAT sans l'une\n",
+    "d'elles, c'est qu'elle etait superflue — on la supprime definitivement.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "0fb398d7",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.610850Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.610649Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.622713Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.622084Z"
+    },
+    "papermill": {
+     "duration": 0.014917,
+     "end_time": "2026-09-28T11:04:55.623490",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.608573",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Ordonnancement : unsat\n",
+      "Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5\n",
+      "MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3\n",
+      "Contraintes redundantes eliminees : ['e01', 'e12', 'e23']\n",
+      "-> Le core de Z3 (taille 5) n'etait PAS minimal : le MUS est de taille 3.\n"
+     ]
+    }
+   ],
+   "source": [
+    "from z3 import *\n",
+    "\n",
+    "def compute_mus(constraints):\n",
+    "    \"\"\"MUS deletion-based : sous-ensemble irreductible rendant le systeme UNSAT.\n",
+    "\n",
+    "    constraints : liste de couples (formule, etiquette Bool).\n",
+    "    Renvoie le plus petit sous-ensemble tel qu'aucune contrainte ne puisse\n",
+    "    etre retiree sans rendre le systeme satisfiable.\"\"\"\n",
+    "    mus = list(constraints)\n",
+    "    i = 0\n",
+    "    while i < len(mus):\n",
+    "        candidat = mus[:i] + mus[i+1:]          # mus sans la contrainte i\n",
+    "        s = Solver(); s.set(\"unsat_core\", True)\n",
+    "        for formule, etiquette in candidat:\n",
+    "            s.assert_and_track(formule, etiquette)\n",
+    "        if s.check() == unsat:\n",
+    "            mus = candidat                       # reste UNSAT -> i etait superflue\n",
+    "        else:\n",
+    "            i += 1                                # i est essentielle -> on la garde\n",
+    "    return mus\n",
+    "\n",
+    "# Ordonnancement de taches : 5 taches t0..t4 avec precedences (durees) + deadline.\n",
+    "# Les aretes transitives (ex. t0 -> t3) rendent certaines contraintes redondantes.\n",
+    "t = [Int('t%d' % k) for k in range(5)]\n",
+    "precedences = [\n",
+    "    (t[1] >= t[0] + 5,  Bool('e01')),   # t0 -> t1 (duree 5)\n",
+    "    (t[2] >= t[1] + 3,  Bool('e12')),   # t1 -> t2 (duree 3)\n",
+    "    (t[3] >= t[2] + 4,  Bool('e23')),   # t2 -> t3 (duree 4)\n",
+    "    (t[3] >= t[0] + 12, Bool('e03')),   # t0 -> t3 transitif (5+3+4 = 12)\n",
+    "    (t[4] >= t[3] + 2,  Bool('e34')),   # t3 -> t4 (duree 2)\n",
+    "    (t[4] <= t[0] + 10, Bool('dead')),  # deadline : chemin total = 14 > 10 -> UNSAT\n",
+    "]\n",
+    "\n",
+    "# Core brut de Z3\n",
+    "s_core = Solver(); s_core.set(\"unsat_core\", True)\n",
+    "for f, e in precedences:\n",
+    "    s_core.assert_and_track(f, e)\n",
+    "print(\"Ordonnancement :\", s_core.check())\n",
+    "core_z3 = [str(c) for c in s_core.unsat_core()]\n",
+    "print(\"Core Z3 (brut) :\", sorted(core_z3), \"- taille\", len(core_z3))\n",
+    "\n",
+    "# MUS irreductible\n",
+    "mus = compute_mus(precedences)\n",
+    "mus_labels = sorted(str(e) for f, e in mus)\n",
+    "print(\"MUS (irreductible) :\", mus_labels, \"- taille\", len(mus_labels))\n",
+    "print(\"Contraintes redundantes eliminees :\", sorted(set(core_z3) - set(mus_labels)))\n",
+    "print(\"-> Le core de Z3 (taille %d) n'etait PAS minimal : le MUS est de taille %d.\" % (len(core_z3), len(mus_labels)))\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3c987bed",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001763,
+     "end_time": "2026-09-28T11:04:55.629006",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.627243",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "**Lecture chiffree — deux preuves differentes du meme UNSAT.** `Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5` puis `MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3`. Regarder les etiquettes, pas seulement les tailles : le core brut contient le chemin DETAILLE t0->t1->t2->t3, le MUS contient l'arete TRANSITIVE `e03` — absente du core. Z3 refute en descendant la chaine (5+3+4 = 12, puis +2 = 14, contre la borne de 10) ; l'algorithme deletion-based trouve le raccourci et rend une preuve 40 % plus courte (3 contraintes contre 5).\n",
+    "\n",
+    "**Pourquoi le core n'etait pas minimal.** Les aretes `e01`, `e12`, `e23` (le chemin t0->t1->t2->t3) sont **impliquees** par l'arete transitive `e03` (t0->t3, de duree cumulee 12). Z3 les a inclues dans son core parce qu'elles participent a la refutation, mais elles sont *logiquement superflues* des que `e03` est presente. Le MUS les ecarte et ne garde que l'irreductible : `e03` + `e34` + `dead` (la deadline que les 14 unites de chemin total violent).\n",
+    "\n",
+    "**Le MUS n'est pas forcement unique — et le core depend du chemin de refutation.** Un systeme peut contenir **plusieurs** sous-ensembles minimaux distincts. Si l'on a trois paires de contraintes independantes chacune contradictoire (`{A,B}`, `{C,D}`, `{E,F}`), chacune est un MUS valide de taille 2. `unsat_core()` en renvoie **un** ; l'algorithme deletion-based en renvoie un **autre** selon l'ordre de suppression — avant de s'appuyer sur UN core pour relacher une contrainte, savoir qu'un autre existait, plus petit. C'est la limite du core unique : il diagnostique **un** conflit, pas **tous** les conflits minimaux (les enumerer tous est un probleme distinct, dit *MUS enumeration*, nettement plus couteux).\n",
+    "\n",
+    "**Pont avec les sections precedentes.** Le `unsat_core()` (sections 2-6) repond : *ces contraintes suffisent au conflit*. Le MUS repond plus fort : *aucune d'elles ne peut etre retiree*. Sur un modele ou l'on veut **corriger** la specification (relacher la bonne contrainte), c'est le MUS — pas le core brut — qui indique exactement les frontieres du conflit irreductible.\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "recap-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001393,
+     "end_time": "2026-09-28T11:04:55.631847",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.630454",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "## 3. Ce que ce notebook a demontre\n",
+    "\n",
+    "Trois lecons au-dela du core brut :\n",
+    "1. **Là où ça compte** - sur un système où aucun conflit n'est visible à l'œil (section 1), le core isole la combinaison coupable parmi de nombreuses contraintes innocentes -- c'est là que le diagnostic devient indispensable, pas décoratif.\n",
+    "\n",
+    "2. **Irréductibilité** - le MUS est le sous-ensemble dont **chaque** membre est essentiel : le retirer rend le système satisfiable. L'algorithme deletion-based le garantit constructivement, là où le core brut de Z3 peut contenir des contraintes redondantes.\n",
+    "\n",
+    "3. **Deux preuves du même UNSAT** - le core brut et le MUS sont deux refutations différentes de la même insatisfiabilité ; le MUS est la plus courte (section 2 : 5 contraintes contre 3, l'arête transitive remplaçant le chemin détaillé). Comparer les deux, c'est mesurer à quel point un diagnostic peut être resserré.\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ex-intro-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001346,
+     "end_time": "2026-09-28T11:04:55.634582",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.633236",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "## 4. Exercices\n",
+    "\n",
+    "Les trois exercices vous font manipuler le MUS sur des variantes : irréductibilité vérifiée membre par membre (1), arête transitive contre chemin détaillé (2), diagnostic actionnable par le MUS (3). La fonction `compute_mus` est définie à la section 2 ; les stubs sont self-contained.\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ex1-md-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001355,
+     "end_time": "2026-09-28T11:04:55.637345",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.635990",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "### Exercice 1 - Irréductibilité vérifiée membre par membre\n",
+    "Construisez 8 contraintes sur `w` : 3 en conflit de chaîne (ex : `w >= 0`, `w >= 4`, `w + 4 <= 6`, `w == 5`) plus 4 compatibles (`w <= 100`, `w != 7`, etc.). Calculez le MUS avec `compute_mus`, puis vérifiez la propriété définitoire : retirer **une à une** chaque contrainte du MUS et re-checker — chaque sous-ensemble doit être **SATISFIABLE**.\n",
+    "\n",
+    "**Étapes** : 8 `assert_and_track` étiquetés ; boucle sur le résultat de `compute_mus` ; pour chaque membre, `check()` sur les autres seuls -> `sat` attendu.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "id": "ex1-code-13b",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.641115Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.640817Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.644275Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.643774Z"
+    },
+    "papermill": {
+     "duration": 0.006724,
+     "end_time": "2026-09-28T11:04:55.645435",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.638711",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Exercice 1 a completer : verifiez que chaque membre du MUS est essentiel\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Exercice 1 : irreductibilite verifiee membre par membre\n",
+    "# TODO etudiant :\n",
+    "# Etape 1 : w = Int('w') ; 8 contraintes etiquetees (chaine en conflit + compatibles)\n",
+    "# Etape 2 : mus = compute_mus(couples) -> sous-ensemble irreductible\n",
+    "# Etape 3 : pour chaque (formule, etiquette) du MUS : re-check SANS elle -> sat attendu\n",
+    "result = None  # TODO etudiant\n",
+    "print(\"Exercice 1 a completer : verifiez que chaque membre du MUS est essentiel\")\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ex2-md-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001476,
+     "end_time": "2026-09-28T11:04:55.648435",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.646959",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "### Exercice 2 - Arête transitive contre chemin détaillé\n",
+    "Encodez 3 tâches `t0, t1, t2` (durée 2) en chaîne `t0 -> t1 -> t2` **plus** l'arête transitive directe `t0 -> t2`, avec une échéance qui rend le tout insatisfiable. Comparez la **taille du core brut** (`unsat_core()`) et la **taille du MUS** : le MUS doit écarter le chemin détaillé au profit de l'arête transitive.\n",
+    "\n",
+    "**Étapes** : `assert_and_track` pour chaque arête + échéance ; `len(unsat_core())` vs `len(compute_mus(...))` -> le MUS est plus court.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "id": "ex2-code-13b",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.652413Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.652070Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.655104Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.654565Z"
+    },
+    "papermill": {
+     "duration": 0.005882,
+     "end_time": "2026-09-28T11:04:55.655858",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.649976",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Exercice 2 a completer : comparez |core brut| et |MUS| sur le meme systeme\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Exercice 2 : arete transitive contre chemin detaille\n",
+    "# TODO etudiant :\n",
+    "# Etape 1 : start_0/1/2 = Int ; duree 2 ; aretes t0->t1, t1->t2 ET transitive t0->t2, echeance\n",
+    "# Etape 2 : s.check() + s.unsat_core() -> taille du core brut\n",
+    "# Etape 3 : compute_mus sur les memes couples -> taille du MUS (plus petite)\n",
+    "taille_mus = None  # TODO etudiant\n",
+    "print(\"Exercice 2 a completer : comparez |core brut| et |MUS| sur le meme systeme\")\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ex3-md-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.001573,
+     "end_time": "2026-09-28T11:04:55.659150",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.657577",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "### Exercice 3 - Diagnostic : laquelle relâcher, décidé par le MUS\n",
+    "Construisez une spécification surcontrainte sur `h` où le core brut contient ~5 contraintes mais où le MUS en isole 2. Relâchez **une seule** contrainte du MUS, re-checkez : le système devient **SATISFIABLE** — preuve que le MUS, pas le core brut, désigne le relâchement minimal.\n",
+    "\n",
+    "**Étapes** : encoder la spécification étiquetée ; `compute_mus` ; retirer un membre du MUS ; re-`check()` -> `sat`.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "id": "ex3-code-13b",
+   "metadata": {
+    "execution": {
+     "iopub.execute_input": "2026-09-28T11:04:55.663491Z",
+     "iopub.status.busy": "2026-09-28T11:04:55.663130Z",
+     "iopub.status.idle": "2026-09-28T11:04:55.666355Z",
+     "shell.execute_reply": "2026-09-28T11:04:55.665890Z"
+    },
+    "papermill": {
+     "duration": 0.006585,
+     "end_time": "2026-09-28T11:04:55.667277",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.660692",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Exercice 3 a completer : relachez une contrainte du MUS et re-checkez\n"
+     ]
+    }
+   ],
+   "source": [
+    "# Exercice 3 : diagnostic actionnable, decide par le MUS\n",
+    "# TODO etudiant :\n",
+    "# Etape 1 : spec surcontrainte sur h etiquetee (core brut ~5 contraintes)\n",
+    "# Etape 2 : mus = compute_mus(...) -> isole 2 contraintes essentielles\n",
+    "# Etape 3 : retirer UNE contrainte du MUS, re-check -> sat (systeme reparable d'un geste)\n",
+    "result = None  # TODO etudiant\n",
+    "print(\"Exercice 3 a completer : relachez une contrainte du MUS et re-checkez\")\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "conclusion-13b",
+   "metadata": {
+    "papermill": {
+     "duration": 0.002313,
+     "end_time": "2026-09-28T11:04:55.671681",
+     "exception": false,
+     "start_time": "2026-09-28T11:04:55.669368",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "## Conclusion\n",
+    "Le MUS referme l'arc ouvert par le [13](Z3-13-UnsatCores-Python.ipynb) : là où `unsat_core()` rend le conflit **visible**, le MUS le rend **irréductible** — la preuve la plus courte qu'aucune contrainte ne puisse être retirée sans faire disparaître le conflit. Sur une spécification surcontrainte, c'est le diagnostic ultime : non seulement *quelles* contraintes conflitent, mais *lesquelles relâcher au strict minimum*.\n",
+    "\n",
+    "La série poursuit avec [Z3-14 - Bit-vectors](Z3-14-BitVectors-Overflow-Python.ipynb) : l'arithmétique bornée des machines, où le débordement devient une propriété décidable — et se prouve.\n"
+   ]
+  }
+ ],
+ "metadata": {
+  "cost": {
+   "api_provider": "none",
+   "api_usd_est": 0.0,
+   "cpu_min": 1,
+   "external_account": false,
+   "free_alternative": "self",
+   "gpu_min": 0,
+   "gpu_required": false,
+   "metadata_written": "2026-08-03",
+   "network": true,
+   "notes": "Z3 unsat-core extraction. Deterministic SMT. CPU-only. 10/10 cells executed.",
+   "qcc_tokens_est": 0,
+   "reduced_pedagogical": false,
+   "reproducibility": "HIGH",
+   "validator": "check_cost_metadata.py",
+   "vram_gb": 0,
+   "vram_tier": "none"
+  },
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.13.3"
+  },
+  "papermill": {
+   "default_parameters": {},
+   "duration": 2.096466,
+   "end_time": "2026-09-28T11:04:55.903141",
+   "environment_variables": {},
+   "exception": null,
+   "input_path": "Z3-13b-UnsatCores-MUS-Python.ipynb",
+   "output_path": "Z3-13b-UnsatCores-MUS-Python.ipynb",
+   "parameters": {},
+   "start_time": "2026-09-28T11:04:53.806675",
+   "version": "2.7.0"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
\ No newline at end of file
diff --git a/_quarto.yml b/_quarto.yml
index 7ea0bc057b..f3df8bfbee 100644
--- a/_quarto.yml
+++ b/_quarto.yml
@@ -1198,6 +1198,7 @@ project:
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-11-Graph-Coloring-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb"
+    - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-15-Nested-Arrays-2D-Python.ipynb"
     - "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16b-Meal-Planner-Data-External-Python.ipynb"
diff --git a/docs/curriculum/ia-symbolique.md b/docs/curriculum/ia-symbolique.md
index 1fcbe7ad47..e179feaf1f 100644
--- a/docs/curriculum/ia-symbolique.md
+++ b/docs/curriculum/ia-symbolique.md
@@ -216,23 +216,24 @@ Preuves formelles en Lean 4, logique probabiliste avec Tweety, web sémantique,
 | 26 | [Z3-Python 17 — Théorie des tableaux : Select, Store et…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-17-Array-Theory-Python.ipynb) | BETA | Oui |
 | 27 | [Z3-Python 18 — Sudoku 4x4 : comparaison des modes Array…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-18-Sudoku-Modes-Python.ipynb) | BETA | Oui |
 | 28 | [13. UNSAT cores : expliquer l'insatisfiabilite (le '…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb) | BETA | Oui |
-| 29 | [LINQ to Z3 - Résolution de Contraintes Déclarative](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/01_Linq2Z3_Intro.ipynb) | BETA | Oui |
-| 30 | [Sudoku : Théorème Explicite vs Modèle Implicite par…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/02_Sudoku_Theorem_vs_Array.ipynb) | BETA | Oui |
-| 31 | [Sudoku 4x4 : comparaison des modes Array et Constants](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/03_Sudoku_Modes_Comparison.ipynb) | BETA | Oui |
-| 32 | [Théorie des Tableaux Z3 — Select, Store et Switching](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/04_Array_Theory.ipynb) | BETA | Oui |
-| 33 | [Tableaux Imbriqués et Grilles 2D : API Déclarative…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/05_Nested_Arrays_2D.ipynb) | BETA | Oui |
-| 34 | [Notebook 06 — Meal-Planner declaratif : du modèle Z3 au…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb) | BETA | Oui |
-| 35 | [07 — Données réelles & externe : Ciqual × RecipeML…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/07_Meal_Planner_Data_External.ipynb) | BETA | Oui |
-| 36 | [08 — Capstone hiérarchique : du squelette int\[\]\[\] réel…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb) | BETA | Oui |
-| 37 | [09 — Convergence à l'échelle : l'encodage décide de la…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb) | BETA | Oui |
-| 38 | [10 — Générer un témoin depuis A & ~B (fork Automata…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/10_Witness_Generation_Automata.ipynb) | BETA | Oui |
-| 39 | [Notebook 11 — Ordonnancement d'atelier (Job Shop…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/11_Job_Shop_Scheduling.ipynb) | BETA | Oui |
-| 40 | [Notebook 12 - Coloration de graphe : le graphe de…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/12_Graph_Coloring_Petersen.ipynb) | BETA | Oui |
-| 41 | [Notebook 13 — Cryptarithmes : l'arithmétique…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/13_Cryptarithmetic_SMT.ipynb) | BETA | Oui |
-| 42 | [Notebook 14 — De SAT à OPT : optimisation et…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/14_Optimize_MaxSAT.ipynb) | BETA | Oui |
-| 43 | [15 — Théorie des bit-vectors Z3 : vérifier le…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/15_BitVectors_Overflow.ipynb) | BETA | Oui |
-| 44 | [17 — UNSAT cores Z3 : expliquer l'insatisfiabilité (le…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/17_UnsatCores.ipynb) | BETA | Oui |
-| 45 | [Notebook 18 - L'enigme d'Einstein : la logique des…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/18_Einsteins_Riddle.ipynb) | BETA | Oui |
+| 29 | [Z3-Python-13b — UNSAT cores : le MUS (sous-ensemble irreductible)](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb) | BETA | Oui |
+| 30 | [LINQ to Z3 - Résolution de Contraintes Déclarative](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/01_Linq2Z3_Intro.ipynb) | BETA | Oui |
+| 31 | [Sudoku : Théorème Explicite vs Modèle Implicite par…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/02_Sudoku_Theorem_vs_Array.ipynb) | BETA | Oui |
+| 32 | [Sudoku 4x4 : comparaison des modes Array et Constants](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/03_Sudoku_Modes_Comparison.ipynb) | BETA | Oui |
+| 33 | [Théorie des Tableaux Z3 — Select, Store et Switching](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/04_Array_Theory.ipynb) | BETA | Oui |
+| 34 | [Tableaux Imbriqués et Grilles 2D : API Déclarative…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/05_Nested_Arrays_2D.ipynb) | BETA | Oui |
+| 35 | [Notebook 06 — Meal-Planner declaratif : du modèle Z3 au…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb) | BETA | Oui |
+| 36 | [07 — Données réelles & externe : Ciqual × RecipeML…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/07_Meal_Planner_Data_External.ipynb) | BETA | Oui |
+| 37 | [08 — Capstone hiérarchique : du squelette int\[\]\[\] réel…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb) | BETA | Oui |
+| 38 | [09 — Convergence à l'échelle : l'encodage décide de la…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb) | BETA | Oui |
+| 39 | [10 — Générer un témoin depuis A & ~B (fork Automata…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/10_Witness_Generation_Automata.ipynb) | BETA | Oui |
+| 40 | [Notebook 11 — Ordonnancement d'atelier (Job Shop…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/11_Job_Shop_Scheduling.ipynb) | BETA | Oui |
+| 41 | [Notebook 12 - Coloration de graphe : le graphe de…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/12_Graph_Coloring_Petersen.ipynb) | BETA | Oui |
+| 42 | [Notebook 13 — Cryptarithmes : l'arithmétique…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/13_Cryptarithmetic_SMT.ipynb) | BETA | Oui |
+| 43 | [Notebook 14 — De SAT à OPT : optimisation et…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/14_Optimize_MaxSAT.ipynb) | BETA | Oui |
+| 44 | [15 — Théorie des bit-vectors Z3 : vérifier le…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/15_BitVectors_Overflow.ipynb) | BETA | Oui |
+| 45 | [17 — UNSAT cores Z3 : expliquer l'insatisfiabilité (le…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/17_UnsatCores.ipynb) | BETA | Oui |
+| 46 | [Notebook 18 - L'enigme d'Einstein : la logique des…](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/18_Einsteins_Riddle.ipynb) | BETA | Oui |
 
 ## SymbolicAI/SemanticWeb (28 notebooks)
 
diff --git a/docs/curriculum/symbolic-formalization.md b/docs/curriculum/symbolic-formalization.md
index a2b3780329..3337e42850 100644
--- a/docs/curriculum/symbolic-formalization.md
+++ b/docs/curriculum/symbolic-formalization.md
@@ -138,7 +138,7 @@ dans un solveur SOTA (Microsoft Research). Sélection dans la série
 | 14 | [Z3-Python-04-Strings-Regex](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-04-Strings-Regex-Python.ipynb) | 30 min | théorie des chaînes et regex symboliques → étape 11 |
 | 15 | [Z3-Python-05-Quantifiers-Proofs](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-05-Quantifiers-Proofs-Python.ipynb) | 30 min | quantificateurs, **preuves** — vers le bloc 4 → étape 2 (FOL) |
 | 16 | [Z3-Python-06-Advanced-Optimization](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-Python.ipynb) | 30 min | Optimize, soft constraints → étape 13 |
-| 17 | [Z3-13-UnsatCores-Python](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb) | 30 min | cœurs insatisfaisables — écho des MUS de l'étape 4 → étape 4 |
+| 17 | [Z3-13-UnsatCores-Python](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb) + [13b — le MUS](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb) | 30 min | cœurs insatisfaisables, MUS par deletion-based (13b) — écho des MUS de l'étape 4 → étape 4 |
 | 18 | [Z3-Python-16-Meal-Planner](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16-Meal-Planner-Python.ipynb) | 30 min | **capstone** : optimisation sous contraintes réelles → étapes 12+16 |
 
 ### Bloc 3 — Planification (étapes 19-25, 4 h 45)
diff --git a/scripts/tests/baseline_nb_nav_chain.json b/scripts/tests/baseline_nb_nav_chain.json
index ddd3e41aee..91d6aa85b2 100644
--- a/scripts/tests/baseline_nb_nav_chain.json
+++ b/scripts/tests/baseline_nb_nav_chain.json
@@ -1910,6 +1910,11 @@
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-CSharp.ipynb",
       "series": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API"
     },
+    {
+      "kind": "orphan_entry",
+      "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb",
+      "series": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API"
+    },
     {
       "kind": "orphan_entry",
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb",
diff --git a/slides/03-logique/slides.md b/slides/03-logique/slides.md
index 880221a528..4d17a65f9a 100644
--- a/slides/03-logique/slides.md
+++ b/slides/03-logique/slides.md
@@ -1478,7 +1478,7 @@ h2 { margin-top: 0.3em !important; margin-bottom: 0.1em !important; }
 - Debloquer une configuration industrielle : le solveur dit UNSAT, quelle contrainte relacher ?
 - Revision des croyances : quelle croyance retirer pour rester coherent (postulats AGM)
 
-*Notebooks : [Z3-13-UnsatCores-Python](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb) (noyaux d'insatisfiabilite) · [17_UnsatCores](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/17_UnsatCores.ipynb) · [Tweety-4-Belief-Revision](../../MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-4-Belief-Revision.ipynb) (MUS, MCS, dualite).*
+*Notebooks : [Z3-13-UnsatCores-Python](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb) (noyaux d'insatisfiabilite) · [Z3-13b-UnsatCores-MUS-Python](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb) (MUS par deletion-based) · [17_UnsatCores](../../MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/17_UnsatCores.ipynb) · [Tweety-4-Belief-Revision](../../MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-4-Belief-Revision.ipynb) (MUS, MCS, dualite).*
 
 ---
 layout: default