fix(notebooks,#17550): tranche 14/16 Z3-Python-13-UnsatCores -- 6 cellules MD newlines doublage

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb

@@ -15,13 +15,9 @@
    },
    "source": [
     "← [12 - Arithmetique reelle](Z3-12-Real-Arithmetic-Python.ipynb) | [README Z3-Python](README.md)\n",
-    "\n",
     "# 13. UNSAT cores : expliquer l'insatisfiabilite (le ' pourquoi ')\n",
-    "\n",
     "Jusqu'ici, le solveur repondait a une question binaire : *ce système a-t-il une solution ?* -> **SAT** (oui, voici un temoin) ou **UNSAT** (non, prouve impossible). C'est un **verdict**, pas une **explication**.\n",
-    "\n",
     "Pour un ingenieur qui **ecrit** la specification, UNSAT est souvent un bug de modelisation : une contrainte trop forte, ou deux contraintes incompatibles. La reponse ' impossible ' ne suffit pas - il faut savoir **lesquelles** des contraintes se contredisent. C'est le rôle du **noyau d'insatisfiabilite** (UNSAT core) : le sous-ensemble **minimal** de contraintes responsable du conflit. Z3 passe du diagnostic binaire au diagnostic chirurgical.\n",
-    "\n",
     "> Port pyz3 du notebook C# [`17_UnsatCores.ipynb`](../Z3-Linq2Z3/17_UnsatCores.ipynb). EPIC #1206, Prong B. (Le bloc DSL `Explain()` du C#, spécifique a Z3.Linq, n'est pas porte ; l'API brute `assert_and_track` + `unsat_core` de pyz3 fait le même travail.)"
    ]
   },
@@ -142,9 +138,7 @@
    },
    "source": [
     "## 2. L'API `assert_and_track` : etiqueter chaque contrainte\n",
-    "\n",
     "Pour obtenir une explication, on fournit les contraintes comme des **hypothese traceables** : `s.assert_and_track(formule, etiquette)` ou `etiquette` est un `Bool` servant de nom. Après un `unsat`, `s.unsat_core()` renvoie le sous-ensemble **minimal** d'etiquettes responsable du conflit.\n",
-    "\n",
     "Trois contraintes sur `x` : `x >= 3`, `x <= 5`, `x = 10`. Lesquelles se contredisent ?"
    ]
   },
@@ -385,9 +379,7 @@
    },
    "source": [
     "## 5. Innocence prouvee : une contrainte non impliquee ecartee du core\n",
-    "\n",
     "Un dernier temoin de la minimalite : sur un système a 3 contraintes (`x == 1`, `x >= 0` innocente, `x == 2`), le core minimal est `{x==1, x==2}`. La contrainte `x >= 0` est **compatible** avec les deux (un x valant 1 ou 2 verifie x >= 0) - elle n'est pas impliquee dans le conflit, donc Z3 l'ecarte du core. C'est ce qui distingue le core d'une simple liste de contraintes : il isole la **cause**, pas le contexte.\n",
-    "\n",
     "> Note port : le notebook C# original compare ici l'API brute (`Check(assumptions)` + `UnsatCore`) avec le DSL Z3.Linq (`Explain()`). Le DSL n'existe pas en pyz3 - l'API brute `assert_and_track` + `unsat_core` est l'equivalent direct, et c'est elle que cette section demontre."
    ]
   },
@@ -452,9 +444,7 @@
    },
    "source": [
     "## 6. Le vrai test : un core invisible a l'inspection\n",
-    "\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",
-    "\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 ?"
    ]
   },
@@ -528,13 +518,9 @@
    "metadata": {},
    "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"
+    "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"
    ]
   },
   {
@@ -656,13 +642,9 @@
    "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",
-    "\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"
+    "**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"
    ]
   },
   {