diff --git a/MyIA.AI.Notebooks/GameTheory/SocialChoice/04-Computational-Aggregation-SAT-Z3-Csharp.ipynb b/MyIA.AI.Notebooks/GameTheory/SocialChoice/04-Computational-Aggregation-SAT-Z3-Csharp.ipynb index fd7ba25a7c..fc26e9bd77 100644 --- a/MyIA.AI.Notebooks/GameTheory/SocialChoice/04-Computational-Aggregation-SAT-Z3-Csharp.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/SocialChoice/04-Computational-Aggregation-SAT-Z3-Csharp.ipynb @@ -3,7 +3,16 @@ { "cell_type": "markdown", "id": "35fbfe8e", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.00639, + "end_time": "2026-10-03T06:38:22.142955+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:22.136565+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "# SocialChoice 04 : Agregation Computationnelle - SAT et DPLL (twin C# .NET)\n", "\n", @@ -22,7 +31,16 @@ { "cell_type": "markdown", "id": "44399c4e", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.00506, + "end_time": "2026-10-03T06:38:22.153964+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:22.148904+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "## 0. Configuration\n", "\n", @@ -35,24 +53,142 @@ "id": "caae5054", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:27.167349Z", - "iopub.status.busy": "2026-08-17T12:18:27.162394Z", - "iopub.status.idle": "2026-08-17T12:18:28.279242Z", - "shell.execute_reply": "2026-08-17T12:18:28.276806Z" - } + "iopub.execute_input": "2026-10-03T06:38:22.174451Z", + "iopub.status.busy": "2026-10-03T06:38:22.168482Z", + "iopub.status.idle": "2026-10-03T06:38:23.672663Z", + "shell.execute_reply": "2026-10-03T06:38:23.668012Z" + }, + "papermill": { + "duration": 1.51482, + "end_time": "2026-10-03T06:38:23.672829+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:22.158009+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "" + "text/html": [ + "\r\n", + "
\r\n", + " \r\n", + " \r\n", + "
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "Configuration OK : SocialChoice 04 - SAT et DPLL (twin C# .NET)\r\n" + "output_type": "stream", + "text": [ + "Configuration OK : SocialChoice 04 - SAT et DPLL (twin C# .NET)\n" + ] } ], "source": [ @@ -73,7 +209,16 @@ { "cell_type": "markdown", "id": "e55a9e7d", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004109, + "end_time": "2026-10-03T06:38:23.681666+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:23.677557+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -91,7 +236,16 @@ { "cell_type": "markdown", "id": "55364027", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.003803, + "end_time": "2026-10-03T06:38:23.689443+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:23.685640+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "### 1.1 Solveur DPLL from-scratch\n", "\n", @@ -110,11 +264,19 @@ "id": "3b4fa15e", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:28.280754Z", - "iopub.status.busy": "2026-08-17T12:18:28.280527Z", - "iopub.status.idle": "2026-08-17T12:18:28.544739Z", - "shell.execute_reply": "2026-08-17T12:18:28.544505Z" - } + "iopub.execute_input": "2026-10-03T06:38:23.699642Z", + "iopub.status.busy": "2026-10-03T06:38:23.699369Z", + "iopub.status.idle": "2026-10-03T06:38:24.070234Z", + "shell.execute_reply": "2026-10-03T06:38:24.070058Z" + }, + "papermill": { + "duration": 0.376581, + "end_time": "2026-10-03T06:38:24.070345+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:23.693764+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [], "source": [ @@ -227,7 +389,16 @@ { "cell_type": "markdown", "id": "96ab14e7", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004647, + "end_time": "2026-10-03T06:38:24.079874+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.075227+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "### 1.2 Premier exemple : verification SAT\n", "\n", @@ -244,52 +415,76 @@ "id": "3129f116", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:28.546356Z", - "iopub.status.busy": "2026-08-17T12:18:28.546083Z", - "iopub.status.idle": "2026-08-17T12:18:28.837375Z", - "shell.execute_reply": "2026-08-17T12:18:28.837016Z" - } + "iopub.execute_input": "2026-10-03T06:38:24.089849Z", + "iopub.status.busy": "2026-10-03T06:38:24.089660Z", + "iopub.status.idle": "2026-10-03T06:38:24.473088Z", + "shell.execute_reply": "2026-10-03T06:38:24.472946Z" + }, + "papermill": { + "duration": 0.389387, + "end_time": "2026-10-03T06:38:24.473171+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.083784+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Formule : (x1 v x2) ^ (~x1 v x3) ^ (~x2 v ~x3)\r\n" + "output_type": "stream", + "text": [ + "Formule : (x1 v x2) ^ (~x1 v x3) ^ (~x2 v ~x3)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Resultat : SAT\r\n" + "output_type": "stream", + "text": [ + "Resultat : SAT\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Modele : " + "output_type": "stream", + "text": [ + "Modele : " + ] }, { - "output_type": "stream", "name": "stdout", - "text": "x1=True, x2=False, x3=True\r\n" + "output_type": "stream", + "text": [ + "x1=True, x2=False, x3=True\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Verification des modeles possibles :\r\n" + "output_type": "stream", + "text": [ + "Verification des modeles possibles :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " x1=False, x2=True, x3=False : SATISFAIT\r\n" + "output_type": "stream", + "text": [ + " x1=False, x2=True, x3=False : SATISFAIT\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " x1=True, x2=False, x3=True : SATISFAIT\r\n" + "output_type": "stream", + "text": [ + " x1=True, x2=False, x3=True : SATISFAIT\n" + ] } ], "source": [ @@ -328,7 +523,16 @@ { "cell_type": "markdown", "id": "f33e2670", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.003703, + "end_time": "2026-10-03T06:38:24.481026+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.477323+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interpretation.** Le solveur DPLL trouve un modèle satisfaisant. L'enumeration manuelle confirme qu'il existe plusieurs affectations valides (par exemple $x_1=F, x_2=T, x_3=F$)." ] @@ -336,7 +540,16 @@ { "cell_type": "markdown", "id": "4dbb5095", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.003521, + "end_time": "2026-10-03T06:38:24.488103+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.484582+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "### 1.3 Exemple UNSAT\n", "\n", @@ -349,27 +562,41 @@ "id": "480f83bc", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:28.838796Z", - "iopub.status.busy": "2026-08-17T12:18:28.838591Z", - "iopub.status.idle": "2026-08-17T12:18:28.883726Z", - "shell.execute_reply": "2026-08-17T12:18:28.883524Z" - } + "iopub.execute_input": "2026-10-03T06:38:24.497563Z", + "iopub.status.busy": "2026-10-03T06:38:24.497342Z", + "iopub.status.idle": "2026-10-03T06:38:24.567705Z", + "shell.execute_reply": "2026-10-03T06:38:24.567536Z" + }, + "papermill": { + "duration": 0.076073, + "end_time": "2026-10-03T06:38:24.567793+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.491720+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Formule : (x1) ^ (~x1)\r\n" + "output_type": "stream", + "text": [ + "Formule : (x1) ^ (~x1)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Resultat : UNSAT\r\n" + "output_type": "stream", + "text": [ + "Resultat : UNSAT\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "L'unite propagation force x1=true (clause 1) puis detecte le conflit (clause 2 falsifiee).\r\n" + "output_type": "stream", + "text": [ + "L'unite propagation force x1=true (clause 1) puis detecte le conflit (clause 2 falsifiee).\n" + ] } ], "source": [ @@ -388,7 +615,16 @@ { "cell_type": "markdown", "id": "f92b5011", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004592, + "end_time": "2026-10-03T06:38:24.577204+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.572612+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -409,32 +645,48 @@ "id": "1f687b50", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:28.885314Z", - "iopub.status.busy": "2026-08-17T12:18:28.885019Z", - "iopub.status.idle": "2026-08-17T12:18:29.103600Z", - "shell.execute_reply": "2026-08-17T12:18:29.103403Z" - } + "iopub.execute_input": "2026-10-03T06:38:24.588749Z", + "iopub.status.busy": "2026-10-03T06:38:24.588468Z", + "iopub.status.idle": "2026-10-03T06:38:24.835749Z", + "shell.execute_reply": "2026-10-03T06:38:24.835588Z" + }, + "papermill": { + "duration": 0.253843, + "end_time": "2026-10-03T06:38:24.835839+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.581996+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Encodage Arrow (3 alt, 2 voters)\r\n" + "output_type": "stream", + "text": [ + "Encodage Arrow (3 alt, 2 voters)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Profils : 36\r\n" + "output_type": "stream", + "text": [ + " Profils : 36\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Variables : 216\r\n" + "output_type": "stream", + "text": [ + " Variables : 216\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Clauses : 2216\r\n" + "output_type": "stream", + "text": [ + " Clauses : 2216\n" + ] } ], "source": [ @@ -617,7 +869,16 @@ { "cell_type": "markdown", "id": "c5ecdc99", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004507, + "end_time": "2026-10-03T06:38:24.845239+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.840732+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interpretation de l'encodage.** Pour 3 alternatives et 2 votants, l'encodage genere **216 variables** booleennes (36 profils x 6 paires ordonnees) et un peu plus de **2200 clauses** reparties sur les 6 familles d'axiomes. C'est un problème SAT de taille modeste, bien dans la portee de DPLL." ] @@ -625,7 +886,16 @@ { "cell_type": "markdown", "id": "207140f7", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004534, + "end_time": "2026-10-03T06:38:24.854610+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.850076+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -640,67 +910,97 @@ "id": "074f0fcd", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.104953Z", - "iopub.status.busy": "2026-08-17T12:18:29.104754Z", - "iopub.status.idle": "2026-08-17T12:18:29.174299Z", - "shell.execute_reply": "2026-08-17T12:18:29.174054Z" - } + "iopub.execute_input": "2026-10-03T06:38:24.865721Z", + "iopub.status.busy": "2026-10-03T06:38:24.865567Z", + "iopub.status.idle": "2026-10-03T06:38:24.915869Z", + "shell.execute_reply": "2026-10-03T06:38:24.915718Z" + }, + "papermill": { + "duration": 0.056946, + "end_time": "2026-10-03T06:38:24.915945+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.858999+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "VERIFICATION DU THEOREME D'ARROW PAR DPLL\r\n" + "output_type": "stream", + "text": [ + "VERIFICATION DU THEOREME D'ARROW PAR DPLL\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "==================================================\r\n" + "output_type": "stream", + "text": [ + "==================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Configuration : 3 alternatives, 2 votants\r\n" + "output_type": "stream", + "text": [ + "Configuration : 3 alternatives, 2 votants\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " DPLL (from-scratch) : UNSAT (Arrow verifie)\r\n" + "output_type": "stream", + "text": [ + " DPLL (from-scratch) : UNSAT (Arrow verifie)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 216 variables, 2216 clauses, 36 profils\r\n" + "output_type": "stream", + "text": [ + " 216 variables, 2216 clauses, 36 profils\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Temps : 0.00 s\r\n" + "output_type": "stream", + "text": [ + " Temps : 0.00 s\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Resultat : UNSAT\r\n" + "output_type": "stream", + "text": [ + "Resultat : UNSAT\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Aucune SWF ne peut satisfaire Pareto + IIA + non-dictature\r\n" + "output_type": "stream", + "text": [ + "=> Aucune SWF ne peut satisfaire Pareto + IIA + non-dictature\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Le theoreme d'Arrow est mecaniquement verifie\r\n" + "output_type": "stream", + "text": [ + "=> Le theoreme d'Arrow est mecaniquement verifie\n" + ] } ], "source": [ @@ -736,7 +1036,16 @@ { "cell_type": "markdown", "id": "14fc44c7", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004834, + "end_time": "2026-10-03T06:38:24.925757+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.920923+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interpretation.** DPLL confirme **UNSAT** : aucune affectation des 216 variables ne satisfait simultanement les 6 familles de clauses. Le theoreme d'Arrow est prouve par exhaustion mecanique (elaguee par unit propagation).\n", "\n", @@ -746,7 +1055,16 @@ { "cell_type": "markdown", "id": "3022782f", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004581, + "end_time": "2026-10-03T06:38:24.935041+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.930460+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -761,102 +1079,146 @@ "id": "3e23fc63", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.175677Z", - "iopub.status.busy": "2026-08-17T12:18:29.175475Z", - "iopub.status.idle": "2026-08-17T12:18:29.234550Z", - "shell.execute_reply": "2026-08-17T12:18:29.234357Z" - } + "iopub.execute_input": "2026-10-03T06:38:24.946418Z", + "iopub.status.busy": "2026-10-03T06:38:24.946238Z", + "iopub.status.idle": "2026-10-03T06:38:24.996273Z", + "shell.execute_reply": "2026-10-03T06:38:24.996129Z" + }, + "papermill": { + "duration": 0.056678, + "end_time": "2026-10-03T06:38:24.996353+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:24.939675+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "CAS 2 ALTERNATIVES : ANALYSE DE L'ENCODAGE\r\n" + "output_type": "stream", + "text": [ + "CAS 2 ALTERNATIVES : ANALYSE DE L'ENCODAGE\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "==================================================\r\n" + "output_type": "stream", + "text": [ + "==================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Profils : 4\r\n" + "output_type": "stream", + "text": [ + " Profils : 4\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Variables : 8\r\n" + "output_type": "stream", + "text": [ + " Variables : 8\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Clauses : 12\r\n" + "output_type": "stream", + "text": [ + " Clauses : 12\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Resultat : SAT\r\n" + "output_type": "stream", + "text": [ + " Resultat : SAT\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Analyse :\r\n" + "output_type": "stream", + "text": [ + "Analyse :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " L'encodage SAT trouve SAT pour 2 alternatives.\r\n" + "output_type": "stream", + "text": [ + " L'encodage SAT trouve SAT pour 2 alternatives.\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Une SWF non dictatoriale existe (regle majoritaire).\r\n" + "output_type": "stream", + "text": [ + " Une SWF non dictatoriale existe (regle majoritaire).\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " - Pareto + IIA + non-dictature sont compatibles des que |A| < 3\r\n" + "output_type": "stream", + "text": [ + " - Pareto + IIA + non-dictature sont compatibles des que |A| < 3\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " - IIA : le classement social d'une paire ne depend que des\r\n" + "output_type": "stream", + "text": [ + " - IIA : le classement social d'une paire ne depend que des\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " preferences individuelles sur cette paire (une seule paire ici)\r\n" + "output_type": "stream", + "text": [ + " preferences individuelles sur cette paire (une seule paire ici)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " - Aucun electeur ne peut etre dictateur au sens d'Arrow\r\n" + "output_type": "stream", + "text": [ + " - Aucun electeur ne peut etre dictateur au sens d'Arrow\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Note : le theoreme d'Arrow classique suppose |A| >= 3.\r\n" + "output_type": "stream", + "text": [ + " Note : le theoreme d'Arrow classique suppose |A| >= 3.\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Le cas |A| = 2 est en dessous de la frontiere d'impossibilite :\r\n" + "output_type": "stream", + "text": [ + " Le cas |A| = 2 est en dessous de la frontiere d'impossibilite :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " la conclusion d'Arrow ne s'applique pas, et SAT est correct.\r\n" + "output_type": "stream", + "text": [ + " la conclusion d'Arrow ne s'applique pas, et SAT est correct.\n" + ] } ], "source": [ @@ -896,7 +1258,16 @@ { "cell_type": "markdown", "id": "0bd07dde", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.004308, + "end_time": "2026-10-03T06:38:25.005443+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.001135+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -917,7 +1288,16 @@ { "cell_type": "markdown", "id": "sen-tranche2-0", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.005085, + "end_time": "2026-10-03T06:38:25.015060+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.009975+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "## 5. Theoreme de Sen : un autre angle d'impossibilite\n", "\n", @@ -932,47 +1312,69 @@ "id": "sen-tranche2-1", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.235856Z", - "iopub.status.busy": "2026-08-17T12:18:29.235669Z", - "iopub.status.idle": "2026-08-17T12:18:29.356633Z", - "shell.execute_reply": "2026-08-17T12:18:29.356350Z" - } + "iopub.execute_input": "2026-10-03T06:38:25.026915Z", + "iopub.status.busy": "2026-10-03T06:38:25.026705Z", + "iopub.status.idle": "2026-10-03T06:38:25.143813Z", + "shell.execute_reply": "2026-10-03T06:38:25.143665Z" + }, + "papermill": { + "duration": 0.123975, + "end_time": "2026-10-03T06:38:25.143908+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.019933+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "ENCODAGE DU THEOREME DE SEN (3 alt, 2 voters)\r\n" + "output_type": "stream", + "text": [ + "ENCODAGE DU THEOREME DE SEN (3 alt, 2 voters)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Variables : 216\r\n" + "output_type": "stream", + "text": [ + " Variables : 216\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Clauses : 558\r\n" + "output_type": "stream", + "text": [ + " Clauses : 558\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Pairs de liberte: voter0->(A,C), voter1->(B,C)\r\n" + "output_type": "stream", + "text": [ + " Pairs de liberte: voter0->(A,C), voter1->(B,C)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Resultat DPLL : UNSAT (Sen verifie) en 0.1 ms\r\n" + "output_type": "stream", + "text": [ + "Resultat DPLL : UNSAT (Sen verifie) en 0.1 ms\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Liberte minimale + Pareto + transitivite = IMPOSSIBLE (theoreme de Sen)\r\n" + "output_type": "stream", + "text": [ + "=> Liberte minimale + Pareto + transitivite = IMPOSSIBLE (theoreme de Sen)\n" + ] } ], "source": [ @@ -1115,7 +1517,16 @@ { "cell_type": "markdown", "id": "sen-tranche2-2", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.005399, + "end_time": "2026-10-03T06:38:25.154568+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.149169+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interpretation du theoreme de Sen.** L'encodage produit **moins de clauses** que celui d'Arrow (transitivite + Pareto + liberte remplacent IIA + non-dictature qui sont quadratiques en profils). Le résultat UNSAT confirme le theoreme : on ne peut pas avoir simultanement le respect des droits individuels minimaux, l'efficacite collective (Pareto) et la coherence du classement social (transitivite).\n", "\n", @@ -1125,7 +1536,16 @@ { "cell_type": "markdown", "id": "sen-tranche2-3", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.005264, + "end_time": "2026-10-03T06:38:25.165064+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.159800+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -1140,67 +1560,97 @@ "id": "sen-tranche2-4", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.358170Z", - "iopub.status.busy": "2026-08-17T12:18:29.357923Z", - "iopub.status.idle": "2026-08-17T12:18:29.444088Z", - "shell.execute_reply": "2026-08-17T12:18:29.443859Z" - } + "iopub.execute_input": "2026-10-03T06:38:25.179056Z", + "iopub.status.busy": "2026-10-03T06:38:25.178874Z", + "iopub.status.idle": "2026-10-03T06:38:25.238129Z", + "shell.execute_reply": "2026-10-03T06:38:25.237979Z" + }, + "papermill": { + "duration": 0.067929, + "end_time": "2026-10-03T06:38:25.238208+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.170279+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "BENCHMARK STRUCTUREL : ARROW vs SEN (3 alt, 2 voters)\r\n" + "output_type": "stream", + "text": [ + "BENCHMARK STRUCTUREL : ARROW vs SEN (3 alt, 2 voters)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "==========================================================\r\n" + "output_type": "stream", + "text": [ + "==========================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Theoreme Profils Vars Clauses Verdict DPLL(ms)\r\n" + "output_type": "stream", + "text": [ + " Theoreme Profils Vars Clauses Verdict DPLL(ms)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "----------------------------------------------------------\r\n" + "output_type": "stream", + "text": [ + "----------------------------------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Arrow 36 216 2216 UNSAT (Arrow) 1.1\r\n" + "output_type": "stream", + "text": [ + " Arrow 36 216 2216 UNSAT (Arrow) 1.4\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Sen 36 216 558 UNSAT (Sen) 0.0\r\n" + "output_type": "stream", + "text": [ + " Sen 36 216 558 UNSAT (Sen) 0.1\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Ratio clauses Arrow/Sen : 4.0x\r\n" + "output_type": "stream", + "text": [ + "Ratio clauses Arrow/Sen : 4.0x\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Sen remplace IIA (quadratique en profils) + non-dictature par une seule\r\n" + "output_type": "stream", + "text": [ + "=> Sen remplace IIA (quadratique en profils) + non-dictature par une seule\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " contrainte de liberte lineaire => encodage beaucoup plus compact.\r\n" + "output_type": "stream", + "text": [ + " contrainte de liberte lineaire => encodage beaucoup plus compact.\n" + ] } ], "source": [ @@ -1237,7 +1687,16 @@ { "cell_type": "markdown", "id": "sen-tranche2-5", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.005319, + "end_time": "2026-10-03T06:38:25.249150+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.243831+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Analyse du benchmark structurel.**\n", "\n", @@ -1255,7 +1714,16 @@ { "cell_type": "markdown", "id": "z3-tranche3-0", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.005322, + "end_time": "2026-10-03T06:38:25.260078+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.254756+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -1265,7 +1733,9 @@ "\n", "L'avantage du SMT : les contraintes d'**ordre total** (transitivite, antisymetrie) decoulent naturellement de la théorie des entiers, sans avoir a les enumerer en clauses CNF. Z3 resout le système par son solveur SMT, plus puissant que DPLL sur les gros encodages.\n", "\n", - "**Verdict SOTA (EPIC #3801) : RECOVERABLE-LOCAL.** Microsoft.Z3 4.12.2 (version max publiee sur NuGet) est installable et invocable en kernel `.net-csharp` (confirme cycle précédent : `x>0 AND x<0` -> UNSATISFIABLE, `x>5` -> SATISFIABLE x=6). On execute donc le **vrai solveur Z3**, pas un workaround." + "**Verdict SOTA (EPIC #3801) : RECOVERABLE-LOCAL.** Microsoft.Z3 4.12.2 (version max publiee sur NuGet) est installable et invocable en kernel `.net-csharp` (confirme cycle précédent : `x>0 AND x<0` -> UNSATISFIABLE, `x>5` -> SATISFIABLE x=6). On execute donc le **vrai solveur Z3**, pas un workaround.\n", + "\n", + "Sous Linux et sous macOS Apple Silicon, le package NuGet ne contient pas la bibliothèque native de Z3 : la cellule suivante charge alors celle du paquet Python `z3-solver`, celui du twin Python, par `Z3NativeLoader.cs` de la série [Z3-API](../../SymbolicAI/SMT/Z3-API/README.md) (voir l'en-tête du fichier). Pour utiliser la même version de Z3 que le package NuGet : `pip install z3-solver==4.12.2.0`." ] }, { @@ -1274,65 +1744,95 @@ "id": "z3-tranche3-1", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.445797Z", - "iopub.status.busy": "2026-08-17T12:18:29.445566Z", - "iopub.status.idle": "2026-08-17T12:18:29.892944Z", - "shell.execute_reply": "2026-08-17T12:18:29.892768Z" - } + "iopub.execute_input": "2026-10-03T06:38:25.272757Z", + "iopub.status.busy": "2026-10-03T06:38:25.272556Z", + "iopub.status.idle": "2026-10-03T06:38:27.542618Z", + "shell.execute_reply": "2026-10-03T06:38:27.542332Z" + }, + "papermill": { + "duration": 2.277313, + "end_time": "2026-10-03T06:38:27.542712+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:25.265399+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
" + "text/html": [ + "
Installed Packages
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "VERIFICATION DU THEOREME D'ARROW PAR z3 (SMT)\r\n" + "output_type": "stream", + "text": [ + "VERIFICATION DU THEOREME D'ARROW PAR z3 (SMT)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Configuration : 3 alternatives, 2 electeurs\r\n" + "output_type": "stream", + "text": [ + " Configuration : 3 alternatives, 2 electeurs\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Profils : 36\r\n" + "output_type": "stream", + "text": [ + " Profils : 36\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Variables entieres : 108\r\n" + "output_type": "stream", + "text": [ + " Variables entieres : 108\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Contraintes (assert): 1244\r\n" + "output_type": "stream", + "text": [ + " Contraintes (assert): 1244\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Resultat : unsatisfiable\r\n" + "output_type": "stream", + "text": [ + " Resultat : unsatisfiable\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Temps : 95.5 ms\r\n" + "output_type": "stream", + "text": [ + " Temps : 55.9 ms\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Arrow verifie : Pareto + IIA + non-dictature = IMPOSSIBLE (SMT entiers)\r\n" + "output_type": "stream", + "text": [ + "=> Arrow verifie : Pareto + IIA + non-dictature = IMPOSSIBLE (SMT entiers)\n" + ] } ], "source": [ "#r \"nuget: Microsoft.Z3, 4.12.2\"\n", + "#load \"../../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs\"\n", "using Microsoft.Z3;\n", "\n", + "// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)\n", + "Z3NativeLoader.Register(typeof(Context).Assembly);\n", + "\n", "// === Encodeur SMT du theoreme d'Arrow avec Z3 (port C# de ArrowZ3Encoder Python, Partie 2) ===\n", "// Variables entieres : r_{pi}_{alt} = rang de alt dans le classement social du profil pi.\n", "// Contraintes : ordre total (rangs dans [0,n_alt), antisymetrie), Pareto faible, IIA, non-dictature.\n", @@ -1467,77 +1967,111 @@ "id": "z3-tranche3-2", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:29.894110Z", - "iopub.status.busy": "2026-08-17T12:18:29.893901Z", - "iopub.status.idle": "2026-08-17T12:18:30.016008Z", - "shell.execute_reply": "2026-08-17T12:18:30.015765Z" - } + "iopub.execute_input": "2026-10-03T06:38:27.566027Z", + "iopub.status.busy": "2026-10-03T06:38:27.565828Z", + "iopub.status.idle": "2026-10-03T06:38:27.738765Z", + "shell.execute_reply": "2026-10-03T06:38:27.737643Z" + }, + "papermill": { + "duration": 0.190032, + "end_time": "2026-10-03T06:38:27.738953+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:27.548921+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "RELAXATION 2 ALTERNATIVES (SMT)\r\n" + "output_type": "stream", + "text": [ + "RELAXATION 2 ALTERNATIVES (SMT)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Profils : 4, vars entieres : 8\r\n" + "output_type": "stream", + "text": [ + " Profils : 4, vars entieres : 8\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Resultat : satisfiable\r\n" + "output_type": "stream", + "text": [ + " Resultat : satisfiable\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "BENCHMARK ARROW : SAT (DPLL, booleens) vs SMT (Z3, entiers)\r\n" + "output_type": "stream", + "text": [ + "BENCHMARK ARROW : SAT (DPLL, booleens) vs SMT (Z3, entiers)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "==============================================================\r\n" + "output_type": "stream", + "text": [ + "==============================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Methode Variables Contraintes Verdict Temps(ms)\r\n" + "output_type": "stream", + "text": [ + " Methode Variables Contraintes Verdict Temps(ms)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "--------------------------------------------------------------\r\n" + "output_type": "stream", + "text": [ + "--------------------------------------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " SAT (DPLL booleens) 216 2216 UNSAT 1.1\r\n" + "output_type": "stream", + "text": [ + " SAT (DPLL booleens) 216 2216 UNSAT 1.6\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " SMT (Z3 entiers) 108 1244 UNSAT 95.5\r\n" + "output_type": "stream", + "text": [ + " SMT (Z3 entiers) 108 1244 UNSAT 55.9\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Les deux methodes convergent : UNSAT. SAT encode l'ordre en booleens\r\n" + "output_type": "stream", + "text": [ + "=> Les deux methodes convergent : UNSAT. SAT encode l'ordre en booleens\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " (une clause par paire), SMT en rangs entiers (theorie arithmetique native).\r\n" + "output_type": "stream", + "text": [ + " (une clause par paire), SMT en rangs entiers (theorie arithmetique native).\n" + ] } ], "source": [ @@ -1574,7 +2108,16 @@ { "cell_type": "markdown", "id": "z3-tranche3-3", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.011008, + "end_time": "2026-10-03T06:38:27.762041+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:27.751033+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interpretation du résultat SMT.** Z3 confirme le même verdict que DPLL : **UNSAT**. Les deux approches prouvent le theoreme d'Arrow, mais par des voies radicalement différentes :\n", "\n", @@ -1593,7 +2136,16 @@ { "cell_type": "markdown", "id": "db11645c", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006127, + "end_time": "2026-10-03T06:38:27.775872+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:27.769745+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "### 7.1 Relaxation des axiomes : chaque paire est réalisable\n", "\n", @@ -1612,52 +2164,76 @@ "id": "8a4828ff", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:30.017399Z", - "iopub.status.busy": "2026-08-17T12:18:30.017146Z", - "iopub.status.idle": "2026-08-17T12:18:30.174449Z", - "shell.execute_reply": "2026-08-17T12:18:30.174243Z" - } + "iopub.execute_input": "2026-10-03T06:38:27.790105Z", + "iopub.status.busy": "2026-10-03T06:38:27.789920Z", + "iopub.status.idle": "2026-10-03T06:38:28.088971Z", + "shell.execute_reply": "2026-10-03T06:38:28.088807Z" + }, + "papermill": { + "duration": 0.307077, + "end_time": "2026-10-03T06:38:28.089048+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:27.781971+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "RELAXATION DES AXIOMES D'ARROW (SMT, 3 alternatives, 2 electeurs)\r\n" + "output_type": "stream", + "text": [ + "RELAXATION DES AXIOMES D'ARROW (SMT, 3 alternatives, 2 electeurs)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "================================================================\r\n" + "output_type": "stream", + "text": [ + "================================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Cas 1 : Pareto + IIA -> satisfiable (temoin : dictature)\r\n" + "output_type": "stream", + "text": [ + " Cas 1 : Pareto + IIA -> satisfiable (temoin : dictature)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Cas 2 : Pareto + non-dictature -> satisfiable (temoin : Borda)\r\n" + "output_type": "stream", + "text": [ + " Cas 2 : Pareto + non-dictature -> satisfiable (temoin : Borda)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Cas 3 : IIA + non-dictature -> satisfiable (temoin : SWF triviale)\r\n" + "output_type": "stream", + "text": [ + " Cas 3 : IIA + non-dictature -> satisfiable (temoin : SWF triviale)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "=> Chaque paire d'axiomes est realisable : l'impossibilite n'apparait\r\n" + "output_type": "stream", + "text": [ + "=> Chaque paire d'axiomes est realisable : l'impossibilite n'apparait\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " qu'en reunissant les TROIS axiomes (cas complet : UNSAT).\r\n" + "output_type": "stream", + "text": [ + " qu'en reunissant les TROIS axiomes (cas complet : UNSAT).\n" + ] } ], "source": [ @@ -1698,7 +2274,16 @@ { "cell_type": "markdown", "id": "dcc6949c", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006612, + "end_time": "2026-10-03T06:38:28.101911+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:28.095299+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Lecture du résultat.** Les trois paires sont `satisfiable` : la frontière de l'impossibilité est exactement le **trio** d'axiomes, pas une paire. Chaque relaxation ouvre une porte connue — une dictature (Pareto+IIA), une règle de position type Borda (Pareto+non-dictature), une fonction triviale (IIA+non-dictature). C'est la lecture constructive du théorème : abandonner *un seul* axiome suffit à rétablir l'existence d'une fonction de choix social." ] @@ -1706,7 +2291,16 @@ { "cell_type": "markdown", "id": "c5b0ad63", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.007118, + "end_time": "2026-10-03T06:38:28.115816+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:28.108698+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "### 7.2 Passage à l'échelle : grille alternatives × électeurs\n", "\n", @@ -1719,77 +2313,111 @@ "id": "c6233055", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:30.175842Z", - "iopub.status.busy": "2026-08-17T12:18:30.175638Z", - "iopub.status.idle": "2026-08-17T12:18:30.697133Z", - "shell.execute_reply": "2026-08-17T12:18:30.696860Z" - } + "iopub.execute_input": "2026-10-03T06:38:28.132644Z", + "iopub.status.busy": "2026-10-03T06:38:28.132235Z", + "iopub.status.idle": "2026-10-03T06:38:53.603332Z", + "shell.execute_reply": "2026-10-03T06:38:53.603135Z" + }, + "papermill": { + "duration": 25.480565, + "end_time": "2026-10-03T06:38:53.603434+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:28.122869+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "PASSAGE A L'ECHELLE : ARROW SMT (Z3)\r\n" + "output_type": "stream", + "text": [ + "PASSAGE A L'ECHELLE : ARROW SMT (Z3)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "======================================================================\r\n" + "output_type": "stream", + "text": [ + "======================================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " Alt Voters Profils Vars int Resultat Temps(ms)\r\n" + "output_type": "stream", + "text": [ + " Alt Voters Profils Vars int Resultat Temps(ms)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "----------------------------------------------------------------------\r\n" + "output_type": "stream", + "text": [ + "----------------------------------------------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 2 2 4 8 SAT 16.3\r\n" + "output_type": "stream", + "text": [ + " 2 2 4 8 SAT 144.3\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 2 3 8 16 SAT 17.6\r\n" + "output_type": "stream", + "text": [ + " 2 3 8 16 SAT 106.8\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 3 2 36 108 UNSAT 29.2\r\n" + "output_type": "stream", + "text": [ + " 3 2 36 108 UNSAT 94.4\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 3 3 216 648 UNSAT 225.8\r\n" + "output_type": "stream", + "text": [ + " 3 3 216 648 UNSAT 500.9\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 4 2 576 2304 UNSAT 4649.7\r\n" + "output_type": "stream", + "text": [ + " 4 2 576 2304 UNSAT 7989.1\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 4 3 13824 55296 ABANDON construction > budget 15 s ( 15022 ms ecoules)\r\n" + "output_type": "stream", + "text": [ + " 4 3 13824 55296 ABANDON construction > budget 15 s ( 15092 ms ecoules)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "FRONTIERE MESUREE : 4 alternatives x 2 electeurs tiennent (UNSAT) ; c'est la profondeur du profil (3 electeurs = 13 824 profils), pas la largeur, qui fait exploser la construction.\r\n" + "output_type": "stream", + "text": [ + "FRONTIERE MESUREE : 4 alternatives x 2 electeurs tiennent (UNSAT) ; c'est la profondeur du profil (3 electeurs = 13 824 profils), pas la largeur, qui fait exploser la construction.\n" + ] } ], "source": [ @@ -1847,7 +2475,16 @@ { "cell_type": "markdown", "id": "6521b221", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006598, + "end_time": "2026-10-03T06:38:53.617433+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:53.610835+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Lecture du résultat.** La grille exhibe la frontière exacte du théorème : les deux lignes à 2 alternatives sont `SAT` (aucun cycle possible — le théorème exige |A| >= 3, cf. la relaxation de la section précédente), les deux à 3 alternatives sont `UNSAT`. Côté coût, le temps Z3 croît fortement avec la grille au rythme de l'explosion du nombre de profils ; la case (3, 3) reste largement jouable — le jumeau Python mesure un ordre de grandeur ~1 s sur la même case. Point honnête : à cette échelle notebook, le DPLL booléen from-scratch de la partie 1 résout le même cas Arrow (3 alternatives, 2 électeurs) plus vite que Z3 sur le même cas : le backtracking compilé n'a pas de surcoût constant, et l'avantage d'un solveur de production (apprentissage de clauses, heuristiques de branchement) ne devient visible qu'au-delà de ces tailles. Les deux encodages — booléen (partie 1) et rangs entiers (partie 2, cette section) — convergent sur les mêmes verdicts. L'estimation à 4 alternatives marque la limite pratique : 576 profils (2 électeurs) reste jouable, 13 824 profils (3 électeurs) sort du cadre du notebook.\n", "\n", @@ -1860,7 +2497,16 @@ { "cell_type": "markdown", "id": "pysat-tranche-0", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006213, + "end_time": "2026-10-03T06:38:53.630288+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:53.624075+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "## 8. Pont industriel : les solveurs PySAT via PythonNet\n", @@ -1876,7 +2522,7 @@ "repose sur `BinaryFormatter`, supprime de .NET 9 ; les previews 3.1.0 anterieures a la\n", "sortie de CPython 3.13 ne chargent pas son ABI) + `Runtime.PythonDLL` pointant vers un\n", "CPython 3.13 dans lequel `python-sat` est installe (`pip install python-sat`). La\n", - "variable d'environnement `PYTHONNET_PYDLL` surcharge le chemin par defaut.\n", + "variable d'environnement `PYTHONNET_PYDLL` surcharge le chemin par defaut. Sans cette variable ni ce fichier, la cellule interroge le premier interpréteur (`python3`, puis `python`) qui importe `pysat`, et en reprend la bibliothèque et le `sys.path` : sous Linux et macOS, `pip install python-sat` suffit, environnement virtuel compris.\n", "\n", "Le pont est **en plus, jamais a la place** : le DPLL from-scratch reste l'outil\n", "pedagogique des sections 1 a 6 ; le pont fournit la jambe industrielle qui manquait\n", @@ -1889,89 +2535,131 @@ "id": "pysat-tranche-1", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:30.698693Z", - "iopub.status.busy": "2026-08-17T12:18:30.698476Z", - "iopub.status.idle": "2026-08-17T12:18:34.795026Z", - "shell.execute_reply": "2026-08-17T12:18:34.794697Z" - } + "iopub.execute_input": "2026-10-03T06:38:53.645926Z", + "iopub.status.busy": "2026-10-03T06:38:53.645702Z", + "iopub.status.idle": "2026-10-03T06:39:15.801262Z", + "shell.execute_reply": "2026-10-03T06:39:15.801062Z" + }, + "papermill": { + "duration": 22.16457, + "end_time": "2026-10-03T06:39:15.801370+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:53.636800+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
" + "text/html": [ + "
Installed Packages
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "Pont PythonNet : CPython 3.13.15 (tags/v3.13.15:4061bc4, Aug 5 2026, 13:05:39) [MSC v.1944 64 bit (AMD64)], pythonnet 3.1.0\r\n" + "output_type": "stream", + "text": [ + "Pont PythonNet : CPython 3.11.15 (main, Mar 3 2026, 09:26:23) [GCC 13.3.0], pythonnet 3.1.0\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "PYSAT SUR L'ENCODAGE D'ARROW (3 alternatives, 2 votants)\r\n" + "output_type": "stream", + "text": [ + "PYSAT SUR L'ENCODAGE D'ARROW (3 alternatives, 2 votants)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "======================================================\r\n" + "output_type": "stream", + "text": [ + "======================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Meme instance que DPLL : 216 variables, 2216 clauses\r\n" + "output_type": "stream", + "text": [ + "Meme instance que DPLL : 216 variables, 2216 clauses\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Glucose3 : UNSAT (Arrow verifie) [ 2.4 ms]\nMiniSat22 : UNSAT (Arrow verifie) [ 1.7 ms]\nCaDiCaL103 : UNSAT (Arrow verifie) [ 4.6 ms]\r\n" + "output_type": "stream", + "text": [ + "Glucose3 : UNSAT (Arrow verifie) [ 1.1 ms]\n", + "MiniSat22 : UNSAT (Arrow verifie) [ 0.8 ms]\n", + "CaDiCaL103 : UNSAT (Arrow verifie) [ 2.6 ms]\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Les 3 solveurs CDCL retrouvent le verdict du DPLL (Section 3) et du twin Python (cellule 11).\r\n" + "output_type": "stream", + "text": [ + "Les 3 solveurs CDCL retrouvent le verdict du DPLL (Section 3) et du twin Python (cellule 11).\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "PYSAT SUR L'ENCODAGE D'ARROW (4 alternatives, 2 votants)\r\n" + "output_type": "stream", + "text": [ + "PYSAT SUR L'ENCODAGE D'ARROW (4 alternatives, 2 votants)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "======================================================\r\n" + "output_type": "stream", + "text": [ + "======================================================\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Encodage : 576 profils, 6912 variables, 1010882 clauses, construction 1201 ms\r\n" + "output_type": "stream", + "text": [ + "Encodage : 576 profils, 6912 variables, 1010882 clauses, construction 2240 ms\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Glucose3 : UNSAT (Arrow verifie) [ 287.1 ms]\nMiniSat22 : UNSAT (Arrow verifie) [ 285.5 ms]\nCaDiCaL103 : UNSAT (Arrow verifie) [ 322.3 ms]\r\n" + "output_type": "stream", + "text": [ + "Glucose3 : UNSAT (Arrow verifie) [ 286.2 ms]\n", + "MiniSat22 : UNSAT (Arrow verifie) [ 290.4 ms]\n", + "CaDiCaL103 : UNSAT (Arrow verifie) [ 434.9 ms]\n" + ] } ], "source": [ @@ -1982,9 +2670,56 @@ "// Les 3 solveurs CDCL du twin Python (cellule 11) sur le MEME encodage C# que le\n", "// DPLL from-scratch de la Section 3. Pont EN PLUS, jamais a la place.\n", "\n", - "Runtime.PythonDLL = Environment.GetEnvironmentVariable(\"PYTHONNET_PYDLL\")\n", + "// Repli portable (Linux, macOS, ou Windows sans le CPython ci-dessus) : le premier\n", + "// interpreteur (python3, puis python) qui importe le module fournit sa bibliotheque\n", + "// partagee, son prefixe et son sys.path, environnement virtuel compris.\n", + "static void InitPythonFromInterpreter(string module)\n", + "{\n", + " const string probe =\n", + " \"import importlib, json, os, sys, sysconfig\\n\" +\n", + " \"importlib.import_module(sys.argv[1])\\n\" +\n", + " \"v = sysconfig.get_config_var; lib = v('LIBDIR') or ''; mm = sys.version_info[:2]\\n\" +\n", + " \"c = [os.path.join(lib, n) for n in (v('INSTSONAME'), v('LDLIBRARY')) if n]\\n\" +\n", + " \"c += [os.path.join(d, 'libpython%d.%d.dylib' % mm) for d in (lib, os.path.join(sys.base_prefix, 'lib'))]\\n\" +\n", + " \"c.append(os.path.join(sys.base_prefix, 'python%d%d.dll' % mm))\\n\" +\n", + " \"dll = next((p for p in c if os.path.isfile(p)), '')\\n\" +\n", + " \"print(json.dumps({'dll': dll, 'home': sys.base_prefix, 'path': [p for p in sys.path if p]}))\\n\";\n", + " foreach (var exe in new[] { \"python3\", \"python\" })\n", + " {\n", + " try\n", + " {\n", + " var psi = new System.Diagnostics.ProcessStartInfo(exe)\n", + " { RedirectStandardOutput = true, RedirectStandardError = true, UseShellExecute = false };\n", + " foreach (var arg in new[] { \"-c\", probe, module }) psi.ArgumentList.Add(arg);\n", + " using var p = System.Diagnostics.Process.Start(psi);\n", + " var stderr = p.StandardError.ReadToEndAsync();\n", + " string json = p.StandardOutput.ReadToEnd();\n", + " p.WaitForExit();\n", + " if (p.ExitCode != 0) continue;\n", + " var info = System.Text.Json.JsonDocument.Parse(json).RootElement;\n", + " string dll = info.GetProperty(\"dll\").GetString();\n", + " if (string.IsNullOrEmpty(dll)) continue;\n", + " Runtime.PythonDLL = dll;\n", + " PythonEngine.PythonHome = info.GetProperty(\"home\").GetString();\n", + " PythonEngine.Initialize();\n", + " using (Py.GIL())\n", + " {\n", + " var path = info.GetProperty(\"path\").EnumerateArray()\n", + " .Select(e => (PyObject)new PyString(e.GetString())).ToArray();\n", + " Py.Import(\"sys\").SetAttr(\"path\", new PyList(path));\n", + " }\n", + " return;\n", + " }\n", + " catch (System.ComponentModel.Win32Exception) { } // interpreteur absent du PATH\n", + " }\n", + " throw new System.IO.FileNotFoundException(\n", + " $\"Aucun CPython n'importe {module} : l'installer (pip install), ou definir PYTHONNET_PYDLL.\");\n", + "}\n", + "\n", + "var pyDll = Environment.GetEnvironmentVariable(\"PYTHONNET_PYDLL\")\n", " ?? @\"C:\\Users\\jsboi\\AppData\\Local\\Programs\\Python\\Python313\\python313.dll\";\n", - "PythonEngine.Initialize();\n", + "if (System.IO.File.Exists(pyDll)) { Runtime.PythonDLL = pyDll; PythonEngine.Initialize(); }\n", + "else InitPythonFromInterpreter(\"pysat\");\n", "Console.WriteLine($\"Pont PythonNet : CPython {PythonEngine.Version}, pythonnet 3.1.0\");\n", "Console.WriteLine();\n", "\n", @@ -2057,7 +2792,16 @@ { "cell_type": "markdown", "id": "pysat-tranche-2", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.007469, + "end_time": "2026-10-03T06:39:15.816887+00:00", + "exception": false, + "start_time": "2026-10-03T06:39:15.809418+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Lecture du résultat.** Les trois solveurs CDCL (**Glucose3**, **MiniSat22**,\n", "**CaDiCaL103**) concluent **UNSAT** sur l'encodage d'Arrow produit par l'`ArrowSATEncoder`\n", @@ -2076,7 +2820,16 @@ { "cell_type": "markdown", "id": "a84aabff", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006944, + "end_time": "2026-10-03T06:39:15.831101+00:00", + "exception": false, + "start_time": "2026-10-03T06:39:15.824157+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "## 9. Exercices\n", "\n", @@ -2096,17 +2849,27 @@ "id": "7d0146e7", "metadata": { "execution": { - "iopub.execute_input": "2026-08-17T12:18:34.796547Z", - "iopub.status.busy": "2026-08-17T12:18:34.796374Z", - "iopub.status.idle": "2026-08-17T12:18:34.840815Z", - "shell.execute_reply": "2026-08-17T12:18:34.840506Z" - } + "iopub.execute_input": "2026-10-03T06:39:15.847934Z", + "iopub.status.busy": "2026-10-03T06:39:15.847713Z", + "iopub.status.idle": "2026-10-03T06:39:15.870011Z", + "shell.execute_reply": "2026-10-03T06:39:15.869886Z" + }, + "papermill": { + "duration": 0.031655, + "end_time": "2026-10-03T06:39:15.870078+00:00", + "exception": false, + "start_time": "2026-10-03T06:39:15.838423+00:00", + "status": "completed" + }, + "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "3 exercices definis (stubs) : purs litteraux (DPLL), robustesse Sen (liberty-pairs), Sen par Z3 (SMT).\r\n" + "output_type": "stream", + "text": [ + "3 exercices definis (stubs) : purs litteraux (DPLL), robustesse Sen (liberty-pairs), Sen par Z3 (SMT).\n" + ] } ], "source": [ @@ -2151,7 +2914,16 @@ { "cell_type": "markdown", "id": "f8da6333", - "metadata": {}, + "metadata": { + "papermill": { + "duration": 0.006681, + "end_time": "2026-10-03T06:39:15.883349+00:00", + "exception": false, + "start_time": "2026-10-03T06:39:15.876668+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -2212,8 +2984,20 @@ "name": "C#", "pygments_lexer": "csharp", "version": "13.0" + }, + "papermill": { + "default_parameters": {}, + "duration": 55.716328, + "end_time": "2026-10-03T06:39:16.007473+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "04-Computational-Aggregation-SAT-Z3-Csharp.ipynb", + "output_path": "04-Computational-Aggregation-SAT-Z3-Csharp.ipynb", + "parameters": {}, + "start_time": "2026-10-03T06:38:20.291145+00:00", + "version": "2.7.0" } }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb index 30d9ab3234..07e9445d4d 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-10-SymbolicAutomata-CSharp.ipynb @@ -5,10 +5,10 @@ "id": "1b2fe231-df48-4cf9-8103-51c13128d979", "metadata": { "papermill": { - "duration": 0.009069, - "end_time": "2026-07-08T06:06:10.522766+00:00", + "duration": 0.005214, + "end_time": "2026-10-03T06:38:02.138376+00:00", "exception": false, - "start_time": "2026-07-08T06:06:10.513697+00:00", + "start_time": "2026-10-03T06:38:02.133162+00:00", "status": "completed" }, "tags": [] @@ -46,6 +46,7 @@ "\n", "- Bases du C# (classes, génériques, LINQ).\n", "- Notions de théorie des langages (états, alphabet, transitions) — voir §1.\n", + "- Pour le pont de la tranche 3 : un CPython où `automata-lib` est installé (`pip install automata-lib`). Sans `PYTHONNET_PYDLL` ni le CPython Windows préconfiguré, la cellule du pont interroge le premier interpréteur (`python3`, puis `python`) qui importe `automata`, et en reprend la bibliothèque et le `sys.path`, environnement virtuel compris.\n", "\n", "### Durée estimée : 45 minutes\n" ] @@ -55,10 +56,10 @@ "id": "3f8b2b57-6876-436c-b5ba-a712307aa313", "metadata": { "papermill": { - "duration": 0.009868, - "end_time": "2026-07-08T06:06:10.543772+00:00", + "duration": 0.003661, + "end_time": "2026-10-03T06:38:02.147373+00:00", "exception": false, - "start_time": "2026-07-08T06:06:10.533904+00:00", + "start_time": "2026-10-03T06:38:02.143712+00:00", "status": "completed" }, "tags": [] @@ -98,10 +99,10 @@ "id": "db383a36-5da4-4b60-925b-b7b4811415fb", "metadata": { "papermill": { - "duration": 0.008998, - "end_time": "2026-07-08T06:06:10.559757+00:00", + "duration": 0.004857, + "end_time": "2026-10-03T06:38:02.156390+00:00", "exception": false, - "start_time": "2026-07-08T06:06:10.550759+00:00", + "start_time": "2026-10-03T06:38:02.151533+00:00", "status": "completed" }, "tags": [] @@ -127,34 +128,147 @@ "id": "f637c881-d705-427b-80a7-fae497ef4df9", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:10.595236Z", - "iopub.status.busy": "2026-07-08T06:06:10.581996Z", - "iopub.status.idle": "2026-07-08T06:06:14.278509Z", - "shell.execute_reply": "2026-07-08T06:06:14.269861Z" + "iopub.execute_input": "2026-10-03T06:38:02.183230Z", + "iopub.status.busy": "2026-10-03T06:38:02.170731Z", + "iopub.status.idle": "2026-10-03T06:38:04.372598Z", + "shell.execute_reply": "2026-10-03T06:38:04.366797Z" }, "papermill": { - "duration": 3.710976, - "end_time": "2026-07-08T06:06:14.279234+00:00", + "duration": 2.212375, + "end_time": "2026-10-03T06:38:04.372748+00:00", "exception": false, - "start_time": "2026-07-08T06:06:10.568258+00:00", + "start_time": "2026-10-03T06:38:02.160373+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "" + "text/html": [ + "\r\n", + "
\r\n", + " \r\n", + " \r\n", + "
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/plain": "Bibliotheques definies :\n - DFA : automate deterministe (Delta : (etat, symbole) -> etat)\n - NFA : automate non deterministe (Delta : (etat, symbole) -> ensemble d'etats)\nEnvironnement pret." + "text/plain": [ + "Bibliotheques definies :\n", + " - DFA : automate deterministe (Delta : (etat, symbole) -> etat)\n", + " - NFA : automate non deterministe (Delta : (etat, symbole) -> ensemble d'etats)\n", + "Environnement pret." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -247,10 +361,10 @@ "id": "3c14ad21-b825-4e46-bae2-5e522d4a828d", "metadata": { "papermill": { - "duration": 0.007424, - "end_time": "2026-07-08T06:06:14.294273+00:00", + "duration": 0.003463, + "end_time": "2026-10-03T06:38:04.380296+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.286849+00:00", + "start_time": "2026-10-03T06:38:04.376833+00:00", "status": "completed" }, "tags": [] @@ -271,27 +385,41 @@ "id": "eb299818-47f2-439c-9722-02e33e10087a", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:14.309386Z", - "iopub.status.busy": "2026-07-08T06:06:14.308992Z", - "iopub.status.idle": "2026-07-08T06:06:14.608496Z", - "shell.execute_reply": "2026-07-08T06:06:14.608271Z" + "iopub.execute_input": "2026-10-03T06:38:04.390278Z", + "iopub.status.busy": "2026-10-03T06:38:04.390081Z", + "iopub.status.idle": "2026-10-03T06:38:04.696291Z", + "shell.execute_reply": "2026-10-03T06:38:04.696103Z" }, "papermill": { - "duration": 0.307874, - "end_time": "2026-07-08T06:06:14.608605+00:00", + "duration": 0.312141, + "end_time": "2026-10-03T06:38:04.696392+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.300731+00:00", + "start_time": "2026-10-03T06:38:04.384251+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "NFA pour reconnaissance de 'ab'\n\r\nAlphabet : { a, b } Etat initial : q0 Etat final : q2\n\r\nMot Accepte ? \r\n--------------------\r\nab OUI \r\naab OUI \r\nabab OUI \r\na non \r\nb non \r\nba non \r\naa non \r\n" + "text/plain": [ + "NFA pour reconnaissance de 'ab'\n", + "\n", + "Alphabet : { a, b } Etat initial : q0 Etat final : q2\n", + "\n", + "Mot Accepte ? \n", + "--------------------\n", + "ab OUI \n", + "aab OUI \n", + "abab OUI \n", + "a non \n", + "b non \n", + "ba non \n", + "aa non \n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -325,10 +453,10 @@ "id": "063b7601-ec88-46a5-86a2-43f4aadae0a2", "metadata": { "papermill": { - "duration": 0.006033, - "end_time": "2026-07-08T06:06:14.621605+00:00", + "duration": 0.004094, + "end_time": "2026-10-03T06:38:04.705286+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.615572+00:00", + "start_time": "2026-10-03T06:38:04.701192+00:00", "status": "completed" }, "tags": [] @@ -349,10 +477,10 @@ "id": "b3446074-6802-40b0-8fd0-e72762bd586f", "metadata": { "papermill": { - "duration": 0.007291, - "end_time": "2026-07-08T06:06:14.637649+00:00", + "duration": 0.003527, + "end_time": "2026-10-03T06:38:04.712900+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.630358+00:00", + "start_time": "2026-10-03T06:38:04.709373+00:00", "status": "completed" }, "tags": [] @@ -371,27 +499,40 @@ "id": "061d2bfa-feed-416b-8ce0-62cd8c840620", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:14.653402Z", - "iopub.status.busy": "2026-07-08T06:06:14.652915Z", - "iopub.status.idle": "2026-07-08T06:06:14.946337Z", - "shell.execute_reply": "2026-07-08T06:06:14.946077Z" + "iopub.execute_input": "2026-10-03T06:38:04.722229Z", + "iopub.status.busy": "2026-10-03T06:38:04.721922Z", + "iopub.status.idle": "2026-10-03T06:38:04.915469Z", + "shell.execute_reply": "2026-10-03T06:38:04.915261Z" }, "papermill": { - "duration": 0.301755, - "end_time": "2026-07-08T06:06:14.946447+00:00", + "duration": 0.199229, + "end_time": "2026-10-03T06:38:04.915617+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.644692+00:00", + "start_time": "2026-10-03T06:38:04.716388+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "DFA pour nombre pair de 'a'\n\r\nMot #a Accepte ? \r\n--------------------------\r\n(vide) 0 OUI \r\na 1 non \r\naa 2 OUI \r\naaa 3 non \r\nb 0 OUI \r\nab 1 non \r\naba 2 OUI \r\nbab 1 non \r\n" + "text/plain": [ + "DFA pour nombre pair de 'a'\n", + "\n", + "Mot #a Accepte ? \n", + "--------------------------\n", + "(vide) 0 OUI \n", + "a 1 non \n", + "aa 2 OUI \n", + "aaa 3 non \n", + "b 0 OUI \n", + "ab 1 non \n", + "aba 2 OUI \n", + "bab 1 non \n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -426,10 +567,10 @@ "id": "8ba25e3b-822d-4f8a-bcfa-9b7d8bb9a24e", "metadata": { "papermill": { - "duration": 0.008328, - "end_time": "2026-07-08T06:06:14.962737+00:00", + "duration": 0.004923, + "end_time": "2026-10-03T06:38:04.926096+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.954409+00:00", + "start_time": "2026-10-03T06:38:04.921173+00:00", "status": "completed" }, "tags": [] @@ -446,10 +587,10 @@ "id": "54108984-9b99-4e5c-9db9-c3adf859f389", "metadata": { "papermill": { - "duration": 0.008172, - "end_time": "2026-07-08T06:06:14.978834+00:00", + "duration": 0.003902, + "end_time": "2026-10-03T06:38:04.933840+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.970662+00:00", + "start_time": "2026-10-03T06:38:04.929938+00:00", "status": "completed" }, "tags": [] @@ -473,25 +614,27 @@ "id": "c2d7c2a6-9401-49c1-a011-7d7c19c4027b", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:14.996925Z", - "iopub.status.busy": "2026-07-08T06:06:14.996637Z", - "iopub.status.idle": "2026-07-08T06:06:15.150370Z", - "shell.execute_reply": "2026-07-08T06:06:15.150119Z" + "iopub.execute_input": "2026-10-03T06:38:04.945003Z", + "iopub.status.busy": "2026-10-03T06:38:04.944812Z", + "iopub.status.idle": "2026-10-03T06:38:05.041169Z", + "shell.execute_reply": "2026-10-03T06:38:05.041003Z" }, "papermill": { - "duration": 0.163129, - "end_time": "2026-07-08T06:06:15.150474+00:00", + "duration": 0.1025, + "end_time": "2026-10-03T06:38:05.041258+00:00", "exception": false, - "start_time": "2026-07-08T06:06:14.987345+00:00", + "start_time": "2026-10-03T06:38:04.938758+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Exercice a completer : NFA pour mots se terminant par 'ba'\r\n" + "output_type": "stream", + "text": [ + "Exercice a completer : NFA pour mots se terminant par 'ba'\n" + ] } ], "source": [ @@ -509,10 +652,10 @@ "id": "5078b1b7-59fe-4fa3-ad05-f73b807f9127", "metadata": { "papermill": { - "duration": 0.010353, - "end_time": "2026-07-08T06:06:15.171501+00:00", + "duration": 0.004278, + "end_time": "2026-10-03T06:38:05.050340+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.161148+00:00", + "start_time": "2026-10-03T06:38:05.046062+00:00", "status": "completed" }, "tags": [] @@ -539,27 +682,44 @@ "id": "2a088629-843b-4bac-b22b-ab843472d4bf", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:15.186686Z", - "iopub.status.busy": "2026-07-08T06:06:15.186278Z", - "iopub.status.idle": "2026-07-08T06:06:15.508779Z", - "shell.execute_reply": "2026-07-08T06:06:15.508450Z" + "iopub.execute_input": "2026-10-03T06:38:05.061058Z", + "iopub.status.busy": "2026-10-03T06:38:05.060833Z", + "iopub.status.idle": "2026-10-03T06:38:05.221835Z", + "shell.execute_reply": "2026-10-03T06:38:05.221647Z" }, "papermill": { - "duration": 0.331248, - "end_time": "2026-07-08T06:06:15.508906+00:00", + "duration": 0.167338, + "end_time": "2026-10-03T06:38:05.221922+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.177658+00:00", + "start_time": "2026-10-03T06:38:05.054584+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Operations sur les automates\n\r\nL1 = 'nombre pair de a' L2 = 'se termine par b' L1 n L2\n\r\nMot L1 L2 L1nL2 \r\n----------------------------\r\nb OUI OUI OUI \r\nab non OUI non \r\nbb OUI OUI OUI \r\naab OUI OUI OUI \r\nbab non OUI non \r\naa OUI non non \r\naabab non OUI non \r\n\nVerification coherence : L1 n L2 == L1 logique AND L2 sur chaque mot.\r\nCoherence produit cartesien : OK (intersection = AND logique)\r\n" + "text/plain": [ + "Operations sur les automates\n", + "\n", + "L1 = 'nombre pair de a' L2 = 'se termine par b' L1 n L2\n", + "\n", + "Mot L1 L2 L1nL2 \n", + "----------------------------\n", + "b OUI OUI OUI \n", + "ab non OUI non \n", + "bb OUI OUI OUI \n", + "aab OUI OUI OUI \n", + "bab non OUI non \n", + "aa OUI non non \n", + "aabab non OUI non \n", + "\n", + "Verification coherence : L1 n L2 == L1 logique AND L2 sur chaque mot.\n", + "Coherence produit cartesien : OK (intersection = AND logique)\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -623,10 +783,10 @@ "id": "a7b9dd2d-02a3-4342-9ba8-bebac2426985", "metadata": { "papermill": { - "duration": 0.005744, - "end_time": "2026-07-08T06:06:15.522418+00:00", + "duration": 0.003991, + "end_time": "2026-10-03T06:38:05.230479+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.516674+00:00", + "start_time": "2026-10-03T06:38:05.226488+00:00", "status": "completed" }, "tags": [] @@ -654,7 +814,17 @@ }, { "cell_type": "markdown", - "metadata": {}, + "id": "d39e5128", + "metadata": { + "papermill": { + "duration": 0.00398, + "end_time": "2026-10-03T06:38:05.238223+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:05.234243+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "***\n", "\n", @@ -682,64 +852,133 @@ { "cell_type": "code", "execution_count": 6, - "metadata": {}, + "id": "8dc1e652", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:38:05.248892Z", + "iopub.status.busy": "2026-10-03T06:38:05.248656Z", + "iopub.status.idle": "2026-10-03T06:38:12.036768Z", + "shell.execute_reply": "2026-10-03T06:38:12.036408Z" + }, + "papermill": { + "duration": 6.794073, + "end_time": "2026-10-03T06:38:12.036868+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:05.242795+00:00", + "status": "completed" + }, + "tags": [] + }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
" + "text/html": [ + "
Installed Packages
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "Pont PythonNet : CPython 3.13.12 | packaged by Anaconda, Inc. | (main, Feb 24 2026, 16:05:56) [MSC v.1942 64 bit (AMD64)] -> automata-lib (même moteur que le jumeau Python)\r\n" + "output_type": "stream", + "text": [ + "Pont PythonNet : CPython 3.11.15 (main, Mar 3 2026, 09:26:23) [GCC 13.3.0] -> automata-lib (même moteur que le jumeau Python)\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Mouvement 1 : NFA de \"ab\" (jumeau Python) rejoué via le moteur\nVecteur de tests (identique au jumeau) :\n 'ab' -> Accepté\n 'aab' -> Accepté\n 'abab' -> Accepté\n 'a' -> Rejeté\n 'b' -> Rejeté\n 'ba' -> Rejeté\n 'aa' -> Rejeté\nmoteur : automata-lib 9.2.0 sous CPython\r\n" + "output_type": "stream", + "text": [ + "Mouvement 1 : NFA de \"ab\" (jumeau Python) rejoué via le moteur\n", + "Vecteur de tests (identique au jumeau) :\n", + " 'ab' -> Accepté\n", + " 'aab' -> Accepté\n", + " 'abab' -> Accepté\n", + " 'a' -> Rejeté\n", + " 'b' -> Rejeté\n", + " 'ba' -> Rejeté\n", + " 'aa' -> Rejeté\n", + "moteur : automata-lib 9.2.0 sous CPython\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Mouvement 2 : DFA nombre pair de a (jumeau Python) + complement() du moteur\nVecteur de tests (identique au jumeau) :\n '' -> Pair\n 'a' -> Impair\n 'aa' -> Pair\n 'aaa' -> Impair\n 'b' -> Pair\n 'ab' -> Impair\n 'aba' -> Pair\n 'bab' -> Impair\ncomplement() : inversion vérifiée sur les 8 mots -> True\r\n" + "output_type": "stream", + "text": [ + "Mouvement 2 : DFA nombre pair de a (jumeau Python) + complement() du moteur\n", + "Vecteur de tests (identique au jumeau) :\n", + " '' -> Pair\n", + " 'a' -> Impair\n", + " 'aa' -> Pair\n", + " 'aaa' -> Impair\n", + " 'b' -> Pair\n", + " 'ab' -> Impair\n", + " 'aba' -> Pair\n", + " 'bab' -> Impair\n", + "complement() : inversion vérifiée sur les 8 mots -> True\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Mouvement 3 : opérations natives du moteur (Prong B)\nfrom_nfa : NFA 3 états -> DFA 3 états ; minify -> 3 états\nminify préserve le langage (symmetric_difference vide) : True\n\nunion / intersection natives (témoins) :\n 'ab' union=True intersection=False (pair? non | dans le langage? oui)\n 'aa' union=True intersection=False (pair? oui | dans le langage? non)\n 'ba' union=False intersection=False (pair? non | dans le langage? non)\n 'a' union=False intersection=False (pair? non | dans le langage? non)\n\ncontraste mesuré : from_substring(ab) vs le NFA -- langages équivalents = False\n témoin bab : from_substring accepte=True, NFA accepte=False\n -> le NFA exige au moins un a avant le premier b : son langage est a+ . b . (a|b)*, pas contient-ab\r\n" + "output_type": "stream", + "text": [ + "Mouvement 3 : opérations natives du moteur (Prong B)\n", + "from_nfa : NFA 3 états -> DFA 3 états ; minify -> 3 états\n", + "minify préserve le langage (symmetric_difference vide) : True\n", + "\n", + "union / intersection natives (témoins) :\n", + " 'ab' union=True intersection=False (pair? non | dans le langage? oui)\n", + " 'aa' union=True intersection=False (pair? oui | dans le langage? non)\n", + " 'ba' union=False intersection=False (pair? non | dans le langage? non)\n", + " 'a' union=False intersection=False (pair? non | dans le langage? non)\n", + "\n", + "contraste mesuré : from_substring(ab) vs le NFA -- langages équivalents = False\n", + " témoin bab : from_substring accepte=True, NFA accepte=False\n", + " -> le NFA exige au moins un a avant le premier b : son langage est a+ . b . (a|b)*, pas contient-ab\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "\r\n" + "output_type": "stream", + "text": [ + "\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Objets vivants dans le scope moteur : nfa_ab.accepts_input(aab) = True, accepts_input(bab) = False\r\n" + "output_type": "stream", + "text": [ + "Objets vivants dans le scope moteur : nfa_ab.accepts_input(aab) = True, accepts_input(bab) = False\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "--> le C# pilote le moteur par l'API du scope (Exec + Get) : le pont est une API, pas un eval aveugle.\r\n" + "output_type": "stream", + "text": [ + "--> le C# pilote le moteur par l'API du scope (Exec + Get) : le pont est une API, pas un eval aveugle.\n" + ] } ], "source": [ @@ -755,15 +994,62 @@ " Environment.GetEnvironmentVariable(\"PYTHONNET_PYDLL\"),\n", " @\"C:\\ProgramData\\miniconda3\\python313.dll\",\n", "};\n", + "// Repli portable (Linux, macOS, ou Windows sans le CPython ci-dessus) : le premier\n", + "// interpreteur (python3, puis python) qui importe le module fournit sa bibliotheque\n", + "// partagee, son prefixe et son sys.path, environnement virtuel compris.\n", + "static void InitPythonFromInterpreter(string module)\n", + "{\n", + " const string probe =\n", + " \"import importlib, json, os, sys, sysconfig\\n\" +\n", + " \"importlib.import_module(sys.argv[1])\\n\" +\n", + " \"v = sysconfig.get_config_var; lib = v('LIBDIR') or ''; mm = sys.version_info[:2]\\n\" +\n", + " \"c = [os.path.join(lib, n) for n in (v('INSTSONAME'), v('LDLIBRARY')) if n]\\n\" +\n", + " \"c += [os.path.join(d, 'libpython%d.%d.dylib' % mm) for d in (lib, os.path.join(sys.base_prefix, 'lib'))]\\n\" +\n", + " \"c.append(os.path.join(sys.base_prefix, 'python%d%d.dll' % mm))\\n\" +\n", + " \"dll = next((p for p in c if os.path.isfile(p)), '')\\n\" +\n", + " \"print(json.dumps({'dll': dll, 'home': sys.base_prefix, 'path': [p for p in sys.path if p]}))\\n\";\n", + " foreach (var exe in new[] { \"python3\", \"python\" })\n", + " {\n", + " try\n", + " {\n", + " var psi = new System.Diagnostics.ProcessStartInfo(exe)\n", + " { RedirectStandardOutput = true, RedirectStandardError = true, UseShellExecute = false };\n", + " foreach (var arg in new[] { \"-c\", probe, module }) psi.ArgumentList.Add(arg);\n", + " using var p = System.Diagnostics.Process.Start(psi);\n", + " var stderr = p.StandardError.ReadToEndAsync();\n", + " string json = p.StandardOutput.ReadToEnd();\n", + " p.WaitForExit();\n", + " if (p.ExitCode != 0) continue;\n", + " var info = System.Text.Json.JsonDocument.Parse(json).RootElement;\n", + " string dll = info.GetProperty(\"dll\").GetString();\n", + " if (string.IsNullOrEmpty(dll)) continue;\n", + " Runtime.PythonDLL = dll;\n", + " PythonEngine.PythonHome = info.GetProperty(\"home\").GetString();\n", + " PythonEngine.Initialize();\n", + " using (Py.GIL())\n", + " {\n", + " var path = info.GetProperty(\"path\").EnumerateArray()\n", + " .Select(e => (PyObject)new PyString(e.GetString())).ToArray();\n", + " Py.Import(\"sys\").SetAttr(\"path\", new PyList(path));\n", + " }\n", + " return;\n", + " }\n", + " catch (System.ComponentModel.Win32Exception) { } // interpreteur absent du PATH\n", + " }\n", + " throw new System.IO.FileNotFoundException(\n", + " $\"Aucun CPython n'importe {module} : l'installer (pip install), ou definir PYTHONNET_PYDLL.\");\n", + "}\n", + "\n", "string pyDll = dllCandidates.FirstOrDefault(File.Exists);\n", - "if (pyDll == null)\n", - " throw new FileNotFoundException(\"Aucun CPython avec automata-lib trouvé : fixer PYTHONNET_PYDLL (pip install automata-lib).\");\n", - "string pyDir = Path.GetDirectoryName(pyDll);\n", - "Environment.SetEnvironmentVariable(\n", - " \"PATH\", pyDir + Path.PathSeparator + Environment.GetEnvironmentVariable(\"PATH\"));\n", - "\n", - "Runtime.PythonDLL = pyDll;\n", - "PythonEngine.Initialize();\n", + "if (pyDll != null)\n", + "{\n", + " string pyDir = Path.GetDirectoryName(pyDll);\n", + " Environment.SetEnvironmentVariable(\n", + " \"PATH\", pyDir + Path.PathSeparator + Environment.GetEnvironmentVariable(\"PATH\"));\n", + " Runtime.PythonDLL = pyDll;\n", + " PythonEngine.Initialize();\n", + "}\n", + "else InitPythonFromInterpreter(\"automata\");\n", "Console.WriteLine($\"Pont PythonNet : CPython {PythonEngine.Version} -> automata-lib (même moteur que le jumeau Python)\");\n", "Console.WriteLine();\n", "\n", @@ -848,7 +1134,17 @@ }, { "cell_type": "markdown", - "metadata": {}, + "id": "c9444d2d", + "metadata": { + "papermill": { + "duration": 0.004385, + "end_time": "2026-10-03T06:38:12.046457+00:00", + "exception": false, + "start_time": "2026-10-03T06:38:12.042072+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "**Interprétation : le moteur sous le pont**\n", "\n", @@ -870,10 +1166,10 @@ "id": "7243aa33-9df1-4a4c-91e4-f387197c2fc8", "metadata": { "papermill": { - "duration": 0.006248, - "end_time": "2026-07-08T06:06:15.535615+00:00", + "duration": 0.00429, + "end_time": "2026-10-03T06:38:12.055131+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.529367+00:00", + "start_time": "2026-10-03T06:38:12.050841+00:00", "status": "completed" }, "tags": [] @@ -917,10 +1213,10 @@ "id": "91914c88-fb90-4f6e-92d5-515d81072508", "metadata": { "papermill": { - "duration": 0.006149, - "end_time": "2026-07-08T06:06:15.628096+00:00", + "duration": 0.004238, + "end_time": "2026-10-03T06:38:12.063631+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.621947+00:00", + "start_time": "2026-10-03T06:38:12.059393+00:00", "status": "completed" }, "tags": [] @@ -932,7 +1228,9 @@ "\n", "Z3 est le solveur SMT de Microsoft Research. En .NET, on l'obtient via le package NuGet\n", "`Microsoft.Z3` (version 4.12.2, dernière publiée). La cellule suivante restore le package\n", - "et importe l'espace de noms.\n" + "et importe l'espace de noms.\n", + "\n", + "Sous Linux et sous macOS Apple Silicon, ce package ne contient pas la bibliothèque native de Z3 : la cellule charge alors celle du paquet Python `z3-solver`, par `Z3NativeLoader.cs` de la série [Z3-API](../../SymbolicAI/SMT/Z3-API/README.md) (voir l'en-tête du fichier). Pour utiliser la même version de Z3 que le package NuGet : `pip install z3-solver==4.12.2.0`.\n" ] }, { @@ -941,43 +1239,59 @@ "id": "4dc984fd-3317-4383-9fd8-e46d9ba6c3af", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:15.656365Z", - "iopub.status.busy": "2026-07-08T06:06:15.655846Z", - "iopub.status.idle": "2026-07-08T06:06:16.745206Z", - "shell.execute_reply": "2026-07-08T06:06:16.744464Z" + "iopub.execute_input": "2026-10-03T06:38:12.074079Z", + "iopub.status.busy": "2026-10-03T06:38:12.073893Z", + "iopub.status.idle": "2026-10-03T06:38:14.465753Z", + "shell.execute_reply": "2026-10-03T06:38:14.465565Z" }, "papermill": { - "duration": 1.109356, - "end_time": "2026-07-08T06:06:16.745467+00:00", + "duration": 2.398087, + "end_time": "2026-10-03T06:38:14.465843+00:00", "exception": false, - "start_time": "2026-07-08T06:06:15.636111+00:00", + "start_time": "2026-10-03T06:38:12.067756+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
  • Microsoft.Z3
" + "text/html": [ + "
Installed Packages
  • Microsoft.Z3, 4.12.2
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/plain": "Z3 importe avec succes.\nPackage NuGet : Microsoft.Z3 4.12.2 (solveur SMT SOTA de Microsoft Research)\nContexte SMT cree.\n\nTypes de variables disponibles :\n - IntExpr : Entiers mathematiques (infinis, via MkIntConst)\n - BitVecExpr : Vecteurs de bits (taille fixe)\n - BoolExpr : Booleens (formules logiques)\n - RealExpr : Nombres reels" + "text/plain": [ + "Z3 importe avec succes.\n", + "Package NuGet : Microsoft.Z3 4.12.2 (solveur SMT SOTA de Microsoft Research)\n", + "Contexte SMT cree.\n", + "\n", + "Types de variables disponibles :\n", + " - IntExpr : Entiers mathematiques (infinis, via MkIntConst)\n", + " - BitVecExpr : Vecteurs de bits (taille fixe)\n", + " - BoolExpr : Booleens (formules logiques)\n", + " - RealExpr : Nombres reels" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ "// Restoration du package NuGet Microsoft.Z3 (solveur SOT de Microsoft Research).\n", "// Version 4.12.2 = derniere publiee sur NuGet (4.13+ n'existe pas encore en package).\n", "#r \"nuget: Microsoft.Z3, 4.12.2\"\n", + "#load \"../../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs\"\n", "using Microsoft.Z3;\n", "using System.Text;\n", "\n", + "// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)\n", + "Z3NativeLoader.Register(typeof(Context).Assembly);\n", + "\n", "var ctx = new Context();\n", "$@\"Z3 importe avec succes.\n", "Package NuGet : Microsoft.Z3 4.12.2 (solveur SMT SOTA de Microsoft Research)\n", @@ -995,10 +1309,10 @@ "id": "fd9ed1af-0b0d-4752-b685-d5c9a00708c5", "metadata": { "papermill": { - "duration": 0.009596, - "end_time": "2026-07-08T06:06:16.776198+00:00", + "duration": 0.004567, + "end_time": "2026-10-03T06:38:14.475622+00:00", "exception": false, - "start_time": "2026-07-08T06:06:16.766602+00:00", + "start_time": "2026-10-03T06:38:14.471055+00:00", "status": "completed" }, "tags": [] @@ -1017,27 +1331,50 @@ "id": "0b8b42f6-e164-4172-9fe6-0d90466698d6", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:16.797785Z", - "iopub.status.busy": "2026-07-08T06:06:16.797345Z", - "iopub.status.idle": "2026-07-08T06:06:17.426746Z", - "shell.execute_reply": "2026-07-08T06:06:17.426329Z" + "iopub.execute_input": "2026-10-03T06:38:14.486277Z", + "iopub.status.busy": "2026-10-03T06:38:14.486100Z", + "iopub.status.idle": "2026-10-03T06:38:14.675043Z", + "shell.execute_reply": "2026-10-03T06:38:14.674882Z" }, "papermill": { - "duration": 0.64079, - "end_time": "2026-07-08T06:06:17.426908+00:00", + "duration": 0.195115, + "end_time": "2026-10-03T06:38:14.675131+00:00", "exception": false, - "start_time": "2026-07-08T06:06:16.786118+00:00", + "start_time": "2026-10-03T06:38:14.480016+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Predicats symboliques avec Z3\n\r\nVariable : x (sort : Int)\n\r\nPredicats simples :\r\n x > 0 -> (> x 0)\r\n x < 100 -> (< x 100)\r\n x >= 10 -> (>= x 10)\r\n x <= 50 -> (<= x 50)\r\n x est pair (x mod 2 = 0) -> (= (mod x 2) 0)\r\n\nPredicats composes :\r\n 10 <= x <= 100 : (and (>= x 10) (<= x 100))\r\n x < 0 ou x > 100 : (or (< x 0) (> x 100))\r\n\nEvaluation de (10 <= x <= 100) sur des valeurs :\r\n x = -5 -> UNSATISFIABLE (rejete)\r\n x = 0 -> UNSATISFIABLE (rejete)\r\n x = 10 -> SATISFIABLE (accepte)\r\n x = 50 -> SATISFIABLE (accepte)\r\n x = 100 -> SATISFIABLE (accepte)\r\n x = 150 -> UNSATISFIABLE (rejete)\r\n" + "text/plain": [ + "Predicats symboliques avec Z3\n", + "\n", + "Variable : x (sort : Int)\n", + "\n", + "Predicats simples :\n", + " x > 0 -> (> x 0)\n", + " x < 100 -> (< x 100)\n", + " x >= 10 -> (>= x 10)\n", + " x <= 50 -> (<= x 50)\n", + " x est pair (x mod 2 = 0) -> (= (mod x 2) 0)\n", + "\n", + "Predicats composes :\n", + " 10 <= x <= 100 : (and (>= x 10) (<= x 100))\n", + " x < 0 ou x > 100 : (or (< x 0) (> x 100))\n", + "\n", + "Evaluation de (10 <= x <= 100) sur des valeurs :\n", + " x = -5 -> UNSATISFIABLE (rejete)\n", + " x = 0 -> UNSATISFIABLE (rejete)\n", + " x = 10 -> SATISFIABLE (accepte)\n", + " x = 50 -> SATISFIABLE (accepte)\n", + " x = 100 -> SATISFIABLE (accepte)\n", + " x = 150 -> UNSATISFIABLE (rejete)\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1083,10 +1420,10 @@ "id": "30ab4762-d2d8-4f9c-9cf3-51a69404f3cd", "metadata": { "papermill": { - "duration": 0.006854, - "end_time": "2026-07-08T06:06:17.441537+00:00", + "duration": 0.004771, + "end_time": "2026-10-03T06:38:14.685084+00:00", "exception": false, - "start_time": "2026-07-08T06:06:17.434683+00:00", + "start_time": "2026-10-03T06:38:14.680313+00:00", "status": "completed" }, "tags": [] @@ -1105,10 +1442,10 @@ "id": "d88dd21a-178a-4e26-b5b5-b46eeb5c3b69", "metadata": { "papermill": { - "duration": 0.006423, - "end_time": "2026-07-08T06:06:17.456145+00:00", + "duration": 0.004053, + "end_time": "2026-10-03T06:38:14.693494+00:00", "exception": false, - "start_time": "2026-07-08T06:06:17.449722+00:00", + "start_time": "2026-10-03T06:38:14.689441+00:00", "status": "completed" }, "tags": [] @@ -1133,27 +1470,29 @@ "id": "cd24edd2-d299-4b43-a3d2-0719ebed59d6", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:17.475098Z", - "iopub.status.busy": "2026-07-08T06:06:17.474571Z", - "iopub.status.idle": "2026-07-08T06:06:17.745396Z", - "shell.execute_reply": "2026-07-08T06:06:17.745163Z" + "iopub.execute_input": "2026-10-03T06:38:14.703373Z", + "iopub.status.busy": "2026-10-03T06:38:14.703181Z", + "iopub.status.idle": "2026-10-03T06:38:14.767822Z", + "shell.execute_reply": "2026-10-03T06:38:14.767676Z" }, "papermill": { - "duration": 0.28199, - "end_time": "2026-07-08T06:06:17.745501+00:00", + "duration": 0.070294, + "end_time": "2026-10-03T06:38:14.767899+00:00", "exception": false, - "start_time": "2026-07-08T06:06:17.463511+00:00", + "start_time": "2026-10-03T06:38:14.697605+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Classe SymbolicAutomaton definie (transitions = predicats Z3, Accepts via solveur SMT)." + "text/plain": [ + "Classe SymbolicAutomaton definie (transitions = predicats Z3, Accepts via solveur SMT)." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1224,10 +1563,10 @@ "id": "95ff9a96-1557-4e2b-aa65-ff09be95f550", "metadata": { "papermill": { - "duration": 0.006817, - "end_time": "2026-07-08T06:06:17.759178+00:00", + "duration": 0.00436, + "end_time": "2026-10-03T06:38:14.776829+00:00", "exception": false, - "start_time": "2026-07-08T06:06:17.752361+00:00", + "start_time": "2026-10-03T06:38:14.772469+00:00", "status": "completed" }, "tags": [] @@ -1245,27 +1584,41 @@ "id": "6ef13c4c-9693-4c79-9fb0-3842f9a62415", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:17.775770Z", - "iopub.status.busy": "2026-07-08T06:06:17.775441Z", - "iopub.status.idle": "2026-07-08T06:06:18.112831Z", - "shell.execute_reply": "2026-07-08T06:06:18.112603Z" + "iopub.execute_input": "2026-10-03T06:38:14.787420Z", + "iopub.status.busy": "2026-10-03T06:38:14.787238Z", + "iopub.status.idle": "2026-10-03T06:38:14.916198Z", + "shell.execute_reply": "2026-10-03T06:38:14.916034Z" }, "papermill": { - "duration": 0.346881, - "end_time": "2026-07-08T06:06:18.112950+00:00", + "duration": 0.134962, + "end_time": "2026-10-03T06:38:14.916289+00:00", "exception": false, - "start_time": "2026-07-08T06:06:17.766069+00:00", + "start_time": "2026-10-03T06:38:14.781327+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Automate symbolique pour l'intervalle [10, 100]\r\n q0 --[10 <= x <= 100]--> q1 (final)\n\r\nValeur Accepte ? \r\n----------------------\r\n-10 non \r\n0 non \r\n9 non \r\n10 OUI \r\n50 OUI \r\n100 OUI \r\n101 non \r\n500 non \r\n" + "text/plain": [ + "Automate symbolique pour l'intervalle [10, 100]\n", + " q0 --[10 <= x <= 100]--> q1 (final)\n", + "\n", + "Valeur Accepte ? \n", + "----------------------\n", + "-10 non \n", + "0 non \n", + "9 non \n", + "10 OUI \n", + "50 OUI \n", + "100 OUI \n", + "101 non \n", + "500 non \n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1291,10 +1644,10 @@ "id": "ac3d54ad-441d-4769-b849-3a80ab31aaa7", "metadata": { "papermill": { - "duration": 0.009006, - "end_time": "2026-07-08T06:06:18.129585+00:00", + "duration": 0.005066, + "end_time": "2026-10-03T06:38:14.926599+00:00", "exception": false, - "start_time": "2026-07-08T06:06:18.120579+00:00", + "start_time": "2026-10-03T06:38:14.921533+00:00", "status": "completed" }, "tags": [] @@ -1314,10 +1667,10 @@ "id": "ee5b50f3-629d-4d82-ab20-1b87626afe41", "metadata": { "papermill": { - "duration": 0.006402, - "end_time": "2026-07-08T06:06:18.142786+00:00", + "duration": 0.004526, + "end_time": "2026-10-03T06:38:14.936495+00:00", "exception": false, - "start_time": "2026-07-08T06:06:18.136384+00:00", + "start_time": "2026-10-03T06:38:14.931969+00:00", "status": "completed" }, "tags": [] @@ -1336,27 +1689,44 @@ "id": "b8278199-29b9-40d7-921b-c4510780ff18", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:18.157559Z", - "iopub.status.busy": "2026-07-08T06:06:18.157231Z", - "iopub.status.idle": "2026-07-08T06:06:19.013031Z", - "shell.execute_reply": "2026-07-08T06:06:19.012630Z" + "iopub.execute_input": "2026-10-03T06:38:14.946754Z", + "iopub.status.busy": "2026-10-03T06:38:14.946459Z", + "iopub.status.idle": "2026-10-03T06:38:15.228901Z", + "shell.execute_reply": "2026-10-03T06:38:15.228727Z" }, "papermill": { - "duration": 0.863931, - "end_time": "2026-07-08T06:06:19.013194+00:00", + "duration": 0.288315, + "end_time": "2026-10-03T06:38:15.228990+00:00", "exception": false, - "start_time": "2026-07-08T06:06:18.149263+00:00", + "start_time": "2026-10-03T06:38:14.940675+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Automate symbolique : nombres pairs POSITIFS\r\n q0 --[x >= 0]--> q1 --[x mod 2 = 0]--> q2 (final)\n\r\nValeur Accepte ? \r\n----------------------\r\n-4 non \r\n-2 non \r\n0 OUI \r\n1 non \r\n2 OUI \r\n3 non \r\n4 OUI \r\n7 non \r\n8 OUI \r\n100 OUI \r\n101 non \r\n" + "text/plain": [ + "Automate symbolique : nombres pairs POSITIFS\n", + " q0 --[x >= 0]--> q1 --[x mod 2 = 0]--> q2 (final)\n", + "\n", + "Valeur Accepte ? \n", + "----------------------\n", + "-4 non \n", + "-2 non \n", + "0 OUI \n", + "1 non \n", + "2 OUI \n", + "3 non \n", + "4 OUI \n", + "7 non \n", + "8 OUI \n", + "100 OUI \n", + "101 non \n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1383,10 +1753,10 @@ "id": "445dc32a-5710-48df-b0c1-0023d981a3d9", "metadata": { "papermill": { - "duration": 0.012683, - "end_time": "2026-07-08T06:06:19.036859+00:00", + "duration": 0.004841, + "end_time": "2026-10-03T06:38:15.239087+00:00", "exception": false, - "start_time": "2026-07-08T06:06:19.024176+00:00", + "start_time": "2026-10-03T06:38:15.234246+00:00", "status": "completed" }, "tags": [] @@ -1407,10 +1777,10 @@ "id": "f33e9fdf-45ce-4a06-ae3b-0e31241861af", "metadata": { "papermill": { - "duration": 0.012798, - "end_time": "2026-07-08T06:06:19.064003+00:00", + "duration": 0.004956, + "end_time": "2026-10-03T06:38:15.248666+00:00", "exception": false, - "start_time": "2026-07-08T06:06:19.051205+00:00", + "start_time": "2026-10-03T06:38:15.243710+00:00", "status": "completed" }, "tags": [] @@ -1428,27 +1798,43 @@ "id": "d8fdab0e-02ca-44db-9f4d-60834bb94086", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:19.090440Z", - "iopub.status.busy": "2026-07-08T06:06:19.090059Z", - "iopub.status.idle": "2026-07-08T06:06:20.231185Z", - "shell.execute_reply": "2026-07-08T06:06:20.230823Z" + "iopub.execute_input": "2026-10-03T06:38:15.259563Z", + "iopub.status.busy": "2026-10-03T06:38:15.259332Z", + "iopub.status.idle": "2026-10-03T06:38:15.635988Z", + "shell.execute_reply": "2026-10-03T06:38:15.635311Z" }, "papermill": { - "duration": 1.155451, - "end_time": "2026-07-08T06:06:20.231342+00:00", + "duration": 0.382837, + "end_time": "2026-10-03T06:38:15.636106+00:00", "exception": false, - "start_time": "2026-07-08T06:06:19.075891+00:00", + "start_time": "2026-10-03T06:38:15.253269+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Automate symbolique : multiples de 5 STRICTEMENT positifs\r\n q0 --[x > 0]--> q1 --[x mod 5 = 0]--> q2 (final)\n\r\nValeur Accepte ? \r\n----------------------\r\n-10 non \r\n0 non \r\n3 non \r\n5 OUI \r\n10 OUI \r\n12 non \r\n15 OUI \r\n20 OUI \r\n23 non \r\n100 OUI \r\n" + "text/plain": [ + "Automate symbolique : multiples de 5 STRICTEMENT positifs\n", + " q0 --[x > 0]--> q1 --[x mod 5 = 0]--> q2 (final)\n", + "\n", + "Valeur Accepte ? \n", + "----------------------\n", + "-10 non \n", + "0 non \n", + "3 non \n", + "5 OUI \n", + "10 OUI \n", + "12 non \n", + "15 OUI \n", + "20 OUI \n", + "23 non \n", + "100 OUI \n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1475,10 +1861,10 @@ "id": "dddea215-2f54-42b7-b857-43353d92cad9", "metadata": { "papermill": { - "duration": 0.010947, - "end_time": "2026-07-08T06:06:20.257816+00:00", + "duration": 0.005009, + "end_time": "2026-10-03T06:38:15.646648+00:00", "exception": false, - "start_time": "2026-07-08T06:06:20.246869+00:00", + "start_time": "2026-10-03T06:38:15.641639+00:00", "status": "completed" }, "tags": [] @@ -1503,25 +1889,27 @@ "id": "8958aab6-cac4-4624-b675-2ca31aa07bce", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:20.286558Z", - "iopub.status.busy": "2026-07-08T06:06:20.285987Z", - "iopub.status.idle": "2026-07-08T06:06:20.358475Z", - "shell.execute_reply": "2026-07-08T06:06:20.358125Z" + "iopub.execute_input": "2026-10-03T06:38:15.657375Z", + "iopub.status.busy": "2026-10-03T06:38:15.657200Z", + "iopub.status.idle": "2026-10-03T06:38:15.672857Z", + "shell.execute_reply": "2026-10-03T06:38:15.672739Z" }, "papermill": { - "duration": 0.084535, - "end_time": "2026-07-08T06:06:20.358628+00:00", + "duration": 0.021587, + "end_time": "2026-10-03T06:38:15.672922+00:00", "exception": false, - "start_time": "2026-07-08T06:06:20.274093+00:00", + "start_time": "2026-10-03T06:38:15.651335+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Exercice a completer : automate pour multiples de 7 dans [20, 100]\r\n" + "output_type": "stream", + "text": [ + "Exercice a completer : automate pour multiples de 7 dans [20, 100]\n" + ] } ], "source": [ @@ -1540,10 +1928,10 @@ "id": "faeb3046-d35b-4515-8bcf-90b2fd267d58", "metadata": { "papermill": { - "duration": 0.01046, - "end_time": "2026-07-08T06:06:20.386626+00:00", + "duration": 0.004337, + "end_time": "2026-10-03T06:38:15.681742+00:00", "exception": false, - "start_time": "2026-07-08T06:06:20.376166+00:00", + "start_time": "2026-10-03T06:38:15.677405+00:00", "status": "completed" }, "tags": [] @@ -1568,35 +1956,87 @@ "id": "1235e540-0ce3-4d4a-ad66-5096011e0089", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:20.412708Z", - "iopub.status.busy": "2026-07-08T06:06:20.412228Z", - "iopub.status.idle": "2026-07-08T06:06:21.948938Z", - "shell.execute_reply": "2026-07-08T06:06:21.949097Z" + "iopub.execute_input": "2026-10-03T06:38:15.691889Z", + "iopub.status.busy": "2026-10-03T06:38:15.691721Z", + "iopub.status.idle": "2026-10-03T06:38:17.186726Z", + "shell.execute_reply": "2026-10-03T06:38:17.186480Z" }, "papermill": { - "duration": 1.551845, - "end_time": "2026-07-08T06:06:21.949215+00:00", + "duration": 1.50065, + "end_time": "2026-10-03T06:38:17.186806+00:00", "exception": false, - "start_time": "2026-07-08T06:06:20.397370+00:00", + "start_time": "2026-10-03T06:38:15.686156+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Operations sur predicats symboliques\n\r\nPredicats : mult3 = (x mod 3 = 0), mult5 = (x mod 5 = 0)\n\r\nValeur mult3 mult5 3 OU 5 3 ET 5 (15) non-3 \r\n--------------------------------------------------\r\n1 non non non non OUI \r\n3 OUI non OUI non non \r\n5 non OUI OUI non OUI \r\n7 non non non non OUI \r\n9 OUI non OUI non non \r\n10 non OUI OUI non OUI \r\n15 OUI OUI OUI OUI non \r\n20 non OUI OUI non OUI \r\n30 OUI OUI OUI OUI non \r\n23 non non non non OUI \r\n\nVerification : '3 ET 5' = multiples de 15 uniquement (15, 30). 'non-3' = complement.\r\n" + "text/plain": [ + "Operations sur predicats symboliques\n", + "\n", + "Predicats : mult3 = (x mod 3 = 0), mult5 = (x mod 5 = 0)\n", + "\n", + "Valeur mult3 mult5 3 OU 5 3 ET 5 (15) non-3 \n", + "--------------------------------------------------\n", + "1 non non non non OUI \n", + "3 OUI non OUI non non \n", + "5 non OUI OUI non OUI \n", + "7 non non non non OUI \n", + "9 OUI non OUI non non \n", + "10 non OUI OUI non OUI \n", + "15 OUI OUI OUI OUI non \n", + "20 non OUI OUI non OUI \n", + "30 OUI OUI OUI OUI non \n", + "23 non non non non OUI \n", + "\n", + "Verification : '3 ET 5' = multiples de 15 uniquement (15, 30). 'non-3' = complement.\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "execute_result", "data": { - "text/html": "
<null>
" + "text/html": [ + "
<null>
" + ] }, + "execution_count": 14, "metadata": {}, - "execution_count": 14 + "output_type": "execute_result" } ], "source": [ @@ -1629,10 +2069,10 @@ "id": "4b751f0a-6ec3-49d0-b71d-155c5115863b", "metadata": { "papermill": { - "duration": 0.013135, - "end_time": "2026-07-08T06:06:21.973918+00:00", + "duration": 0.005367, + "end_time": "2026-10-03T06:38:17.197773+00:00", "exception": false, - "start_time": "2026-07-08T06:06:21.960783+00:00", + "start_time": "2026-10-03T06:38:17.192406+00:00", "status": "completed" }, "tags": [] @@ -1662,10 +2102,10 @@ "id": "66c05503", "metadata": { "papermill": { - "duration": 0.009259, - "end_time": "2026-07-08T06:06:21.990384+00:00", + "duration": 0.005125, + "end_time": "2026-10-03T06:38:17.208655+00:00", "exception": false, - "start_time": "2026-07-08T06:06:21.981125+00:00", + "start_time": "2026-10-03T06:38:17.203530+00:00", "status": "completed" }, "tags": [] @@ -1699,25 +2139,27 @@ "id": "da94b5e3", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T06:06:22.011186Z", - "iopub.status.busy": "2026-07-08T06:06:22.010749Z", - "iopub.status.idle": "2026-07-08T06:06:22.104260Z", - "shell.execute_reply": "2026-07-08T06:06:22.104060Z" + "iopub.execute_input": "2026-10-03T06:38:17.219985Z", + "iopub.status.busy": "2026-10-03T06:38:17.219793Z", + "iopub.status.idle": "2026-10-03T06:38:17.237976Z", + "shell.execute_reply": "2026-10-03T06:38:17.237847Z" }, "papermill": { - "duration": 0.104652, - "end_time": "2026-07-08T06:06:22.104360+00:00", + "duration": 0.024499, + "end_time": "2026-10-03T06:38:17.238043+00:00", "exception": false, - "start_time": "2026-07-08T06:06:21.999708+00:00", + "start_time": "2026-10-03T06:38:17.213544+00:00", "status": "completed" }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Exercice a completer : automate pour nombres premiers avec 30\r\n" + "output_type": "stream", + "text": [ + "Exercice a completer : automate pour nombres premiers avec 30\n" + ] } ], "source": [ @@ -1737,10 +2179,10 @@ "id": "808d1734-2307-4aff-8eb9-aff5cf972b81", "metadata": { "papermill": { - "duration": 0.007283, - "end_time": "2026-07-08T06:06:22.118994+00:00", + "duration": 0.004614, + "end_time": "2026-10-03T06:38:17.247640+00:00", "exception": false, - "start_time": "2026-07-08T06:06:22.111711+00:00", + "start_time": "2026-10-03T06:38:17.243026+00:00", "status": "completed" }, "tags": [] @@ -1780,6 +2222,24 @@ } ], "metadata": { + "cost": { + "api_provider": "none", + "api_usd_est": 0.0, + "cpu_min": 4, + "external_account": "none", + "free_alternative": "self", + "gpu_min": 0, + "gpu_required": false, + "metadata_written": "2026-08-03", + "network": true, + "notes": "Automates symboliques (DFA/NFA hand-rolled) + solveur Z3 (Microsoft.Z3 nuget 4.12.2) pour equivalence/emptiness. .NET Interactive C#. 14 cellules executees, CPU pur deterministe. network=true (restore NuGet Microsoft.Z3). ~4 min CPU.", + "qcc_tokens_est": 0, + "reduced_pedagogical": null, + "reproducibility": "HIGH", + "validator": "manual", + "vram_gb": 0, + "vram_tier": "NONE" + }, "kernelspec": { "display_name": ".NET (C#)", "language": "C#", @@ -1792,25 +2252,19 @@ "pygments_lexer": "csharp", "version": "13.0" }, - "cost": { - "api_usd_est": 0.0, - "api_provider": "none", - "qcc_tokens_est": 0, - "cpu_min": 4, - "gpu_min": 0, - "gpu_required": false, - "vram_gb": 0, - "vram_tier": "NONE", - "network": true, - "external_account": "none", - "free_alternative": "self", - "reduced_pedagogical": null, - "reproducibility": "HIGH", - "metadata_written": "2026-08-03", - "validator": "manual", - "notes": "Automates symboliques (DFA/NFA hand-rolled) + solveur Z3 (Microsoft.Z3 nuget 4.12.2) pour equivalence/emptiness. .NET Interactive C#. 14 cellules executees, CPU pur deterministe. network=true (restore NuGet Microsoft.Z3). ~4 min CPU." + "papermill": { + "default_parameters": {}, + "duration": 17.055283, + "end_time": "2026-10-03T06:38:17.368847+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Search-10-SymbolicAutomata-CSharp.ipynb", + "output_path": "Search-10-SymbolicAutomata-CSharp.ipynb", + "parameters": {}, + "start_time": "2026-10-03T06:38:00.313564+00:00", + "version": "2.7.0" } }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-CSharp.ipynb b/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-CSharp.ipynb index d4af52b8ae..de44d31313 100644 --- a/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-CSharp.ipynb +++ b/MyIA.AI.Notebooks/Sudoku/Sudoku-12-Z3-CSharp.ipynb @@ -4,6 +4,13 @@ "cell_type": "markdown", "id": "89962877", "metadata": { + "papermill": { + "duration": 0.009468, + "end_time": "2026-10-03T06:34:59.807562+00:00", + "exception": false, + "start_time": "2026-10-03T06:34:59.798094+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -42,7 +49,9 @@ "- [Programming Z3](https://theory.stanford.edu/~nikolaj/programmingz3.html)\n", "- [Z3Py Guide Examples](https://ericpony.github.io/z3py-tutorial/guide-examples.htm) en Python\n", "\n", - "## Configuration de l'environnement" + "## Configuration de l'environnement\n", + "\n", + "La cellule suivante restaure le package NuGet `Microsoft.Z3`. Sous Linux et sous macOS Apple Silicon, ce package ne contient pas la bibliothèque native de Z3 : la cellule charge alors celle du paquet Python `z3-solver`, par `Z3NativeLoader.cs` de la série [Z3-API](../SymbolicAI/SMT/Z3-API/README.md) (voir l'en-tête du fichier). Pour utiliser la même version de Z3 que le package NuGet : `pip install z3-solver==4.12.2.0`." ] }, { @@ -53,6 +62,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:34:59.833159Z", + "iopub.status.busy": "2026-10-03T06:34:59.823436Z", + "iopub.status.idle": "2026-10-03T06:35:05.573955Z", + "shell.execute_reply": "2026-10-03T06:35:05.568551Z" + }, + "papermill": { + "duration": 5.761502, + "end_time": "2026-10-03T06:35:05.574081+00:00", + "exception": false, + "start_time": "2026-10-03T06:34:59.812579+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -60,28 +82,149 @@ }, "outputs": [ { - "output_type": "display_data", "data": { - "text/html": "" + "text/html": [ + "\r\n", + "
\r\n", + " \r\n", + " \r\n", + "
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
  • Microsoft.Z3
" + "text/html": [ + "
Installed Packages
  • Microsoft.Z3, 4.12.2
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ - "#r \"nuget: Microsoft.Z3\"" + "#r \"nuget: Microsoft.Z3\"\n", + "#load \"../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs\"\n", + "\n", + "// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)\n", + "Z3NativeLoader.Register(typeof(Microsoft.Z3.Context).Assembly);" ] }, { "cell_type": "markdown", "id": "5f811f2c", "metadata": { + "papermill": { + "duration": 0.003543, + "end_time": "2026-10-03T06:35:05.581640+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:05.578097+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -98,6 +241,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:05.591829Z", + "iopub.status.busy": "2026-10-03T06:35:05.591637Z", + "iopub.status.idle": "2026-10-03T06:35:13.630230Z", + "shell.execute_reply": "2026-10-03T06:35:13.630005Z" + }, + "papermill": { + "duration": 8.044479, + "end_time": "2026-10-03T06:35:13.630330+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:05.585851+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -105,94 +261,215 @@ }, "outputs": [ { - "output_type": "display_data", "data": { - "text/markdown": "# Sudoku-00 : Environnement et Classes de Base (C#)\n\n**Navigation** : [Index](README.md) | [Sudoku-01 Backtracking C# >>](Sudoku-01-Backtracking-CSharp.ipynb)\n\n## Objectifs d'apprentissage\n\nÀ la fin de ce notebook, vous saurez :\n1. Comprendre la structure de données `SudokuGrid` et ses méthodes principales\n2. Utiliser `ISudokuSolver` pour implémenter un solveur de Sudoku\n3. Exploiter `SudokuHelper` pour charger des grilles et tester des solveurs\n4. Comparer les performances de plusieurs solveurs sur différentes difficultés\n\n**Prérequis** : Notions de base en C# (.NET Interactive) \n**Durée estimée** : ~15 min" + "text/markdown": [ + "# Sudoku-00 : Environnement et Classes de Base (C#)\n", + "\n", + "**Navigation** : [Index](README.md) | [Sudoku-01 Backtracking C# >>](Sudoku-01-Backtracking-CSharp.ipynb)\n", + "\n", + "## Objectifs d'apprentissage\n", + "\n", + "À la fin de ce notebook, vous saurez :\n", + "1. Comprendre la structure de données `SudokuGrid` et ses méthodes principales\n", + "2. Utiliser `ISudokuSolver` pour implémenter un solveur de Sudoku\n", + "3. Exploiter `SudokuHelper` pour charger des grilles et tester des solveurs\n", + "4. Comparer les performances de plusieurs solveurs sur différentes difficultés\n", + "\n", + "**Prérequis** : Notions de base en C# (.NET Interactive) \n", + "**Durée estimée** : ~15 min" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/html": "
Installing Packages
  • Plotly.NET
" + "text/html": [ + "
Installed Packages
  • Plotly.NET, 5.1.0
" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/markdown": "## Définition de la classe SudokuGrid\n\nNous définissons ici la classe SudokuGrid qui représente une grille de Sudoku et fournit des méthodes pour manipuler et afficher les grilles.\n" + "text/markdown": [ + "## Définition de la classe SudokuGrid\n", + "\n", + "Nous définissons ici la classe SudokuGrid qui représente une grille de Sudoku et fournit des méthodes pour manipuler et afficher les grilles.\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "SudokuGrid defini.\r\n" + "output_type": "stream", + "text": [ + "SudokuGrid defini.\n" + ] }, { - "output_type": "display_data", "data": { - "text/markdown": "### Interprétation : Structure de données pour la grille Sudoku\n\n**Sortie obtenue** : La classe `SudokuGrid` encapsule toutes les opérations de manipulation, validation et affichage d'une grille de Sudoku 9x9.\n\n| Aspect | Valeur | Signification |\n|--------|--------|---------------|\n| `Cells[9,9]` | int[,] | Stockage interne des valeurs (0 = vide) |\n| `AllNeighbours` | 27 x 9 positions | Pré-calcul des voisins ligne/colonne/bloc |\n| `CellNeighbours[9][9]` | ~20 positions chacune | Voisins directs de chaque cellule |\n| `GetAvailableNumbers()` | int[] | Candidats valides pour une cellule |\n| `NbErrors()` | int | Nombre de conflits + modifications erronées |\n\n**Points clés** :\n1. **Pré-calcul des voisins** : `AllNeighbours` et `CellNeighbours` sont calculés une seule fois à l'initialisation, évitant les recalculs coûteux\n2. **Conversion flexible** : Méthodes pour convertir entre tableaux 1D, 2D et jagged arrays (utile pour différents formats de fichiers)\n3. **Validation robuste** : `NbErrors` compte à la fois les doublons (ligne/colonne/bloc) et les modifications de indices pré-remplis\n4. **Parsing tolerant** : `ReadMultiSudoku` accepte plusieurs formats (`.`, `X`, `-`, espaces)\n\n> **Note technique** : La structure `CellNeighbours[i][j]` contient environ 20 positions (8 ligne + 8 colonne + 4 bloc, moins les doublons). Ce pré-calcul est crucial pour les performances des algorithmes de backtracking et de propagation de contraintes." + "text/markdown": [ + "### Interprétation : Structure de données pour la grille Sudoku\n", + "\n", + "**Sortie obtenue** : La classe `SudokuGrid` encapsule toutes les opérations de manipulation, validation et affichage d'une grille de Sudoku 9x9.\n", + "\n", + "| Aspect | Valeur | Signification |\n", + "|--------|--------|---------------|\n", + "| `Cells[9,9]` | int[,] | Stockage interne des valeurs (0 = vide) |\n", + "| `AllNeighbours` | 27 x 9 positions | Pré-calcul des voisins ligne/colonne/bloc |\n", + "| `CellNeighbours[9][9]` | ~20 positions chacune | Voisins directs de chaque cellule |\n", + "| `GetAvailableNumbers()` | int[] | Candidats valides pour une cellule |\n", + "| `NbErrors()` | int | Nombre de conflits + modifications erronées |\n", + "\n", + "**Points clés** :\n", + "1. **Pré-calcul des voisins** : `AllNeighbours` et `CellNeighbours` sont calculés une seule fois à l'initialisation, évitant les recalculs coûteux\n", + "2. **Conversion flexible** : Méthodes pour convertir entre tableaux 1D, 2D et jagged arrays (utile pour différents formats de fichiers)\n", + "3. **Validation robuste** : `NbErrors` compte à la fois les doublons (ligne/colonne/bloc) et les modifications de indices pré-remplis\n", + "4. **Parsing tolerant** : `ReadMultiSudoku` accepte plusieurs formats (`.`, `X`, `-`, espaces)\n", + "\n", + "> **Note technique** : La structure `CellNeighbours[i][j]` contient environ 20 positions (8 ligne + 8 colonne + 4 bloc, moins les doublons). Ce pré-calcul est crucial pour les performances des algorithmes de backtracking et de propagation de contraintes." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/markdown": "## Définition de l'interface ISudokuSolver\n\nNous définissons ici l'interface ISudokuSolver qui sera implémentée par les différentes stratégies de résolution de Sudoku.\n" + "text/markdown": [ + "## Définition de l'interface ISudokuSolver\n", + "\n", + "Nous définissons ici l'interface ISudokuSolver qui sera implémentée par les différentes stratégies de résolution de Sudoku.\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "ISudokuSolver defini.\r\n" + "output_type": "stream", + "text": [ + "ISudokuSolver defini.\n" + ] }, { - "output_type": "display_data", "data": { - "text/markdown": "### Interprétation : Interface de stratégie\n\n**Sortie obtenue** : L'interface `ISudokuSolver` définit le contrat que tous les solveurs doivent respecter.\n\n| Aspect | Valeur | Signification |\n|--------|--------|---------------|\n| `Solve(SudokuGrid)` | SudokuGrid | Méthode unique de résolution |\n| Pattern | Stratégie | Permuter les algorithmes sans modifier le code client |\n\n**Points clés** :\n1. **Simplicité** : Une seule méthode `Solve` prenant une grille et retournant une grille résolue\n2. **Flexibilité** : N'importe quel algorithme (backtracking, CSP, métaheuristique) peut implémenter cette interface\n3. **Composabilité** : Les solveurs peuvent être passés en paramètre, stockés dans des listes, testés unitairement\n4. **Extensibilité** : Ajouter un nouveau solver ne nécessite que d'implémenter l'interface\n\n> **Note technique** : Ce design pattern permet à `SudokuHelper.TestSolvers` d'accepter une liste de `(string, ISudokuSolver)` pour comparer tous les algorithmes avec le même code de test." + "text/markdown": [ + "### Interprétation : Interface de stratégie\n", + "\n", + "**Sortie obtenue** : L'interface `ISudokuSolver` définit le contrat que tous les solveurs doivent respecter.\n", + "\n", + "| Aspect | Valeur | Signification |\n", + "|--------|--------|---------------|\n", + "| `Solve(SudokuGrid)` | SudokuGrid | Méthode unique de résolution |\n", + "| Pattern | Stratégie | Permuter les algorithmes sans modifier le code client |\n", + "\n", + "**Points clés** :\n", + "1. **Simplicité** : Une seule méthode `Solve` prenant une grille et retournant une grille résolue\n", + "2. **Flexibilité** : N'importe quel algorithme (backtracking, CSP, métaheuristique) peut implémenter cette interface\n", + "3. **Composabilité** : Les solveurs peuvent être passés en paramètre, stockés dans des listes, testés unitairement\n", + "4. **Extensibilité** : Ajouter un nouveau solver ne nécessite que d'implémenter l'interface\n", + "\n", + "> **Note technique** : Ce design pattern permet à `SudokuHelper.TestSolvers` d'accepter une liste de `(string, ISudokuSolver)` pour comparer tous les algorithmes avec le même code de test." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/markdown": "## Définition de la classe SudokuHelper\n\nNous ajoutons ici la classe SudokuHelper qui contient des méthodes utilitaires pour charger des grilles de Sudoku et tester des solvers.\n\n- `GetSudokus` : Renvoie des listes de Sudoku issues de fichiers de 3 difficultés différentes.\n- `SolveSudoku` : effectue un test simple d'un solver sur un sudoku donné.\n- `TestSolvers` : exécute les tests de performance sur plusieurs solveurs.\n- `DisplayResults` : affiche les résultats des tests sous forme de graphiques.\n\n" + "text/markdown": [ + "## Définition de la classe SudokuHelper\n", + "\n", + "Nous ajoutons ici la classe SudokuHelper qui contient des méthodes utilitaires pour charger des grilles de Sudoku et tester des solvers.\n", + "\n", + "- `GetSudokus` : Renvoie des listes de Sudoku issues de fichiers de 3 difficultés différentes.\n", + "- `SolveSudoku` : effectue un test simple d'un solver sur un sudoku donné.\n", + "- `TestSolvers` : exécute les tests de performance sur plusieurs solveurs.\n", + "- `DisplayResults` : affiche les résultats des tests sous forme de graphiques.\n", + "\n" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "SudokuHelper defini.\r\n" + "output_type": "stream", + "text": [ + "SudokuHelper defini.\n" + ] }, { - "output_type": "display_data", "data": { - "text/markdown": "### Interprétation : Infrastructure de test et benchmark\n\n**Sortie obtenue** : La classe `SudokuHelper` fournit une infrastructure complète pour tester et comparer les solveurs de Sudoku.\n\n| Aspect | Valeur | Signification |\n|--------|--------|---------------|\n| `GetSudokus()` | 51/95/100 grilles | Trois niveaux de difficulté (Easy/Medium/Hard) |\n| `TestSolvers()` | Performance multi-solveurs | Exécution parallèle avec timeout |\n| `DisplayResults()` | Graphiques SVG inline (SvgChartHelper) | Comparaison des temps par difficulté, sérialisée dans le notebook |\n| `SolveSudoku()` | Test unitaire | Résolution individuelle avec affichage |\n\n**Points clés** :\n1. **Chargement intelligent** : Recherche récursive du dossier `Puzzles` dans l'arborescence\n2. **Robustesse** : Gestion des timeouts (3 000 ms par défaut — paramètre de configuration du solveur, valeur fixée dans le code) et exceptions\n3. **Mesures** : Temps d'exécution total + nombre de grilles resolues\n4. **Disqualification** : Un solver échouant sur une grille est disqualifié pour la difficulté\n\n> **Note technique** : La méthode `TestSolvers` utilise `Interlocked.Increment` pour un thread-safe incrément du compteur de solutions. Le `CancellationToken` permet d'interrompre proprement les solveurs trop lents." + "text/markdown": [ + "### Interprétation : Infrastructure de test et benchmark\n", + "\n", + "**Sortie obtenue** : La classe `SudokuHelper` fournit une infrastructure complète pour tester et comparer les solveurs de Sudoku.\n", + "\n", + "| Aspect | Valeur | Signification |\n", + "|--------|--------|---------------|\n", + "| `GetSudokus()` | 51/95/100 grilles | Trois niveaux de difficulté (Easy/Medium/Hard) |\n", + "| `TestSolvers()` | Performance multi-solveurs | Exécution parallèle avec timeout |\n", + "| `DisplayResults()` | Graphiques SVG inline (SvgChartHelper) | Comparaison des temps par difficulté, sérialisée dans le notebook |\n", + "| `SolveSudoku()` | Test unitaire | Résolution individuelle avec affichage |\n", + "\n", + "**Points clés** :\n", + "1. **Chargement intelligent** : Recherche récursive du dossier `Puzzles` dans l'arborescence\n", + "2. **Robustesse** : Gestion des timeouts (3 000 ms par défaut — paramètre de configuration du solveur, valeur fixée dans le code) et exceptions\n", + "3. **Mesures** : Temps d'exécution total + nombre de grilles resolues\n", + "4. **Disqualification** : Un solver échouant sur une grille est disqualifié pour la difficulté\n", + "\n", + "> **Note technique** : La méthode `TestSolvers` utilise `Interlocked.Increment` pour un thread-safe incrément du compteur de solutions. Le `CancellationToken` permet d'interrompre proprement les solveurs trop lents." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/markdown": "## Exercice : Validation d'une grille Sudoku\n\n### Énoncé\n\nImplémentez une méthode `IsValidSolution` qui vérifie qu'une grille est une solution valide de Sudoku, c'est-à-dire que chaque ligne, chaque colonne et chaque bloc 3x3 contient exactement une fois chaque chiffre de 1 à 9.\n\nUtilisez cette méthode pour valider les résultats de `SudokuHelper.SolveSudoku`.\n\n**Indices :**\n\n- Parcourez les 9 lignes, 9 colonnes et 9 blocs\n- Pour chaque unité, verifiez que les 9 chiffres sont tous présents sans doublon\n- `SudokuGrid.AllNeighbours` contient déjà les indices des unités" + "text/markdown": [ + "## Exercice : Validation d'une grille Sudoku\n", + "\n", + "### Énoncé\n", + "\n", + "Implémentez une méthode `IsValidSolution` qui vérifie qu'une grille est une solution valide de Sudoku, c'est-à-dire que chaque ligne, chaque colonne et chaque bloc 3x3 contient exactement une fois chaque chiffre de 1 à 9.\n", + "\n", + "Utilisez cette méthode pour valider les résultats de `SudokuHelper.SolveSudoku`.\n", + "\n", + "**Indices :**\n", + "\n", + "- Parcourez les 9 lignes, 9 colonnes et 9 blocs\n", + "- Pour chaque unité, verifiez que les 9 chiffres sont tous présents sans doublon\n", + "- `SudokuGrid.AllNeighbours` contient déjà les indices des unités" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "Exercice a completer\r\n" + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] }, { - "output_type": "display_data", "data": { - "text/markdown": "## Résumé et perspectives\n\nCe notebook a posé les fondations de toute la série Sudoku en définissant trois composants essentiels. La classe `SudokuGrid` encapsule la représentation d'une grille 9x9 avec le pré-calcul des voisins (`AllNeighbours`, `CellNeighbours`), ce qui évite les recalculs coûteux lors de la résolution. L'interface `ISudokuSolver` implante le pattern Stratégie, permettant de permuter les algorithmes de résolution sans modifier le code client. Enfin, la classe `SudokuHelper` fournit une infrastructure de benchmark complète avec chargement de puzzles, mesures de performance et visualisation SVG inline (SvgChartHelper, zéro dépendance).\n\nL'infrastructure de test (`TestSolvers`, `DisplayResults`) permet de comparer objectivement les solveurs sur trois niveaux de difficulté (Easy, Medium, Hard) avec gestion des timeouts et des disqualifications. Ce cadre de benchmark sera utilisé dans tous les notebooks suivants pour mesurer les performances de chaque algorithme.\n\nLe notebook suivant, [Sudoku-01-Backtracking](Sudoku-01-Backtracking-CSharp.ipynb), utilise ces classes pour implémenter le premier algorithme de résolution : le backtracking récursif avec ses heuristiques d'amélioration." + "text/markdown": [ + "## Résumé et perspectives\n", + "\n", + "Ce notebook a posé les fondations de toute la série Sudoku en définissant trois composants essentiels. La classe `SudokuGrid` encapsule la représentation d'une grille 9x9 avec le pré-calcul des voisins (`AllNeighbours`, `CellNeighbours`), ce qui évite les recalculs coûteux lors de la résolution. L'interface `ISudokuSolver` implante le pattern Stratégie, permettant de permuter les algorithmes de résolution sans modifier le code client. Enfin, la classe `SudokuHelper` fournit une infrastructure de benchmark complète avec chargement de puzzles, mesures de performance et visualisation SVG inline (SvgChartHelper, zéro dépendance).\n", + "\n", + "L'infrastructure de test (`TestSolvers`, `DisplayResults`) permet de comparer objectivement les solveurs sur trois niveaux de difficulté (Easy, Medium, Hard) avec gestion des timeouts et des disqualifications. Ce cadre de benchmark sera utilisé dans tous les notebooks suivants pour mesurer les performances de chaque algorithme.\n", + "\n", + "Le notebook suivant, [Sudoku-01-Backtracking](Sudoku-01-Backtracking-CSharp.ipynb), utilise ces classes pour implémenter le premier algorithme de résolution : le backtracking récursif avec ses heuristiques d'amélioration." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -203,6 +480,13 @@ "cell_type": "markdown", "id": "f93d667a", "metadata": { + "papermill": { + "duration": 0.004908, + "end_time": "2026-10-03T06:35:13.640898+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.635990+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -219,6 +503,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:13.652245Z", + "iopub.status.busy": "2026-10-03T06:35:13.652028Z", + "iopub.status.idle": "2026-10-03T06:35:13.716015Z", + "shell.execute_reply": "2026-10-03T06:35:13.715867Z" + }, + "papermill": { + "duration": 0.070536, + "end_time": "2026-10-03T06:35:13.716094+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.645558+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -226,9 +523,11 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Classe Z3IntSolverSimple definie (solveur Z3 avec entiers)\r\n" + "output_type": "stream", + "text": [ + "Classe Z3IntSolverSimple definie (solveur Z3 avec entiers)\n" + ] } ], "source": [ @@ -367,6 +666,13 @@ "cell_type": "markdown", "id": "demo-int-md", "metadata": { + "papermill": { + "duration": 0.007473, + "end_time": "2026-10-03T06:35:13.728546+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.721073+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -380,33 +686,80 @@ "execution_count": 4, "id": "demo-int-code", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:35:13.739835Z", + "iopub.status.busy": "2026-10-03T06:35:13.739644Z", + "iopub.status.idle": "2026-10-03T06:35:13.871582Z", + "shell.execute_reply": "2026-10-03T06:35:13.871409Z" + }, + "papermill": { + "duration": 0.138136, + "end_time": "2026-10-03T06:35:13.871662+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.733526+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Grille initiale (les 0 sont les cases a remplir) :\r\n" + "output_type": "stream", + "text": [ + "Grille initiale (les 0 sont les cases a remplir) :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "-------------------------------\n| 9 2 | 5 | 4 3 | \n| 1 | 6 3 | 2 5 | \n| 5 8 | 4 7 | 6 | \n-------------------------------\n| 2 6 | 3 9 | 1 | \n| 5 7 | 1 | 2 9 | \n| 9 | 6 7 | 5 3 | \n-------------------------------\n| 2 4 | 5 3 | 6 | \n| 7 5 | 2 | 3 4 | \n| 8 | 4 1 | 9 5 | \n-------------------------------\r\n" + "output_type": "stream", + "text": [ + "-------------------------------\n", + "| 9 2 | 5 | 4 3 | \n", + "| 1 | 6 3 | 2 5 | \n", + "| 5 8 | 4 7 | 6 | \n", + "-------------------------------\n", + "| 2 6 | 3 9 | 1 | \n", + "| 5 7 | 1 | 2 9 | \n", + "| 9 | 6 7 | 5 3 | \n", + "-------------------------------\n", + "| 2 4 | 5 3 | 6 | \n", + "| 7 5 | 2 | 3 4 | \n", + "| 8 | 4 1 | 9 5 | \n", + "-------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Grille resolue par Z3IntSolverSimple :\r\n" + "output_type": "stream", + "text": [ + "Grille resolue par Z3IntSolverSimple :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "-------------------------------\n| 9 6 2 | 1 8 5 | 4 7 3 | \n| 1 7 4 | 9 6 3 | 8 2 5 | \n| 5 3 8 | 4 2 7 | 1 6 9 | \n-------------------------------\n| 8 2 6 | 3 5 9 | 7 4 1 | \n| 3 5 7 | 8 1 4 | 2 9 6 | \n| 4 9 1 | 6 7 2 | 5 3 8 | \n-------------------------------\n| 2 4 9 | 5 3 8 | 6 1 7 | \n| 7 1 5 | 2 9 6 | 3 8 4 | \n| 6 8 3 | 7 4 1 | 9 5 2 | \n-------------------------------\r\n" + "output_type": "stream", + "text": [ + "-------------------------------\n", + "| 9 6 2 | 1 8 5 | 4 7 3 | \n", + "| 1 7 4 | 9 6 3 | 8 2 5 | \n", + "| 5 3 8 | 4 2 7 | 1 6 9 | \n", + "-------------------------------\n", + "| 8 2 6 | 3 5 9 | 7 4 1 | \n", + "| 3 5 7 | 8 1 4 | 2 9 6 | \n", + "| 4 9 1 | 6 7 2 | 5 3 8 | \n", + "-------------------------------\n", + "| 2 4 9 | 5 3 8 | 6 1 7 | \n", + "| 7 1 5 | 2 9 6 | 3 8 4 | \n", + "| 6 8 3 | 7 4 1 | 9 5 2 | \n", + "-------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Nombre d'erreurs restantes (0 = grille valide) : 0\r\n" + "output_type": "stream", + "text": [ + "Nombre d'erreurs restantes (0 = grille valide) : 0\n" + ] } ], "source": [ @@ -425,6 +778,13 @@ "cell_type": "markdown", "id": "dbdb820e", "metadata": { + "papermill": { + "duration": 0.005088, + "end_time": "2026-10-03T06:35:13.886207+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.881119+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -443,6 +803,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:13.898042Z", + "iopub.status.busy": "2026-10-03T06:35:13.897707Z", + "iopub.status.idle": "2026-10-03T06:35:13.957160Z", + "shell.execute_reply": "2026-10-03T06:35:13.957007Z" + }, + "papermill": { + "duration": 0.065965, + "end_time": "2026-10-03T06:35:13.957243+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.891278+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -450,9 +823,11 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Classe Z3BitVectorSolverBase definie (solveur Z3 abstrait avec vecteurs de bits)\r\n" + "output_type": "stream", + "text": [ + "Classe Z3BitVectorSolverBase definie (solveur Z3 abstrait avec vecteurs de bits)\n" + ] } ], "source": [ @@ -598,6 +973,13 @@ "cell_type": "markdown", "id": "3f116202", "metadata": { + "papermill": { + "duration": 0.004871, + "end_time": "2026-10-03T06:35:13.967700+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.962829+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -610,6 +992,13 @@ "cell_type": "markdown", "id": "add29da2", "metadata": { + "papermill": { + "duration": 0.004629, + "end_time": "2026-10-03T06:35:13.977325+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.972696+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -627,6 +1016,19 @@ "execution_count": 6, "id": "71c3588f", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:35:13.995956Z", + "iopub.status.busy": "2026-10-03T06:35:13.995794Z", + "iopub.status.idle": "2026-10-03T06:35:14.025448Z", + "shell.execute_reply": "2026-10-03T06:35:14.025307Z" + }, + "papermill": { + "duration": 0.042846, + "end_time": "2026-10-03T06:35:14.025569+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:13.982723+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [], @@ -648,6 +1050,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.037348Z", + "iopub.status.busy": "2026-10-03T06:35:14.036330Z", + "iopub.status.idle": "2026-10-03T06:35:14.064532Z", + "shell.execute_reply": "2026-10-03T06:35:14.064281Z" + }, + "papermill": { + "duration": 0.034225, + "end_time": "2026-10-03T06:35:14.064639+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.030414+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -655,9 +1070,11 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Classe Z3BitVectorSolverSimple definie (solveur Z3 BitVector simple)\r\n" + "output_type": "stream", + "text": [ + "Classe Z3BitVectorSolverSimple definie (solveur Z3 BitVector simple)\n" + ] } ], "source": [ @@ -706,6 +1123,13 @@ "cell_type": "markdown", "id": "demo-bv-md", "metadata": { + "papermill": { + "duration": 0.005081, + "end_time": "2026-10-03T06:35:14.075713+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.070632+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -719,33 +1143,80 @@ "execution_count": 8, "id": "demo-bv-code", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.087196Z", + "iopub.status.busy": "2026-10-03T06:35:14.086989Z", + "iopub.status.idle": "2026-10-03T06:35:14.152063Z", + "shell.execute_reply": "2026-10-03T06:35:14.151880Z" + }, + "papermill": { + "duration": 0.071724, + "end_time": "2026-10-03T06:35:14.152136+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.080412+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Grille initiale :\r\n" + "output_type": "stream", + "text": [ + "Grille initiale :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "-------------------------------\n| 9 2 | 5 | 4 3 | \n| 1 | 6 3 | 2 5 | \n| 5 8 | 4 7 | 6 | \n-------------------------------\n| 2 6 | 3 9 | 1 | \n| 5 7 | 1 | 2 9 | \n| 9 | 6 7 | 5 3 | \n-------------------------------\n| 2 4 | 5 3 | 6 | \n| 7 5 | 2 | 3 4 | \n| 8 | 4 1 | 9 5 | \n-------------------------------\r\n" + "output_type": "stream", + "text": [ + "-------------------------------\n", + "| 9 2 | 5 | 4 3 | \n", + "| 1 | 6 3 | 2 5 | \n", + "| 5 8 | 4 7 | 6 | \n", + "-------------------------------\n", + "| 2 6 | 3 9 | 1 | \n", + "| 5 7 | 1 | 2 9 | \n", + "| 9 | 6 7 | 5 3 | \n", + "-------------------------------\n", + "| 2 4 | 5 3 | 6 | \n", + "| 7 5 | 2 | 3 4 | \n", + "| 8 | 4 1 | 9 5 | \n", + "-------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Grille resolue par Z3BitVectorSolverSimple :\r\n" + "output_type": "stream", + "text": [ + "Grille resolue par Z3BitVectorSolverSimple :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "-------------------------------\n| 9 6 2 | 1 8 5 | 4 7 3 | \n| 1 7 4 | 9 6 3 | 8 2 5 | \n| 5 3 8 | 4 2 7 | 1 6 9 | \n-------------------------------\n| 8 2 6 | 3 5 9 | 7 4 1 | \n| 3 5 7 | 8 1 4 | 2 9 6 | \n| 4 9 1 | 6 7 2 | 5 3 8 | \n-------------------------------\n| 2 4 9 | 5 3 8 | 6 1 7 | \n| 7 1 5 | 2 9 6 | 3 8 4 | \n| 6 8 3 | 7 4 1 | 9 5 2 | \n-------------------------------\r\n" + "output_type": "stream", + "text": [ + "-------------------------------\n", + "| 9 6 2 | 1 8 5 | 4 7 3 | \n", + "| 1 7 4 | 9 6 3 | 8 2 5 | \n", + "| 5 3 8 | 4 2 7 | 1 6 9 | \n", + "-------------------------------\n", + "| 8 2 6 | 3 5 9 | 7 4 1 | \n", + "| 3 5 7 | 8 1 4 | 2 9 6 | \n", + "| 4 9 1 | 6 7 2 | 5 3 8 | \n", + "-------------------------------\n", + "| 2 4 9 | 5 3 8 | 6 1 7 | \n", + "| 7 1 5 | 2 9 6 | 3 8 4 | \n", + "| 6 8 3 | 7 4 1 | 9 5 2 | \n", + "-------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Nombre d'erreurs restantes (0 = grille valide) : 0\r\n" + "output_type": "stream", + "text": [ + "Nombre d'erreurs restantes (0 = grille valide) : 0\n" + ] } ], "source": [ @@ -764,6 +1235,13 @@ "cell_type": "markdown", "id": "isz12-enc", "metadata": { + "papermill": { + "duration": 0.005413, + "end_time": "2026-10-03T06:35:14.162770+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.157357+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -781,6 +1259,13 @@ "cell_type": "markdown", "id": "326bf677", "metadata": { + "papermill": { + "duration": 0.007627, + "end_time": "2026-10-03T06:35:14.178416+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.170789+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -797,6 +1282,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.195218Z", + "iopub.status.busy": "2026-10-03T06:35:14.195064Z", + "iopub.status.idle": "2026-10-03T06:35:14.227518Z", + "shell.execute_reply": "2026-10-03T06:35:14.227335Z" + }, + "papermill": { + "duration": 0.040237, + "end_time": "2026-10-03T06:35:14.227588+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.187351+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -804,9 +1302,11 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Classe Z3BitVectorSolverSubstitution definie (solveur Z3 avec substitution)\r\n" + "output_type": "stream", + "text": [ + "Classe Z3BitVectorSolverSubstitution definie (solveur Z3 avec substitution)\n" + ] } ], "source": [ @@ -872,6 +1372,13 @@ "cell_type": "markdown", "id": "29d71930", "metadata": { + "papermill": { + "duration": 0.005063, + "end_time": "2026-10-03T06:35:14.238253+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.233190+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -888,6 +1395,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.250236Z", + "iopub.status.busy": "2026-10-03T06:35:14.250065Z", + "iopub.status.idle": "2026-10-03T06:35:14.283956Z", + "shell.execute_reply": "2026-10-03T06:35:14.283749Z" + }, + "papermill": { + "duration": 0.040503, + "end_time": "2026-10-03T06:35:14.284030+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.243527+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -895,9 +1415,11 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Classe Z3BitSub_Tactic definie (solveur Z3 avec tactiques)\r\n" + "output_type": "stream", + "text": [ + "Classe Z3BitSub_Tactic definie (solveur Z3 avec tactiques)\n" + ] } ], "source": [ @@ -975,6 +1497,13 @@ "cell_type": "markdown", "id": "008967cc", "metadata": { + "papermill": { + "duration": 0.004024, + "end_time": "2026-10-03T06:35:14.292830+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.288806+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -987,6 +1516,13 @@ "cell_type": "markdown", "id": "d0583d20", "metadata": { + "papermill": { + "duration": 0.004191, + "end_time": "2026-10-03T06:35:14.301212+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.297021+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1006,6 +1542,19 @@ "execution_count": 11, "id": "37a27e98", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.310989Z", + "iopub.status.busy": "2026-10-03T06:35:14.310795Z", + "iopub.status.idle": "2026-10-03T06:35:14.326665Z", + "shell.execute_reply": "2026-10-03T06:35:14.326506Z" + }, + "papermill": { + "duration": 0.021498, + "end_time": "2026-10-03T06:35:14.326718+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.305220+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [], @@ -1027,6 +1576,19 @@ "dotnet_interactive": { "language": "csharp" }, + "execution": { + "iopub.execute_input": "2026-10-03T06:35:14.336187Z", + "iopub.status.busy": "2026-10-03T06:35:14.336035Z", + "iopub.status.idle": "2026-10-03T06:35:17.171881Z", + "shell.execute_reply": "2026-10-03T06:35:17.171664Z" + }, + "papermill": { + "duration": 2.841173, + "end_time": "2026-10-03T06:35:17.171977+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:14.330804+00:00", + "status": "completed" + }, "polyglot_notebook": { "kernelName": "csharp" }, @@ -1034,102 +1596,138 @@ }, "outputs": [ { - "output_type": "display_data", "data": { - "text/plain": "Running tests..." + "text/plain": [ + "Running tests..." + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", - "text": "Encodage Difficulte Temps (ms) Resolus Statut\r\n" + "output_type": "stream", + "text": [ + "Encodage Difficulte Temps (ms) Resolus Statut\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "------------------------------------------------------------------------------------\r\n" + "output_type": "stream", + "text": [ + "------------------------------------------------------------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Int Solver Simple Easy 174,1 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Int Solver Simple Easy 102,1 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Int Solver Simple Medium 588,0 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Int Solver Simple Medium 376,7 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Int Solver Simple Hard 958,5 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Int Solver Simple Hard 572,8 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Simple Easy 156,9 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Simple Easy 179,6 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Simple Medium 254,1 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Simple Medium 159,4 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Simple Hard 438,7 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Simple Hard 244,1 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Substitution Easy 179,3 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Substitution Easy 149,8 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Substitution Medium 319,6 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Substitution Medium 161,2 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Substitution Hard 332,2 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Substitution Hard 191,3 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Tactic Easy 213,3 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Tactic Easy 148,4 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Tactic Medium 348,2 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Tactic Medium 210,4 3 Success\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Z3 Bit Vector Solver Tactic Hard 370,1 3 Success\r\n" + "output_type": "stream", + "text": [ + "Z3 Bit Vector Solver Tactic Hard 250,7 3 Success\n" + ] }, { - "output_type": "display_data", "data": { - "text/html": "Comparaison des solveurs - difficulte Easy (temps total, ms)057.589115.179172.768230.358Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + "text/html": [ + "Comparaison des solveurs - difficulte Easy (temps total, ms)048.49396.987145.48193.973Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/html": "Comparaison des solveurs - difficulte Medium (temps total, ms)0158.772317.545476.317635.09Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + "text/html": [ + "Comparaison des solveurs - difficulte Medium (temps total, ms)0101.706203.411305.117406.822Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "display_data", "data": { - "text/html": "Comparaison des solveurs - difficulte Hard (temps total, ms)0258.802517.604776.4051035.207Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + "text/html": [ + "Comparaison des solveurs - difficulte Hard (temps total, ms)0154.652309.304463.956618.607Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic" + ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -1160,6 +1758,13 @@ "cell_type": "markdown", "id": "8af4bf6c", "metadata": { + "papermill": { + "duration": 0.006118, + "end_time": "2026-10-03T06:35:17.184565+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:17.178447+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1167,7 +1772,7 @@ "\n", "La cellule précédente lance le banc d'essai comparatif (`TestSolvers` + `DisplayResults`) sur trois niveaux de difficulté, avec un budget borné (3 grilles par difficulté, 3 s max par grille) afin que la comparaison tienne dans un temps raisonnable. Le tableau texte capture les temps de résolution réels ; les graphiques SVG ci-dessous sont eux aussi sérialisés dans le notebook.\n", "\n", - "Sur l'exécution committee, les quatre encodages résolvent l'intégralité des grilles (statut `Success`, 3/3 à chaque niveau). Le contraste porte sur la **stabilité** : les trois encodages **par vecteurs de bits** dominent sur toutes les difficultés — l'encodage par substitution est le plus rapide en Easy et Medium et les trois restent bien sous la seconde même sur `top95`. L'encodage **entier**, lui, n'est jamais le plus rapide : 3ᵉ sur les grilles faciles (derrière les vecteurs de bits), il **s'effondre** sur les grilles difficiles (environ **3 à 5× les vecteurs de bits** — ordre de grandeur stable d'une machine à l'autre). Les mesures exactes varient d'une exécution à l'autre (contexte partagé, charge machine), mais cette dégradation de l'entier sur `top95` est robuste.\n", + "Sur l'exécution committee, les quatre encodages résolvent l'intégralité des grilles (statut `Success`, 3/3 à chaque niveau). Le contraste porte sur la **stabilité** : les trois encodages **par vecteurs de bits** restent bien sous la seconde même sur `top95`. Sur les grilles faciles, aucun encodage ne domine : leur ordre change d'une exécution à l'autre. L'encodage **entier**, lui, se **dégrade** quand la difficulté monte : sur les grilles difficiles, il est de l'ordre de **2 à 3× plus lent** que chacun des encodages par vecteurs de bits. Les mesures exactes varient d'une exécution à l'autre (contexte partagé, charge machine), mais cette dégradation de l'entier sur `top95` est robuste.\n", "\n", "| Solveur | Approche | Avantages | Inconvénients |\n", "|---------|----------|-----------|---------------|\n", @@ -1184,7 +1789,7 @@ "\n", "3. **Tactiques** : les tactiques comme \"simplify\" pré-traitent les contraintes, mais l'overhead ne se justifie pas toujours pour des Sudoku simples.\n", "\n", - "4. **Performance** : contrairement à ce que suggère l'intuition, les vecteurs de bits prennent l'avantage **dès les grilles faciles** (déjà ~1,5× à 2× plus rapides que l'entier) ; l'écart **se creuse massivement** sur les grilles difficiles, où l'entier devient 3 à 5× plus lent que les vecteurs de bits (temps absolus mesurés dynamiquement par la cellule de banc d'essai ci-dessus, règle #9434). L'intérêt de l'encodage entier est conceptuel (modélisation directe, facile à comprendre), pas la vitesse. Le budget borné du banc d'essai (statut `Timeout` / `Disqualified` possible sur `top95`) fait partie de la mesure : un dépassement est un résultat, pas une erreur.\n", + "4. **Performance** : sur les grilles faciles, aucun encodage ne domine (l'ordre change d'une exécution à l'autre) ; l'écart **se creuse** sur les grilles difficiles, où l'entier devient de l'ordre de 2 à 3× plus lent que les vecteurs de bits (temps absolus mesurés dynamiquement par la cellule de banc d'essai ci-dessus, règle #9434). L'intérêt de l'encodage entier est conceptuel (modélisation directe, facile à comprendre), pas la vitesse. Le budget borné du banc d'essai (statut `Timeout` / `Disqualified` possible sur `top95`) fait partie de la mesure : un dépassement est un résultat, pas une erreur.\n", "\n", "> **Note technique** : les solveurs Z3 utilisent un contexte statique partage pour optimiser la performance. Dans une application de production, il faudrait gerer le cycle de vie du contexte plus proprement." ] @@ -1193,6 +1798,13 @@ "cell_type": "markdown", "id": "2ca3c48e", "metadata": { + "papermill": { + "duration": 0.006011, + "end_time": "2026-10-03T06:35:17.196462+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:17.190451+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1210,43 +1822,70 @@ "execution_count": 13, "id": "cfeff8c4", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:35:17.210111Z", + "iopub.status.busy": "2026-10-03T06:35:17.209906Z", + "iopub.status.idle": "2026-10-03T06:37:56.703098Z", + "shell.execute_reply": "2026-10-03T06:37:56.702964Z" + }, + "papermill": { + "duration": 159.500799, + "end_time": "2026-10-03T06:37:56.703204+00:00", + "exception": false, + "start_time": "2026-10-03T06:35:17.202405+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Statut : SATISFIABLE (optimum) | Reward total maximal : 192\r\n" + "output_type": "stream", + "text": [ + "Statut : SATISFIABLE (optimum) | Reward total maximal : 192\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Carre latin 5x5 optimal (maximise le reward) :\r\n" + "output_type": "stream", + "text": [ + "Carre latin 5x5 optimal (maximise le reward) :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 3 4 2 5 1\r\n" + "output_type": "stream", + "text": [ + " 3 4 2 5 1\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 4 2 5 1 3\r\n" + "output_type": "stream", + "text": [ + " 4 2 5 1 3\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 2 5 1 3 4\r\n" + "output_type": "stream", + "text": [ + " 2 5 1 3 4\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 5 1 3 4 2\r\n" + "output_type": "stream", + "text": [ + " 5 1 3 4 2\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": " 1 3 4 2 5\r\n" + "output_type": "stream", + "text": [ + " 1 3 4 2 5\n" + ] } ], "source": [ @@ -1321,6 +1960,13 @@ "cell_type": "markdown", "id": "isz12-opt", "metadata": { + "papermill": { + "duration": 0.006408, + "end_time": "2026-10-03T06:37:56.717226+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.710818+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1338,6 +1984,13 @@ "cell_type": "markdown", "id": "b6e7de73", "metadata": { + "papermill": { + "duration": 0.006144, + "end_time": "2026-10-03T06:37:56.729975+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.723831+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1357,13 +2010,28 @@ "execution_count": 14, "id": "a316fb8b", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:56.743998Z", + "iopub.status.busy": "2026-10-03T06:37:56.743787Z", + "iopub.status.idle": "2026-10-03T06:37:56.787982Z", + "shell.execute_reply": "2026-10-03T06:37:56.787796Z" + }, + "papermill": { + "duration": 0.052138, + "end_time": "2026-10-03T06:37:56.788066+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.735928+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Implementation a completer pour voir le resultat (non implemente).\r\n" + "output_type": "stream", + "text": [ + "Implementation a completer pour voir le resultat (non implemente).\n" + ] } ], "source": [ @@ -1397,6 +2065,13 @@ "cell_type": "markdown", "id": "fdec7a9b", "metadata": { + "papermill": { + "duration": 0.006911, + "end_time": "2026-10-03T06:37:56.801916+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.795005+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1413,6 +2088,13 @@ "cell_type": "markdown", "id": "abb8c6f4", "metadata": { + "papermill": { + "duration": 0.00714, + "end_time": "2026-10-03T06:37:56.815568+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.808428+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1437,6 +2119,13 @@ "cell_type": "markdown", "id": "940a7420", "metadata": { + "papermill": { + "duration": 0.006954, + "end_time": "2026-10-03T06:37:56.829182+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.822228+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1455,6 +2144,19 @@ "execution_count": 15, "id": "55ada6cd", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:56.843370Z", + "iopub.status.busy": "2026-10-03T06:37:56.843127Z", + "iopub.status.idle": "2026-10-03T06:37:56.862630Z", + "shell.execute_reply": "2026-10-03T06:37:56.862388Z" + }, + "papermill": { + "duration": 0.027358, + "end_time": "2026-10-03T06:37:56.862721+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.835363+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [], @@ -1473,13 +2175,28 @@ "execution_count": 16, "id": "bb6ac47c", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:56.877335Z", + "iopub.status.busy": "2026-10-03T06:37:56.877081Z", + "iopub.status.idle": "2026-10-03T06:37:56.896126Z", + "shell.execute_reply": "2026-10-03T06:37:56.895944Z" + }, + "papermill": { + "duration": 0.027043, + "end_time": "2026-10-03T06:37:56.896193+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.869150+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "TODO : Implementez SudokuXZ3Solver avec les contraintes de diagonale\r\n" + "output_type": "stream", + "text": [ + "TODO : Implementez SudokuXZ3Solver avec les contraintes de diagonale\n" + ] } ], "source": [ @@ -1525,6 +2242,13 @@ "cell_type": "markdown", "id": "713807d9", "metadata": { + "papermill": { + "duration": 0.005896, + "end_time": "2026-10-03T06:37:56.908093+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.902197+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1549,13 +2273,28 @@ "execution_count": 17, "id": "5e3f4e98", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:56.921669Z", + "iopub.status.busy": "2026-10-03T06:37:56.921449Z", + "iopub.status.idle": "2026-10-03T06:37:56.964702Z", + "shell.execute_reply": "2026-10-03T06:37:56.964468Z" + }, + "papermill": { + "duration": 0.050919, + "end_time": "2026-10-03T06:37:56.964787+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.913868+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "TODO : Implementez Z3SudokuUnicityChecker.HasUniqueSolution()\r\n" + "output_type": "stream", + "text": [ + "TODO : Implementez Z3SudokuUnicityChecker.HasUniqueSolution()\n" + ] } ], "source": [ @@ -1610,6 +2349,13 @@ "cell_type": "markdown", "id": "23abb281", "metadata": { + "papermill": { + "duration": 0.006353, + "end_time": "2026-10-03T06:37:56.978884+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.972531+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1634,23 +2380,42 @@ "execution_count": 18, "id": "f6b5e689", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:56.991772Z", + "iopub.status.busy": "2026-10-03T06:37:56.991571Z", + "iopub.status.idle": "2026-10-03T06:37:57.084443Z", + "shell.execute_reply": "2026-10-03T06:37:57.084287Z" + }, + "papermill": { + "duration": 0.09995, + "end_time": "2026-10-03T06:37:57.084548+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:56.984598+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Comparaison des tactiques Z3 :\r\n" + "output_type": "stream", + "text": [ + "Comparaison des tactiques Z3 :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "----------------------------------------\r\n" + "output_type": "stream", + "text": [ + "----------------------------------------\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "TODO : Implementez la comparaison des tactiques Z3\r\n" + "output_type": "stream", + "text": [ + "TODO : Implementez la comparaison des tactiques Z3\n" + ] } ], "source": [ @@ -1692,6 +2457,13 @@ "cell_type": "markdown", "id": "a5cfbbf3", "metadata": { + "papermill": { + "duration": 0.005108, + "end_time": "2026-10-03T06:37:57.095136+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:57.090028+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1723,23 +2495,54 @@ "execution_count": 19, "id": "8a6fd356", "metadata": { + "execution": { + "iopub.execute_input": "2026-10-03T06:37:57.107488Z", + "iopub.status.busy": "2026-10-03T06:37:57.107155Z", + "iopub.status.idle": "2026-10-03T06:37:57.134663Z", + "shell.execute_reply": "2026-10-03T06:37:57.134448Z" + }, + "papermill": { + "duration": 0.034598, + "end_time": "2026-10-03T06:37:57.134735+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:57.100137+00:00", + "status": "completed" + }, "tags": [] }, "outputs": [ { - "output_type": "stream", "name": "stdout", - "text": "Test de verification de proprietes Z3\r\n" + "output_type": "stream", + "text": [ + "Test de verification de proprietes Z3\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "Puzzle selectionne :\r\n" + "output_type": "stream", + "text": [ + "Puzzle selectionne :\n" + ] }, { - "output_type": "stream", "name": "stdout", - "text": "-------------------------------\n| 4 | | 8 5 | \n| 3 | | | \n| | 7 | | \n-------------------------------\n| 2 | | 6 | \n| | 8 | 4 | \n| | 1 | | \n-------------------------------\n| | 6 3 | 7 | \n| 5 | 2 | | \n| 1 4 | | | \n-------------------------------\r\n" + "output_type": "stream", + "text": [ + "-------------------------------\n", + "| 4 | | 8 5 | \n", + "| 3 | | | \n", + "| | 7 | | \n", + "-------------------------------\n", + "| 2 | | 6 | \n", + "| | 8 | 4 | \n", + "| | 1 | | \n", + "-------------------------------\n", + "| | 6 3 | 7 | \n", + "| 5 | 2 | | \n", + "| 1 4 | | | \n", + "-------------------------------\n" + ] } ], "source": [ @@ -1794,6 +2597,13 @@ "cell_type": "markdown", "id": "1923ae48", "metadata": { + "papermill": { + "duration": 0.006028, + "end_time": "2026-10-03T06:37:57.146693+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:57.140665+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1819,6 +2629,13 @@ "cell_type": "markdown", "id": "f1929938", "metadata": { + "papermill": { + "duration": 0.005742, + "end_time": "2026-10-03T06:37:57.158283+00:00", + "exception": false, + "start_time": "2026-10-03T06:37:57.152541+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -1863,6 +2680,18 @@ "pygments_lexer": "csharp", "version": "13.0" }, + "papermill": { + "default_parameters": {}, + "duration": 179.942788, + "end_time": "2026-10-03T06:37:57.281995+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Sudoku-12-Z3-CSharp.ipynb", + "output_path": "Sudoku-12-Z3-CSharp.ipynb", + "parameters": {}, + "start_time": "2026-10-03T06:34:57.339207+00:00", + "version": "2.7.0" + }, "polyglot_notebook": { "kernelInfo": { "defaultKernelName": "csharp", diff --git a/scripts/notebook_tools/twin_pairs.d/search-10-symbolicautomata/0012-2026-10-03-claude-cloud-hors-flotte.yaml b/scripts/notebook_tools/twin_pairs.d/search-10-symbolicautomata/0012-2026-10-03-claude-cloud-hors-flotte.yaml new file mode 100644 index 0000000000..de677e2fa9 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/search-10-symbolicautomata/0012-2026-10-03-claude-cloud-hors-flotte.yaml @@ -0,0 +1,6 @@ +date: '2026-10-03' +by: claude-cloud:hors-flotte +python_sha: 535f2861f13a3b06bd891d7b0e12724872cbe838 +csharp_sha: 07e9445d4d1137509ecfbf31c1824ed9c114cb6d +content_python_sha: 41bac53c96f49157a534c046ae047364376520062918fac6265f81e5716162cc +content_csharp_sha: c45f7b6a693ef4c8d8a346ee9a599b9f6f253a8d1923ef32dc75de8f0302de35 diff --git a/scripts/notebook_tools/twin_pairs.d/socialchoice-4-computational-aggregation-sat-z3/0019-2026-10-03-claude-cloud-hors-flotte.yaml b/scripts/notebook_tools/twin_pairs.d/socialchoice-4-computational-aggregation-sat-z3/0019-2026-10-03-claude-cloud-hors-flotte.yaml new file mode 100644 index 0000000000..691e54c6dc --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/socialchoice-4-computational-aggregation-sat-z3/0019-2026-10-03-claude-cloud-hors-flotte.yaml @@ -0,0 +1,6 @@ +date: '2026-10-03' +by: claude-cloud:hors-flotte +python_sha: e27a85e121b89e1f4a4a49879599edf44138b480 +csharp_sha: fc26e9bd77e05d72dab5db316a3d37d3e9bbf072 +content_python_sha: 104a97247bc839a58bb603034891ee0cd1cb907562c38b9106b532ee6338db16 +content_csharp_sha: da4034f3983a6640ad5d81329980d161942ed61c0b3e7e043fc94a850f601275 diff --git a/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0014-2026-10-03-claude-cloud-hors-flotte.yaml b/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0014-2026-10-03-claude-cloud-hors-flotte.yaml new file mode 100644 index 0000000000..9bc36f0ea2 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/sudoku-12-z3/0014-2026-10-03-claude-cloud-hors-flotte.yaml @@ -0,0 +1,6 @@ +date: '2026-10-03' +by: claude-cloud:hors-flotte +python_sha: 48ede1c4544a6d38bdf77c4470b46fc3fc79339b +csharp_sha: de44d3131395164cb10105a9d64f25c214468bef +content_python_sha: 892ba015197e2d1de8906f50bcec12925d5c624835caa42aaedb6b94e31e0e73 +content_csharp_sha: 76d83ac233d41b1b20f2a5ac6d1f0adccef089d45eb4c6da9b17c76899422dad