diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb index 9db8516b1d..a53d12877f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb @@ -4,38 +4,30 @@ "cell_type": "markdown", "id": "c0", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003723, + "end_time": "2026-09-26T19:41:57.904939", + "exception": false, + "start_time": "2026-09-26T19:41:57.901216", + "status": "completed" + }, "tags": [] }, "source": [ "# Z3-Python-08 : Ordonnancement de tâches (Job-Shop Scheduling)\n", "\n", - "\n", - "\n", "[← Serie Z3-Python](README.md) | [Z3-Python-01b (style declaratif LINQ) →](Z3-01b-Style-Declaratif-Linq.ipynb)\n", "\n", - "\n", - "\n", "## Le problème\n", "\n", - "\n", - "\n", "Le **job-shop scheduling** est un problème canonique d'optimisation combinatoire : on dispose de $m$ machines et de $n$ jobs, chaque job etant une **sequence d'opérations** (une par machine) de durees données. On veut trouver un ordonnancement (date de debut de chaque opération) qui :\n", "\n", - "\n", - "\n", "1. **respecte l'ordre** des opérations de chaque job (precedence),\n", - "\n", "2. **n'utilise chaque machine qu'une fois a la fois** (exclusion disjonctive),\n", - "\n", "3. **minimise le makespan** $C_{\\max}$ (la date de fin de la dernière opération).\n", "\n", - "\n", - "\n", "Ce problème est **NP-difficile** : il n'existe pas d'algorithme polynomial connu, et une approche gloutonne (heuristique) rate souvent l'optimum. C'est typiquement la ou un solveur SMT comme Z3 **brille** : on decrit les contraintes (precedence + exclusion) et l'objectif (minimiser $C_{\\max}$), et `Optimize` trouve l'ordonnancement optimal.\n", "\n", - "\n", - "\n", "**Ce notebook montre** : (a) une heuristique gloutonne FIFO sous-optimale, (b) la modelisation Z3 avec la contrainte disjonctive `Or(... , ...)`, (c) l'optimum trouve par `Optimize.minimize`, et (d) un diagramme de Gantt comparant les deux. Il porte en Python l'exemple C# [11_Job_Shop_Scheduling](../Z3-Linq2Z3/11_Job_Shop_Scheduling.ipynb) de la serie sœur Z3.Linq." ] }, @@ -45,12 +37,18 @@ "id": "c1", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:22.944992Z", - "iopub.status.busy": "2026-07-17T20:08:22.944813Z", - "iopub.status.idle": "2026-07-17T20:08:23.991909Z", - "shell.execute_reply": "2026-07-17T20:08:23.990971Z" + "iopub.execute_input": "2026-09-26T19:41:57.913749Z", + "iopub.status.busy": "2026-09-26T19:41:57.913522Z", + "iopub.status.idle": "2026-09-26T19:41:58.997932Z", + "shell.execute_reply": "2026-09-26T19:41:58.996551Z" + }, + "papermill": { + "duration": 1.08961, + "end_time": "2026-09-26T19:41:58.999188", + "exception": false, + "start_time": "2026-09-26T19:41:57.909578", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -64,29 +62,17 @@ ], "source": [ "# Imports : z3 (solveur SMT) + matplotlib (diagramme de Gantt).\n", - "\n", "import os\n", - "\n", "import z3\n", - "\n", "import matplotlib\n", - "\n", "import matplotlib.pyplot as plt\n", "\n", - "\n", - "\n", "# En mode batch (Papermill/nbconvert headless), on desactive le mode interactif.\n", - "\n", "# On garde le backend inline par defaut (capture les figures au plt.show()).\n", - "\n", "BATCH_MODE = os.getenv(\"BATCH_MODE\", \"false\").lower() in (\"true\", \"1\", \"yes\")\n", - "\n", "if BATCH_MODE:\n", - "\n", " plt.ioff()\n", "\n", - "\n", - "\n", "print(\"z3 version :\", z3.get_version_string())" ] }, @@ -94,30 +80,26 @@ "cell_type": "markdown", "id": "c2", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003295, + "end_time": "2026-09-26T19:41:59.007472", + "exception": false, + "start_time": "2026-09-26T19:41:59.004177", + "status": "completed" + }, "tags": [] }, "source": [ "## Instance de reference : 3 jobs x 2 machines\n", "\n", - "\n", - "\n", "On encode l'instance comme un dictionnaire : chaque job est la liste ordonnee de ses opérations, chaque opération etant un couple `(machine, duree)`.\n", "\n", - "\n", - "\n", "| Job | Opération 1 | Opération 2 |\n", - "\n", "|-----|-------------|-------------|\n", - "\n", "| J0 | M0 (3h) | M1 (3h) |\n", - "\n", "| J1 | M1 (2h) | M0 (2h) |\n", - "\n", "| J2 | M0 (2h) | M1 (2h) |\n", "\n", - "\n", - "\n", "Notez que J0 et J2 commencent par M0, mais J1 commence par M1 : les jobs n'ont pas tous le même parcours." ] }, @@ -127,12 +109,18 @@ "id": "c3", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:23.994508Z", - "iopub.status.busy": "2026-07-17T20:08:23.994224Z", - "iopub.status.idle": "2026-07-17T20:08:23.998991Z", - "shell.execute_reply": "2026-07-17T20:08:23.998395Z" + "iopub.execute_input": "2026-09-26T19:41:59.015059Z", + "iopub.status.busy": "2026-09-26T19:41:59.014480Z", + "iopub.status.idle": "2026-09-26T19:41:59.022051Z", + "shell.execute_reply": "2026-09-26T19:41:59.020526Z" + }, + "papermill": { + "duration": 0.012878, + "end_time": "2026-09-26T19:41:59.023179", + "exception": false, + "start_time": "2026-09-26T19:41:59.010301", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -149,31 +137,18 @@ ], "source": [ "# Instance : 3 jobs x 2 machines (M0, M1).\n", - "\n", "# Format : jobs[j] = [(machine, duree), (machine, duree)] dans l'ordre des operations.\n", - "\n", "MACHINES = [\"M0\", \"M1\"]\n", - "\n", "jobs = {\n", - "\n", " \"J0\": [(\"M0\", 3), (\"M1\", 3)], # 3h sur M0 puis 3h sur M1\n", - "\n", " \"J1\": [(\"M1\", 2), (\"M0\", 2)], # 2h sur M1 puis 2h sur M0\n", - "\n", " \"J2\": [(\"M0\", 2), (\"M1\", 2)], # 2h sur M0 puis 2h sur M1\n", - "\n", "}\n", - "\n", "JOB_NAMES = list(jobs.keys())\n", "\n", - "\n", - "\n", "print(f\"Instance : {len(JOB_NAMES)} jobs x {len(MACHINES)} machines\")\n", - "\n", "for j in JOB_NAMES:\n", - "\n", " parcours = \" puis \".join(f\"{m}({d}h)\" for m, d in jobs[j])\n", - "\n", " print(f\" {j} : {parcours}\")" ] }, @@ -181,7 +156,13 @@ "cell_type": "markdown", "id": "af7a5d35", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003324, + "end_time": "2026-09-26T19:41:59.031538", + "exception": false, + "start_time": "2026-09-26T19:41:59.028214", + "status": "completed" + }, "tags": [] }, "source": [ @@ -201,18 +182,20 @@ "cell_type": "markdown", "id": "c4", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.005989, + "end_time": "2026-09-26T19:41:59.041905", + "exception": false, + "start_time": "2026-09-26T19:41:59.035916", + "status": "completed" + }, "tags": [] }, "source": [ "## Approche gloutonne : ordonnancement FIFO\n", "\n", - "\n", - "\n", "Avant Z3, essayons une **heuristique simple** : on schedule les jobs dans l'ordre (J0, puis J1, puis J2), et pour chaque job on place chaque opération **le plus tot possible** (des que la machine est libre et que l'opération précédente du job est terminee).\n", "\n", - "\n", - "\n", "Cette stratégie FIFO est rapide mais **myope** : elle ne regarde pas plus loin que le job courant, et peut laisser une machine inutilisee la ou un autre ordre aurait mieux equilibre la charge." ] }, @@ -222,12 +205,18 @@ "id": "c5", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.000938Z", - "iopub.status.busy": "2026-07-17T20:08:24.000705Z", - "iopub.status.idle": "2026-07-17T20:08:24.005994Z", - "shell.execute_reply": "2026-07-17T20:08:24.005321Z" + "iopub.execute_input": "2026-09-26T19:41:59.054990Z", + "iopub.status.busy": "2026-09-26T19:41:59.054346Z", + "iopub.status.idle": "2026-09-26T19:41:59.065515Z", + "shell.execute_reply": "2026-09-26T19:41:59.063778Z" + }, + "papermill": { + "duration": 0.019932, + "end_time": "2026-09-26T19:41:59.067173", + "exception": false, + "start_time": "2026-09-26T19:41:59.047241", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -244,41 +233,23 @@ ], "source": [ "def greedy_fifo(jobs, machine_names):\n", - "\n", " \"\"\"Ordonnancement glouton : schedule chaque job dans l'ordre, chaque operation ASAP.\"\"\"\n", - "\n", " machine_free = {m: 0 for m in machine_names} # disponibilite de chaque machine\n", - "\n", " schedule = {}\n", - "\n", " for j in jobs:\n", - "\n", " schedule[j] = []\n", - "\n", " for (m, d) in jobs[j]:\n", - "\n", " job_ready = schedule[j][-1][1] + schedule[j][-1][2] if schedule[j] else 0\n", - "\n", " start = max(machine_free[m], job_ready)\n", - "\n", " schedule[j].append((m, start, d))\n", - "\n", " machine_free[m] = start + d\n", - "\n", " cmax = max(s[1] + s[2] for j in schedule for s in schedule[j])\n", - "\n", " return schedule, cmax\n", "\n", - "\n", - "\n", "greedy_schedule, greedy_cmax = greedy_fifo(jobs, MACHINES)\n", - "\n", "print(f\"Glouton FIFO : Cmax = {greedy_cmax}h\")\n", - "\n", "for j in JOB_NAMES:\n", - "\n", " ops = \", \".join(f\"{m}[{s},{s+d}]\" for m, s, d in greedy_schedule[j])\n", - "\n", " print(f\" {j} : {ops}\")" ] }, @@ -286,26 +257,24 @@ "cell_type": "markdown", "id": "c6", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.005395, + "end_time": "2026-09-26T19:41:59.078694", + "exception": false, + "start_time": "2026-09-26T19:41:59.073299", + "status": "completed" + }, "tags": [] }, "source": [ "## Modelisation Z3 : variables et contraintes\n", "\n", - "\n", - "\n", "Le passage au declaratif. On introduit une variable entiere $s_{j,k}$ = date de debut de l'opération $k$ du job $j$, plus une variable $C_{\\max}$ pour le makespan. Les contraintes se traduisent directement :\n", "\n", - "\n", - "\n", "1. **Precedence intra-job** : l'opération $k$ commence après la fin de l'opération $k{-}1$ : $s_{j,k} \\ge s_{j,k-1} + d_{j,k-1}$.\n", - "\n", "2. **Exclusion disjonctive** (le coeur du modèle) : pour deux opérations $a$ et $b$ sur la **même** machine, l'une doit finir avant que l'autre commence : $s_a + d_a \\le s_b$ **OU** $s_b + d_b \\le s_a$. C'est cette disjonction `Or(...)` (non-lineaire, difficile pour un simple parcours) qui fait toute la valeur du solveur.\n", - "\n", "3. **Objectif** : minimiser $C_{\\max} = \\max_{j,k}(s_{j,k} + d_{j,k})$, via `Optimize.minimize`.\n", "\n", - "\n", - "\n", "La borne superieure sure $C_{\\max} \\le$ somme de toutes les durees (cas ou tout serait sequentialise) garantit un domaine fini au solveur." ] }, @@ -315,12 +284,18 @@ "id": "c7", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.008187Z", - "iopub.status.busy": "2026-07-17T20:08:24.008000Z", - "iopub.status.idle": "2026-07-17T20:08:24.072245Z", - "shell.execute_reply": "2026-07-17T20:08:24.071654Z" + "iopub.execute_input": "2026-09-26T19:41:59.092876Z", + "iopub.status.busy": "2026-09-26T19:41:59.092268Z", + "iopub.status.idle": "2026-09-26T19:41:59.165931Z", + "shell.execute_reply": "2026-09-26T19:41:59.164258Z" + }, + "papermill": { + "duration": 0.083555, + "end_time": "2026-09-26T19:41:59.167610", + "exception": false, + "start_time": "2026-09-26T19:41:59.084055", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -334,87 +309,46 @@ ], "source": [ "def solve_jobshop(jobs, machine_names):\n", - "\n", " \"\"\"Modelise le job-shop en Z3 et minimise le makespan (Cmax).\"\"\"\n", - "\n", " opt = z3.Optimize()\n", - "\n", " job_names = list(jobs.keys())\n", - "\n", " horizon = sum(d for j in jobs for (_, d) in jobs[j]) # borne sup sure\n", "\n", - "\n", - "\n", " # Variables de debut : start[j][k]\n", - "\n", " start = {j: [z3.Int(f\"s_{j}_{k}\") for k in range(len(jobs[j]))] for j in job_names}\n", - "\n", " cmax = z3.Int(\"cmax\")\n", "\n", - "\n", - "\n", " # (1) Domaine + precedence intra-job + borne makespan\n", - "\n", " for j in job_names:\n", - "\n", " for k, (m, d) in enumerate(jobs[j]):\n", - "\n", " opt.add(start[j][k] >= 0)\n", - "\n", " opt.add(start[j][k] + d <= cmax)\n", - "\n", " if k > 0:\n", - "\n", " _, pd = jobs[j][k - 1]\n", - "\n", " opt.add(start[j][k] >= start[j][k - 1] + pd)\n", "\n", - "\n", - "\n", " # (2) Exclusion disjonctive : deux operations sur la MEME machine ne se chevauchent pas\n", - "\n", " for m in machine_names:\n", - "\n", " ops_on_m = [(j, k, jobs[j][k][1])\n", - "\n", " for j in job_names for k in range(len(jobs[j]))\n", - "\n", " if jobs[j][k][0] == m]\n", - "\n", " for a in range(len(ops_on_m)):\n", - "\n", " for b in range(a + 1, len(ops_on_m)):\n", - "\n", " ja, ka, da = ops_on_m[a]\n", - "\n", " jb, kb, db = ops_on_m[b]\n", - "\n", " opt.add(z3.Or(start[ja][ka] + da <= start[jb][kb],\n", - "\n", " start[jb][kb] + db <= start[ja][ka]))\n", "\n", - "\n", - "\n", " # (3) Objectif : minimiser le makespan\n", - "\n", " opt.add(cmax <= horizon)\n", - "\n", " opt.minimize(cmax)\n", - "\n", " assert opt.check() == z3.sat, \"Instance insatisfiable\"\n", - "\n", " model = opt.model()\n", - "\n", " schedule = {j: [(jobs[j][k][0], model[start[j][k]].as_long(), jobs[j][k][1])\n", - "\n", " for k in range(len(jobs[j]))] for j in job_names}\n", - "\n", " return schedule, model[cmax].as_long()\n", "\n", - "\n", - "\n", "opt_schedule, opt_cmax = solve_jobshop(jobs, MACHINES)\n", - "\n", "print(f\"Z3 optimal : Cmax = {opt_cmax}h (glouton = {greedy_cmax}h, gain = {greedy_cmax - opt_cmax}h)\")" ] }, @@ -422,7 +356,13 @@ "cell_type": "markdown", "id": "5f602514", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.00522, + "end_time": "2026-09-26T19:41:59.178214", + "exception": false, + "start_time": "2026-09-26T19:41:59.172994", + "status": "completed" + }, "tags": [] }, "source": [ @@ -446,7 +386,13 @@ "cell_type": "markdown", "id": "c8", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.006387, + "end_time": "2026-09-26T19:41:59.190189", + "exception": false, + "start_time": "2026-09-26T19:41:59.183802", + "status": "completed" + }, "tags": [] }, "source": [ @@ -463,12 +409,18 @@ "id": "c9", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.073890Z", - "iopub.status.busy": "2026-07-17T20:08:24.073749Z", - "iopub.status.idle": "2026-07-17T20:08:24.077363Z", - "shell.execute_reply": "2026-07-17T20:08:24.076976Z" + "iopub.execute_input": "2026-09-26T19:41:59.203021Z", + "iopub.status.busy": "2026-09-26T19:41:59.202555Z", + "iopub.status.idle": "2026-09-26T19:41:59.211778Z", + "shell.execute_reply": "2026-09-26T19:41:59.210061Z" + }, + "papermill": { + "duration": 0.018002, + "end_time": "2026-09-26T19:41:59.213479", + "exception": false, + "start_time": "2026-09-26T19:41:59.195477", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -514,7 +466,13 @@ "cell_type": "markdown", "id": "41adc3b0", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.004753, + "end_time": "2026-09-26T19:41:59.223660", + "exception": false, + "start_time": "2026-09-26T19:41:59.218907", + "status": "completed" + }, "tags": [] }, "source": [ @@ -532,7 +490,13 @@ "cell_type": "markdown", "id": "c10", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.005419, + "end_time": "2026-09-26T19:41:59.234533", + "exception": false, + "start_time": "2026-09-26T19:41:59.229114", + "status": "completed" + }, "tags": [] }, "source": [ @@ -549,18 +513,24 @@ "id": "c11", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.079233Z", - "iopub.status.busy": "2026-07-17T20:08:24.079099Z", - "iopub.status.idle": "2026-07-17T20:08:24.311966Z", - "shell.execute_reply": "2026-07-17T20:08:24.311083Z" + "iopub.execute_input": "2026-09-26T19:41:59.248273Z", + "iopub.status.busy": "2026-09-26T19:41:59.247781Z", + "iopub.status.idle": "2026-09-26T19:41:59.581315Z", + "shell.execute_reply": "2026-09-26T19:41:59.580143Z" + }, + "papermill": { + "duration": 0.342087, + "end_time": "2026-09-26T19:41:59.582267", + "exception": false, + "start_time": "2026-09-26T19:41:59.240180", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ { "data": { - "image/png": "iVBORw0KGgoAAAANSUhEUgAAA90AAAJOCAYAAACqS2TfAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjgsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvwVt1zgAAAAlwSFlzAAAPYQAAD2EBqD+naQAAYWdJREFUeJzt3Qd4VGX69/E7jZBCQgspErp0KQFEAQVFRUQUUbGLYPnjgqu4uqyr4uKqqGtDRUFdwIYCK6AgtkUQQQRpQgKKQAy9GtJIgWTe637YmTcJCQmQJyeZ+X6ua66ZOXMyuc+cQPI7T/NzuVwuAQAAAAAAFc6/4t8SAAAAAAAoQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AMCqf/zjH+Ln5+d0GSikoKBA2rdvL08//bTTpfi0xYsXm38b//nPf8rc98Ybb5QhQ4ZUSl0AgIpF6AYAnLLk5GQZNWqUtGzZUkJDQ82tbdu2MnLkSFm/fn2l17Nx40YT7n///XdxSpMmTUyAKumWk5Nj9pk2bZp5vmrVqhMuSpR0mzRpUpHvkZWVJf/85z+lQ4cO5jOPjIyUCy64QN577z1xuVzlrvWjjz6SHTt2mHNY3NatW+X//u//pFmzZlKzZk2JiIiQnj17yoQJEyQ7O1t8mV6kuOqqqyQ6OtqcHz135XHppZea/Uv6vMtrzJgx8sknn8jPP/982u8BAHBGoEPfFwBQTc2fP19uuOEGCQwMlFtuuUU6duwo/v7+8ssvv8js2bPlzTffNKG8cePGlRq6x40bJ3369DHh1ymdOnWSv/zlLydsr1GjRplfq59beHh4kW3du3f3PN63b5/07dtXNm3aZFo9NcBpmNcgNnToUFmwYIF8+OGHEhAQUOb3+te//mXeQ0N7YZ9//rlcf/31EhwcLLfffrtpDc/Ly5OlS5fKww8/LElJSfLWW2+Jr3rsscckJiZGOnfuLF999VW5vkb/TSxfvvyMv7d+z65du8qLL75oLrIAAKoPQjcAoNy0FVTDmgbqhQsXSmxsbJHXn3vuOXnjjTdMCPdFZ511ltx6662n9bXXXXed1K9fv9TXNVhr4J4zZ45pbXX785//bALxCy+8YIKZtoiezNq1a01rqYa3wvRCifvcfvvtt0XOrfZg2LJliwnlvkw/I72oc/DgQYmKiipzf70oohdh9JyMHTv2jL+/di9/4oknzL+x4hdoAABVl2/+VQQAOC3PP/+86eI8derUEwK30tZvDYHx8fEnfZ9jx46ZbtLNmzc3raoaZP7+979Lbm5ukf1K68Kr+99xxx2eLtvaOqsuuugiT9dsHS/rpiGlXbt25nvFxcWZEHn48OEi76mt5Nqyq63m+j7afVtDtB6z03788UfTsqrHXDhwu40fP17OPvtsc9GjrC7gc+fONS3vF154YZHtepyZmZny73//u8Rz26JFC7n//vs9z93dpWfNmmWGFoSEhMj5558vGzZsMK9PnjzZfI12UdfPtnjX/++//96ct0aNGpnzoj8zo0ePLlL//v37TbjVry/cfV4vAISFhZkeF5XpVHtR6Geq4+cfeuihk+6n+2jX9YYNG5rPS3s06DGW1E1d//198803p1w7AMA5hG4AwCl1LdcgVbjb8+m46667TMtfQkKCvPzyy9K7d28THLWl9VRpeNSgrzS4v//+++bWpk0bs01Du4ZsDdvaunvttdeaQHjZZZfJ0aNHi7xXamqqXH755abLvO7bunVr00r5xRdflKsWfT9tBS18O3LkSLm+9o8//ijydVqL27x588y9dvkuiV7suPnmm83XLFu27KTf54cffjAXF4KCgops1++h47h79Ogh5aXBWVtytRVeP2dtib/yyitl4sSJ8uqrr8qf/vQn0wqv3auHDx9e5Gs1rOtnc++998prr70m/fr1M/eFj7FBgwam2/13331nXnMHVL34UKtWLXMx5VTPR2k3fd+KtH37dnn22WfNhRC9IHEyup/2YNBw/sgjj5iLLDp0ozj3xY2yzjEAoIpxAQBQDmlpadrU6Bo0aNAJr6WmproOHDjguR05csTz2hNPPGG+zm3dunXm+V133VXkPR566CGz/dtvv/Vs0+f69cU1btzYNXToUM/zWbNmmX0XLVpUZL/9+/e7atSo4brssstc+fn5nu2vv/662X/KlCmebb179zbb3nvvPc+23NxcV0xMjOvaa68t8/PRmvTri98K1z916lSz7aeffjrh8yl+0/dz089ct+nnXJrZs2ebfV599dWT1tmwYcMTjsd9bq+++mpXeen+wcHBruTkZM+2yZMnm+36maWnp3u2P/LII2Z74X0L/4y4jR8/3uXn5+dKSUkpsv2mm25yhYaGujZv3uz617/+Zd5r7ty5ZdaoPw8lfbYl3QrXVhb9GS/tZ9Ptuuuuc/Xo0cPzXPcfOXJkifW1adPG/Ky5TZgwwWzfsGHDCe/bsmVLV//+/ctdKwDAeYzpBgCUS3p6urkvaSypdv8tPKuyTtRVWpdanfBLPfjgg0W2a4upjkvWccPavbsi/Pe//zUTgT3wwANFxpnffffdplVcv9ewYcM82/XYCo/J1m7Y5557rmzbtq1c3097ADz11FNFtmnrcXnohGg6U7hb4dbRjIwMc6+tu6Vxv+Y+T6U5dOiQ1KlTp8g299ec7P1Lot2gC3e5dveA0N4Ehd/LvV0/R/f+hY9Pu0xrt3JtZdd8quPOtdu52+uvv26GC+i4982bN8ttt90mV199dZn1aY+F8nbF1gnSKsqiRYvM+VyxYkW59tefwcKT7emM9O7PS3slFKbnTlvmAQDVB6EbAFAu7hCl436L0+7aGgx1hu2yJhJLSUkxAVi7qRcPPbVr1zavVxT3e7Vq1arIdg04GoaLfy8dU1t8TXENOeVdBk0nQrvkkktOq1btJl/aRGruz14/Y/2MSlKeYO5WfHkxd9h3v0d5FQ7Gyj0bevEx/e7thbvMa/drHWLw2WefFdmu0tLSijyvW7eu6a6uY8B1uS59XB567k73fJwuna9AhzvohYFu3bqd1ufovihS/HNxnzvWvQeA6oXQDQAoFw1OOsFWYmLiCa+5WzJPZZ3sMwkO+fn5YkNpy22dyhrYNuj4dJ0ATcN/8QnQ3NwXBnTc78nUq1fvhDCnoVvHvJd0bk/n8yrrc9Tzp5OC6Th2HTOvY+d1YrRdu3aZ8dolja92L9Glte/cubPUiw+FaS8H/R7loRO2lWe5tbLocl6//vqruRBV/N+DXtTQbTpWXSfqO52fOz1+nTQPAFB9MJEaAKDcBgwYYGZVXrly5Wm/hy5JpaHqt99+K7JdW8l1RvHC63tri1/xWcY1SO3Zs6dcAd79XhqCir9HZa8lfiZ0cjJV2vrMGmKnT59uPq+ePXue9L004Oqxl/Q9dEm4ilhTuiw6w7l2E9fJ6jR0a1dxbZHW4F+SL7/8Ut555x3561//asKxTtymLcpl0Unj9EJReW47duyokGPTFnydwE3PQ9OmTT039/nTx19//fVpvbces9bpniQQAFA9ELoBAOWmoUdb6HQmag3Jp9MifMUVV5j7V155pcj2l156yRPs3XRJsSVLlhTZ76233jqhpVtbSVXxgK5BTruSa3fkwrXpsljahbnw96rKdKyzHosu1aYzyBf36KOPmhCr56esmbJ1WS9t0S6+PJt+rX6OOrN8SedWA/mECRMq4Gj+f8tu4XOij0t6fz2nWpOOrX/mmWdM+F6zZo15XN4x3eW5VdSYbp2BX2ciL35z/+zr49Od/V+Xs9O1v09lhnkAgPPoXg4AKDft1qotqjfddJMZJ63LGmmw0cCkraf6mo7X1rHRpdH9taVSw7MGKl0uTFvO3333XRk0aFCRSdQ0bI0YMcJMzKXdkXWyNu1mXHzsc6dOnUyQ0+WZNEzrus8XX3yx6carSzCNGzfOLAWma1xrq7cuNaXjbcsaf16VaCupTlymrcK6PJhOtqXBefbs2WaSMV2zWpfnKot+va6Rrstw6bJphS9w6PnT99GWVF26Syfx0l4B2mKsS3y510Y/U9rart9PJ9vTLuXavV0nHitpDLOuDa6Tv+mkeHqO9Tzqz4VOWKfHoj9PlTWmW5ei03kA3MvA6QUh98R5OoZbe07osemtJNrKrT/jp0svDuhFL/23AACoPgjdAIBTokFHuwdr12DtJjtlyhTTvVsDh7Yca0g+WRBS2lqpE5lNmzbNtPxpK6OG4yeeeKLIfjrLuIZ5bZnWLsYaNDV4aPgsTL9+0qRJZq3vO++807SE6wzSGrp1/WjtkqwzYI8ePdpMynXPPfeYltLia1VXZdoFWi9O6OeuAVhDqq7P3aFDB/M5akguzzj5Ll26mK+ZOXNmkdCt9KKEjg3X2ec//fRTs0a2XsDQ/fX76vmoCPq567rgOuGYnrOaNWvKNddcI6NGjSrys6OTrOnFBvea6YV7RejPgV68+emnnyrtPOrPoV6scNOfMb2pXr16WR+uoOd98ODBpzzLPADAWX66bpjDNQAAgEqkLbYjR44044/LMyEZnLdu3TpJSEgwXeu1ZwcAoPogdAMA4GN0IjttvdZhAjoeHFWfjhXX86Y9FAAA1QuhGwAAAAAAS5i9HAAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAL66TrfO1Ll7926zJmV51h8FAAAAAMA2nZM8IyND4uLixN/fv/qGbg3c8fHxTpcBAAAAAMAJduzYIQ0bNpRqG7q1hdt9IBEREU6XAwAAAACApKenmwZid2attqHb3aVcAzehGwAAAABQlZQ1DJqJ1AAAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAkiq/TrfbhRdfKQGB1aZc4LTExdSXeXNnOl0GAFhz8+CBkrpvj9NloBJt2n9A6jeMcboMVKLY+jEyb9anTpcBVBnVJsXGnHevBAWHOl0GYNXuZROcLgEArNLAPfGKxk6XgUrUY8pOaTYiwekyUIm2TVrjdAlAlUL3cgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALAm09caoXua9eLW5HzxmnkTXDZURgztI6yZ1JTfvmHy3ZpdMmZcox/JdTpcJAEC10OzRT8x98rM3SsS5A6RWx74SVDdG/Pz8Zff7YyVne5LTJaKCzbzhTXN/z6dj5O6uN0vTOvESEVxL0nMyZEnKCpmxYZ64hL+lAF9ESzeKCPD3k8eHd5c2TerKh19ukjW/7peBFzSTGy9t5XRpAABUS36BQXJky2o5lnbQ6VJQCUKDQuSsiBhZuHWpvLt2lgnag9v2l35n93a6NAAOoaUbRbRvXl/iosLlh/W7Zc7irRJcI0B6dTxLruzVTD748henywMAoNo5/P0sc1+zYSsJqt3A6XJg2aHswzL6i3Hich1v1Q70D5RhCUOkSe2GTpcGwCG0dKOIJrER5v5Aara5z83Ll/SsPAkLCZLa4cEOVwcAAFC1FRTkewK3n/hJQlx783jDPhovAF9FSzfK5Od0AQAAANWMtnCP7D5UOsa0lQWbv5Vl21c5XRIAhxC6UcTve9LNfVSdEHOv3ctrhdWQrOyjcjgz1+HqAAAAqse47od7jZB2DVrKrMT5Mivpc6dLAuAgQjeKSNx6UHYfzJSubaLlmj7NpWlcpAQG+MvsZVucLg0AgGqpZnxbCaoXKwGhx4dwhbboYmYyz1i30OnSYIG/f4A82fchaRQZJ2v3JMmu9H3SI76rpOVmSNL+X50uD0B1GNN9xx13iJ+fn4wYMeKE10aOHGle033cJk6cKE2aNJGaNWtK9+7dZeXKlWdeNSpUrdAgc5+Te0xy8vLl6SkrZdPvf8itl7eRLq2jZf7SbfLR1/ySAACgPPxDws19QV6OuPKPSq2OF0vUgD9JUJ0Ys732+Veb5/Ae4TXCzH3OsVyJCA43gVt1jm0nD/S409yua3eFw1UCqFYt3fHx8fLxxx/Lyy+/LCEhx7sh5+TkyPTp06VRo0ae/WbMmCEPPvigTJo0yQTuV155Rfr16ye//vqrNGjA7J1VQY8OsTKodwvzeMPW40uZbN+XIY9N+sHhygAAqH7CWp8nkd0HmsfZKYnm/sD8180N3ql7w85yZau+5nHS/s1yIOuQDJlxr9NlAajus5cnJCSY4D179mzPNn2sgbtz586ebS+99JLcfffdMmzYMGnbtq0J36GhoTJlypSKqR5nrFubGImpFypL1u6U12auc7ocAACqNe06Hlg7RjKTlsrBBW86XQ4qgc5OHh0eZSZKm/zTB06XA8CbxnQPHz5cpk6dKrfccot5rkFaw/XixYvN87y8PFm9erU88sgjnq/x9/eXSy65RJYvX17q++bm5pqbW3r68Ym9YMeEGWudLgEAAK9xYP5Ep0tAJXtz5ftOlwDAW9fpvvXWW2Xp0qWSkpJibsuWLTPb3A4ePCj5+fkSHR1d5Ov0+d69e0t93/Hjx0tkZKTnpi3qAAAAAAD4VEt3VFSUDBgwQKZNmyYul8s8rl+//hkXpC3jOg68cEs3wduep+/tIc3iIiW4RqCkZebK8sQ9MuWzJLm+79lyc7/WMv2rX5hEDQCAcvCvGSZRA0dJcEwz8Q+NkIKsNMlIXCKpiz+S8A59pMHAUZLx8yLGd3uZsKBQ+VP326VpnXiJCK4l6TkZsiRlhczYME8ubNLdrNW9OHm5vLHyPadLBVAdlwzTLuajRo3yzFJemAbwgIAA2bdvX5Ht+jwm5vjsnSUJDg42N1SO5F3p8t2aXSLiMhOqDezVTHbuz3S6LAAAqh3/4FAJqtdQ0td+I/lH0qV2j8FSp+e1kp+ZamYyh3cKDaopZ0XEyMKtSyU9N1MGtekng9v2l8M56ZJ9lPMO4AxD9+WXX27GbusyYToreWE1atSQLl26yMKFC2XQoEFmW0FBgXnuDupw3jufJUp4SJCEhQRJjw5xEh9dS8Tl8rweWy9MnhrRQ86OryNbdqbKc++tkvSsPEdrBgCgKjqWfkh2Tr5fxFVgnvsFBEn9y4ZLjeimkrNjk9kWEBYh0dePkZBG7eRo6l7ZN+clOZZa+rA7VH2Hsg/L6C/GmZ6fKtA/UIYlDJEmtRvKpgNbzDZdRuzhXiOkXVRL2Zt5QF5e/o7syzzgcOUAqvyYbqUt2Zs2bZKNGzeax8VpN/G3335b3n33XbPfvffeK1lZWWbCNVQdkx/pK+88eqlZk3vR6h3y9YoUz2vd28fIisS98vueNOnQIkoG9GzqaK0AAFRZGrb/F7hF/CS0RYJ5lJ283rNLSNOOkrtrs2Rv3yjBsc2lTs/rHCoWFaXAVeAJ3H7iZ2YzVxv2/eLZp0NMW/ntULJsPPCbNKvbSK5t29+xegFUs5ZuFRERUeprN9xwgxw4cEDGjh1rJk/r1KmTfPnllydMrgZnPTPtJ6lTK1iu6dNCLux0lvy4YY/ntUWrd8q8pdsk92i+tG1aT2LrhzlaKwAAVV5AoDQYeJ+ENuskaSs/l6yNSyW8w0Xmpezkn+XwD3MkpGkHCWvZTYLqlj7kDtWLtnDr+O2OMW1lweZvzRJivZucZ15bv3ejzN30lZwT3Vq6ntVBYsKjnC4XQFUO3Tpx2snMnTu3yHPtSk538qotadshz+Mxt3eTvt0ayZadh81znVxN5Rccv3If4O/nUJUAAFSPcd2m+3jj9pK6ZIakfj+zyOv5WceXQnXl5//vC07sKYjqJzQo5Hj38QYtZVbifJmV9HmR13Wst8ovOH7e/TnvgE8545ZuVF8JrRpI74SGsin5kIifnwzsdbzrePLuNKdLAwCg2vELqilxtz8tNRo0kiNb10jeoV0S1ran5Gfxe9WbBQcGy5N9H5JGkXGydk+S7ErfJz3iu0pabobTpQGoIgjdPkwnRGscW0vOax8rAQF+cigtW2Yt3GyWCBtySUunywMAoFoJCK1lArcKbZ5gbio7JVEy1i92uDrYElEjzARu1Tm2nbmppP2bzVJhAODncs/8UEXpOt2RkZHSb+R0CQoOdbocwKrdyybI6h+/dboMALCmf8+uMvGKxk6XgUrUY8oyufCZa5wuA5Vo26Q1smrRCqfLACotq6alpZ10rrMzmr0cAAAAAACUjtANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYEmgVBN7f3xTAgKrTbnAaYmLqe90CQBgVZ3oWBm5IMXpMlCJavoHy7ZJa5wuA5Uotn6M0yUAVYqfy+VySRWWnp4ukZGRkpaWJhEREU6XAwAAAACAlDer0r0cAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgSaCtNwZw6gYOGiK79x50ugygUhzZv1WaxEY5XQYqWZ3oWJk+e57TZQCwaOD1V8ueg3udLgOVKLZ+jMyb9anTZVRZhG6gCtHAHdfzfqfLACrF1pn3yMQrGjtdBirZyAUpTpcAwDIN3M1GJDhdBirRtklrnC6hSqN7OQAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlgTaemMAqKrmvXi1uR88Zp5E1w2VEYM7SOsmdSU375h8t2aXTJmXKMfyXU6XCS/R7NFPzH3yszdKxLkDpFbHvhJUN0b8/Pxl9/tjJWd7ktMlAgBOw8wb3jT393w6Ru7uerM0rRMvEcG1JD0nQ5akrJAZG+aJS/h7ArR0A/BhAf5+8vjw7tKmSV358MtNsubX/TLwgmZy46WtnC4NXsovMEiObFktx9IOOl0KAKCChAaFyFkRMbJw61J5d+0sE7QHt+0v/c7u7XRpqCJo6Qbgs9o3ry9xUeHyw/rdMmfxVgmuESC9Op4lV/ZqJh98+YvT5cELHf5+lrmv2bCVBNVu4HQ5AIAKcCj7sIz+Ypy4XMdbtQP9A2VYwhBpUruh06WhiqClG4DPahIbYe4PpGab+9y8fEnPypOwkCCpHR7scHUAAKA6KCjI9wRuP/GThLj25vGGfVzAx3G0dANAIX5OFwAAAKolbeEe2X2odIxpKws2fyvLtq9yuiRUEYRuAD7r9z3p5j6qToi51+7ltcJqSFb2UTmcmetwdQAAoDqN63641whp16ClzEqcL7OSPne6JFTX7uV33HGH+Pn5yYgRI054beTIkeY13UctWbJEBg4cKHFxcWb73LlzK65qAKgAiVsPyu6DmdK1TbRc06e5jLyuowQG+Mvny5KdLg1eqmZ8W6nVqa8EhB4f2hDaoot5DgCovvz9A+TJvg+ZwL12T5LsSt8nPeK7SrsGTMyK02zpjo+Pl48//lhefvllCQk53jqUk5Mj06dPl0aNGnn2y8rKko4dO8rw4cNl8ODBp/ptAMCKWqFB5j4n95jk5OXL01NWyj3XnCO3Xt7GPJ+/dJt89PWvTpcJL+EfEm7uC/JyxJV/VGp1vFhqdbzI83rt848vX5exbqFjNQIATl14jTBzn3MsVyKCw6VRZJx53jm2nbmppP2bJWk/f1PgNEJ3QkKCbN26VWbPni233HKL2aaPNXA3bdrUs1///v3NDQCqih4dYmVQ7xbm8Yatx5ds2r4vQx6b9IPDlcEbhbU+TyK7DzSPs1MSzf2B+a+bGwCg+uresLNc2aqvJ1gfyDokQ2bc63RZ8LbZy7X1eurUqZ7nU6ZMkWHDhlVkXQBQ4bq1iZGYeqGyZO1OeW3mOqfLgZfTruOBtWMkM2mpHFzwptPlAAAqiM5OHh0eZSZKm/zTB06XA2+dSO3WW2+VRx55RFJSUszzZcuWmS7nixcvPuOCcnNzzc0tPf34REcAcKYmzFjrdAnwIQfmT3S6BACABW+ufN/pEuALoTsqKkoGDBgg06ZNM2vS6eP69etXSEHjx4+XcePGVch7AQAAAABQLZcM0y7mo0aNMo8nTqy4q/nagv7ggw8WaenWydsA4Ew9fW8PaRYXKcE1AiUtM1eWJ+6RKZ8lyfV9z5ab+7WW6V/9wiRqqDD+NcMkauAoCY5pJv6hEVKQlSYZiUskdfFHEt6hjzQYOEoyfl7EGG8AqGbCgkLlT91vl6Z14iUiuJak52TIkpQVMmPDPLmwSXezVvfi5OXyxsr3nC4V1T10X3755ZKXl2eWA+vXr1+FFRQcHGxuAFDRknely3drdomIy0yoNrBXM9m5P9PpsuCl/INDJaheQ0lf+43kH0mX2j0GS52e10p+ZqqZzRwAUD2FBtWUsyJiZOHWpZKemymD2vSTwW37y+GcdMk+yv/vqMDQHRAQIJs2bfI8Li4zM1O2bNnieZ6cnCzr1q2TunXrFllaDAAqyzufJUp4SJCEhQRJjw5xEh9dS8Tl8rweWy9MnhrRQ86OryNbdqbKc++tkvSsPEdrRvV1LP2Q7Jx8v4irwDz3CwiS+pcNlxrRTSVnx/9+f4ZFSPT1YySkUTs5mrpX9s15SY6l7nW4cgDAyRzKPiyjvxhnhtmqQP9AGZYwRJrUbiibDhzPP7qM2MO9Rki7qJayN/OAvLz8HdmXecDhylGtZi93i4iIMLeSrFq1Sjp37mxuSruM6+OxY8eeybcEgDMy+ZG+8s6jl0qX1tGyaPUO+XrF8QkhVff2MbIica/8vidNOrSIkgE9//8yiMAp07D9v8At4iehLRLMo+zk9Z5dQpp2lNxdmyV7+0YJjm0udXpe51CxAIDyKnAVeAK3n/iZ2czVhn2/ePbpENNWfjuULBsP/CbN6jaSa9uylLIvO6WWbp047WTmzp3redynTx/PDyMAVBXPTPtJ6tQKlmv6tJALO50lP27Y43lt0eqdMm/pNsk9mi9tm9aT2PphjtYKLxEQKA0G3iehzTpJ2srPJWvjUgnvcJF5KTv5Zzn8wxwJadpBwlp2k6C6MU5XCwAoJ23h1vHbHWPayoLN35olxHo3Oc+8tn7vRpm76Ss5J7q1dD2rg8SERzldLqpj93IAqI6Sth3yPB5zezfp262RbNl52DzXydVUfsHx1skAfz+HqoQ3jes23ccbt5fUJTMk9fuZRV7Pzzq+LKYrP/9/X3DicC0AQNUTGhRyvPt4g5YyK3G+zEr6vMjrOtZb5Rcc///dn//ffRqhG4BPSGjVQHonNJRNyYdE/PxkYK/jXceTd6c5XRq8lF9QTYm7/Wmp0aCRHNm6RvIO7ZKwtj0lP4ufOQCozoIDg+XJvg9Jo8g4WbsnSXal75Me8V0lLTfD6dJQRRG6AfgEnRCtcWwtOa99rAQE+MmhtGyZtXCzWSJsyCUtnS4PXiggtJYJ3Cq0eYK5qeyURMlYv9jh6gAApyuiRpgJ3KpzbDtzU0n7N5ulwoDi/FxVfOC1rtMdGRkpaWlppU7aBniLLuddLHE973e6DKBSbJ15j8wf0cvpMlDJRi5IkS+WrXK6DAAWdb2ouzQbcfxCI3zDtklrZNWiFeJr0suZVc9o9nIAAAAAAFA6QjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYG23hjAqYuLqS+7l01wugygUriCasrIBSlOl4FKVic61ukSAFgWWz9Gtk1a43QZqORzjtL5uVwul1Rh6enpEhkZKWlpaRIREeF0OQAAAAAASHmzKt3LAQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMCSQKni3MuI6xpoAAAAAABUBe6M6s6s1TZ0Hzp0yNzHx8c7XQoAAAAAAEVkZGRIZGSkVNvQXbduXXO/ffv2kx4IvOuKkV5k2bFjh0RERDhdDioB59z3cM59E+fd93DOfQ/n3Pf48jl3uVwmcMfFxZ10vyofuv39jw8718DtayfR1+n55pz7Fs657+Gc+ybOu+/hnPsezrnv8dVzHlmOhmEmUgMAAAAAwBJCNwAAAAAAvhq6g4OD5YknnjD38A2cc9/DOfc9nHPfxHn3PZxz38M59z2c87L5ucqa3xwAAAAAAHhnSzcAAAAAANUVoRsAAAAAAEsI3QAAAAAAWELoBgDABzz++ONyzz33eJ736dNHHnjgAamO/va3v8l9993ndBkAAJQLoRsAgFL4+fmd9PaPf/xDqoO9e/fKhAkT5NFHHxVv8NBDD8m7774r27Ztc7oUAADKROgGAKAUe/bs8dxeeeUViYiIKLJNw1918M4770iPHj2kcePGTpcieXl5Z/we9evXl379+smbb75ZITUBAGAToRsAgFLExMR4bpGRkaZ1u/C2jz/+WNq0aSM1a9aU1q1byxtvvOH52t9//93sP3PmTLngggskJCREunXrJps3b5affvpJunbtKuHh4dK/f385cOCA5+vuuOMOGTRokIwbN06ioqJM0B8xYkSRsPqf//xHzjnnHPOe9erVk0suuUSysrJKPQ6tc+DAgSdsLygokL/+9a9St25dczzFW+4PHz4sd911l6eOiy++WH7++ecTai1Mu6xr13U3fTxq1Ciz3R2WVWJiojl2/Qyio6Pltttuk4MHD5b7GPV49LgAAKjqCN0AAJyGDz/8UMaOHStPP/20bNq0SZ555hkzblq7PRf2xBNPyGOPPSZr1qyRwMBAufnmm03Q1e7e33//vWzZssW8T2ELFy4077l48WL56KOPZPbs2SaEK21hv+mmm2T48OGefQYPHiwul6vEOv/44w/ZuHGjCfnFaa1hYWGyYsUKef755+XJJ5+Ub775xvP69ddfL/v375cvvvhCVq9eLQkJCdK3b1/znqdCv0+NGjVk2bJlMmnSJBPmNcB37txZVq1aJV9++aXs27dPhgwZUu5jPPfcc2Xnzp3m4gYAAFVZoNMFAABQHWmYfvHFF00YVE2bNjXhdvLkyTJ06FDPftoF3d26e//995swqaG6Z8+eZtudd94p06ZNK/LeGlCnTJkioaGh0q5dOxOGH374YfnnP/9pAumxY8fM93V3F9cW4dJs377dhNW4uLgTXuvQoYM5DnX22WfL66+/bmq79NJLZenSpbJy5UoTuoODg80+L7zwgsydO9e0QheelK0s+t4a6t2eeuopE7j1QoWbHm98fLzpCZCZmVnmMbqPJyUlRZo0aVLuWgAAqGyEbgAATpF2c966dasJzHfffbdnuwZF7YZePNi6aTfq4gFSt2mwLaxjx44mcLudf/75Joju2LHDvKatzfoeGuYvu+wyue6666ROnTol1pqdnW3utQt8cYVrU7GxsZ5atBu5fk/t2l38/fTYT0WXLl2KPNf3XrRokelaXpy+tx5TWceo3c7VkSNHTqkWAAAqG6EbAIBTpGFUvf3229K9e/cirwUEBBR5HhQU5HmsY7xL2qZjq8tL31+7gP/www/y9ddfy2uvvWZmJdcu4traXpyOo1apqalmbHZptRWvRY9RQ7h27S6udu3a5t7f3/+Ebu1Hjx49YX/twl6YvreOyX7uuedO2Fe/Z3mO0d3FvfgxAQBQ1TCmGwCAU6St09q9WZesatGiRZFbScH3VGlLsLuFWv3444+mVVi7X7vDsXZP13Hea9euNd3R58yZU+J7NW/e3EyCpl3fT4WO39alxnQcevFjdAd5Dbza3b2wdevWleu9k5KSTLfw4u/tDuhlHaNOxKYXDbT7PQAAVRmhGwCA06BhcPz48fLqq6+accgbNmyQqVOnyksvvXTG760zlWvXdQ3KCxYsMOOudQZwbVnW1l4dC60TkOl4bZ1kTWc/11nUS6JfozN/6xjtU6Ffo93adXZybW3WCcu05VlbnPV7K50MTR+/99578ttvv5k6NQyXZeTIkaalWse360zu2qX8q6++kmHDhkl+fn65jlEnoXPPCg8AQFVG6AYA4DToUlq6/rUGbR173Lt3bzMhWkW0dOt4Zp187MILL5QbbrhBrrrqKs9yXtpqvWTJErniiiukZcuWZmZ0ndBNl986Wa26vNapdGPXlmYN/FqDhmH9XjfeeKOZuMw9Nl3HW+uM7Tobuy6HlpGRIbfffnuZ7629BHQmcw3YOl5bPz9dUky7retFgvIcox5P4fH0AABUVX6u0tYYAQAAlU7XvtYltXSW8Iqiv+p17Pno0aNN63J1p0uY/eUvf5H169eb7u8AAFRltHQDAODltNX6rbfeMrOre8vs8drDgMANAKgO+G0FAIAP6NSpk7l5A10+DACA6oLu5QAAAAAAWEL3cgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAOAN+fn7yj3/8o8p/75UrV0qNGjUkJSXFel2+ZvHixeZc/Oc//ylz3xtvvFGGDBlSKXUBAKoGQjcAwDoNJGXdCofH0aNHS0JCgtStW1dCQ0OlTZs25vXMzExH6l+wYIFjwbqiPProo3LTTTdJ48aNT3htzpw50r9/f6lfv74J5nFxcSYYfvvtt+Lr/vvf/8pFF11kPpvatWvLueeeK++///5pv9+YMWPkk08+kZ9//rlC6wQAVF2BThcAAPB+JwspGma3bt0q3bt392z76aef5IILLpBhw4ZJzZo1Ze3atfLss8+aALRkyRLx9/ev9NA9ceLEEoN3dna2BAZW7V+n69atM5/dDz/8UGS7y+WS4cOHy7Rp06Rz587y4IMPSkxMjOzZs8cE8b59+8qyZcukR48e4os+++wzGTRokJx//vnm3OvFoZkzZ8rtt98uBw8eNBeHTpV+zl27dpUXX3xR3nvvPSt1AwCqlqr9VwIAwCvceuutJW5/5513TOC+7777TEur29KlS0/Yt3nz5vLQQw+ZbtLnnXeeVBV6UaCqmzp1qjRq1OiEz02DnwbuBx54QF566SUTKgu3jOvFkqp+QcGm119/XWJjY02Lf3BwsNn2f//3f9K6dWvzuZ1O6Fbai+CJJ56QN954Q8LDwyu4agBAVUP3cgCAI5KSkuTPf/6zafn717/+Veb+TZo0MfeHDx8uc9/9+/fLnXfeKdHR0SYUd+zYUd59990i+/z+++8mZL7wwgvy8ssvm27XISEh0rt3b0lMTPTsd8cdd5hWblW4O7xb8a7x7hbRzZs3m4sNkZGREhUVJY8//rhpWd6xY4dcffXVEhERYVqVNfgWlpeXJ2PHjpUuXbqYrw0LCzOt/osWLZLTNXfuXLn44ouL1K0t9OPHjzcBUj+Dwq+53XbbbaY7tdKQqfvoBRE9b3pM2t1aQ6jWrOdFW4Dr1Kljbn/961/N8Ram30dbzevVq2c+az3G4uOg9QKBfp8pU6YU2f7MM8+Y7drroLKkp6ebY3EHbqUXIbSrudZfXEFBgTz99NPSsGFD83OnPQW2bNlywn6XXnqpZGVlyTfffGP9GAAAzvPdy9cAAMccOXLEtPYFBATIxx9/XCTUuB07dswEOQ10GoIfe+wxqVWrlicElkbDZJ8+fUzYGTVqlDRt2lRmzZplwrO+3/33319kf+3im5GRISNHjpScnByZMGGCCagbNmwwoV1D5e7du01AOpWxvDfccIMZi67d4j///HN56qmnzBj1yZMnm/d/7rnn5MMPPzSt9926dZMLL7zQE/S0B4COv7777rtNbf/+97+lX79+ppW/U6dOcip27dol27dvN2PkC9Pw/Mcff5hWbj0P5aW9EvRiwbhx4+THH3+Ut956y4Rv7bqurekajjUY64WU9u3bmyDupp/tVVddJbfccos5r3rur7/+epk/f74MGDDA7KNDCmbPnm26ums4jY+PN+dCv59eSLniiitOWp+O+9fzWJagoCBzUeNk9OdIz5NeMBk6dKgJ/dOnT5dVq1aZbubF6bnWoQ96TtPS0uT55583x7pixYoi+7Vt29aEdu26f80115RZKwCgmnMBAFDJhg8frk2grnfffbfUfZYvX272cd9atWrlWrRoUZnv/corr5j9P/jgA8+2vLw81/nnn+8KDw93paenm23Jyclmv5CQENfOnTs9+65YscJsHz16tGfbyJEjzbaS6PYnnnjC81wf67Z77rnHs+3YsWOuhg0buvz8/FzPPvusZ3tqaqr5/kOHDi2yb25ubpHvoftFR0ebz+1k37sk//3vf81+8+bNK7J9woQJZvucOXNc5TF16lSzf79+/VwFBQWe7fq56nGNGDHihOPt3bt3kfc4cuRIked6Xtq3b++6+OKLi2zfs2ePq27duq5LL73UfBadO3d2NWrUyJWWllZmnfpZFv65Ke1WvLaSZGZmuoYMGWKOz/11oaGhrrlz5xbZT38u9bU2bdoUOXfuz3jDhg0nvHfLli1d/fv3L7MGAED1R0s3AKBSaUuhdh3WrsuFW0GL09ZAbV3WbrjaiqoTgZVn9nJtZdWWWG0pLtyqqV2iddt3330nV155pec1nSjrrLPO8jzXlnSd1E3fR8c5n6677rrL81hbknXyrJ07d5rWWjdtIW7VqpVs27atyL7ulmftrqyt83qvX79mzZpTruPQoUPmXrtJF6Yt6kp7D5wKrb9wV3T9rJYvX17kuNzHu3r16iJfW7hLdmpqquTn55uu8x999FGR/fT8aZd+PV/6uk4Epz8L2iW/LNqtvbQ5BAor/nmURHtgtGzZUq677joZPHiwqVdb9vX9tZ7iY+S1lV5nf3fT2pWeX231L/79dTI2AID3I3QDACrNb7/9JiNGjDBBRieROhkNWJdccol5rGOgNazrvQZPHaNdGl2H+uyzzz5hhnPt6u1+vTDdtzitr6Tuw6dCu1oXpl2ZdZyvjgcuvt0djN10/LmO9f7ll1/k6NGjnu3aVf50FR9f7Q6w2n39TI9LaTfw4ts1WBem3ci1m72G6NzcXM/2ksaT63rWH3zwgemaf88995jx0eWhF2v0VhF0eIJ2odefOffPkw6LaNeunRmmULzbePHPxh3si38O7vNR0nEDALwPE6kBACqFhiwd5+wey3uqszZrS6PSr60OShonXdrY6cKBWIOmjj/X2dp1LPeXX35pWlV1HLi2eJ8qnbSspOCnE6gpHS99Kko7hpK2Fz6u77//3ozn1gsPesFFexLocd18880nXBBQeiFCx06rjRs3lvvYdSz13r17y7zpePaT0Z9T/fx1rHnhCzjaa0Jn2tfadJ+yPoPin4Obno/iF2AAAN6J0A0AqBQ6uZSut62TS+mM5acT2jV4aag6GZ2FXFvUi4c0bTV2v16Y7luczjzuni1dVWaLpM7m3axZMzOZmHbB1wnUtMW/PJODlcQdrpOTk4ts79Wrl2mJ1a7d2m3atk8++cQE7q+++sqsDa7B1d2ToSQ6sZ22wusM6zrp2yuvvFKu76Mt0LrMV1k390Wc0mjo18n8SvpstPeB/nyd7uem76uz2Lt7XwAAvBuhGwBg3Zw5c8yax9rSqWOrT0bHMBfuUu2mM3orHSt8Mjq7tbZkzpgxo0jIee2110zrui4JVnw5LZ3h201nCNduw4XXDddlu9y12eZuLS3cOqr16Ljp06Hj1bXrt7vV2C00NFTGjBkjmzZtMvcltcZqq7t+HhV1XHrxonBQ1WXb9PMv6cKDnj+dDfxvf/ub6Wqus9frxZDyjOnWFvSybsWXaiuuQYMGZsy9/uwWbtHWeQXmzZtnLmaUtGxYeWjLvV5E0eXTAADejzHdAACr9uzZYybZ0tCl43I1yJVEu1Off/75snjxYhPMdfIqHW+tgUe7JmvLrwbusibJ0vG/uiyXdtHWiby0xVpDnC7PpK2lxScOa9GihWn1vffee01ruu6jXbI1vLnpetJK69KWZz0WDYI26CRveqy6lJR2bdYW6kmTJplxyuWZSK4kOhZew2PxccQPP/ywWS9dA6iuA66fuU5iphctNAxr4NZJ7CqCHotOTHf55ZebLuW6lrpOlqaf//r16z376XY9FxdddJEZU630go3Wp+dUW72Lj9e3MaZbz7H2ztCwrxOm6aR/esFAu5zrhHil/RyXh4Z+veihS6IBALwfoRsAYNWvv/7qGU9cfI3swnQdZA3d55xzjglcn376qQnsGhQ1kI8dO9aExMKzQ5dEWx81uGsLqU5IprN06wzhU6dONaGtOA1TGuI0bGvg09nLNeRpF2Q37Yqs61PreHINW1qTrdCtNWro1QsH2hVbA6R+T11rXI/rdGh3bj0mvfCgFxjc9Lh1nXIN5Tor9wsvvGA+r6ioKLNuuA4F0HNSEXRMugZWbb3WtcF1UjhdA1tbuwuHbvfFDz1f7gsEehFE69M6tcbCF0RsevTRR02dur64rhOudXXo0MFcxLn22mtP+331XOrP1KnOHA8AqJ78dN0wp4sAAKCyadjTQPWvf/3LtGh6O+1lEBcXJ++//77Tpfg0nbk9ISHBzIjeqVMnp8sBAFQCxnQDAOADnnnmGTNOuviSaahc2tKv3fgJ3ADgO+heDgCAD+jevfsJS1yh8lWXJe8AABWHlm4AAAAAACxhTDcAAAAAAJbQ0g0AAAAAgCWEbgAAAAAAfHUitYKCAtm9e7dZy9K9XicAAAAAAE7SkdoZGRlmSU5/f//qG7o1cMfHxztdBgAAAAAAJ9ixY4c0bNhQqm3o1hZu94FEREQ4XQ4AAAAAAJKenm4aiN2ZtdqGbneXcg3chG4AAAAAQFVS1jBoJlIDAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEuq/DrdbhdefKUEBFabcoHTEhdTX+bNnSm+aOD1V8ueg3udLgOV6ODOvdKmQZTTZaCS1YmOlemz5zldBgAAlabapNiY8+6VoOBQp8sArNq9bIL4Kg3czUYkOF0GKtHOv8+RiVc0droMVLKRC1KcLgEAgEpF93IAAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwJtPXGqF7mvXi1uR88Zp5E1w2VEYM7SOsmdSU375h8t2aXTJmXKMfyXU6XCVR7M29409zf8+kYubvrzdK0TrxEBNeS9JwMWZKyQmZsmCcu4d+aN2n26CfmPvnZGyXi3AFSq2NfCaobI35+/rL7/bGSsz3J6RIBAIBFtHSjiAB/P3l8eHdp06SufPjlJlnz634ZeEEzufHSVk6XBniV0KAQOSsiRhZuXSrvrp1lgvbgtv2l39m9nS4NFvkFBsmRLavlWNpBp0sBAACVhJZuFNG+eX2JiwqXH9bvljmLt0pwjQDp1fEsubJXM/ngy1+cLg/wGoeyD8voL8aJy3W8VTvQP1CGJQyRJrUbOl0aLDr8/SxzX7NhKwmq3cDpcgAAQCWgpRtFNImNMPcHUrPNfW5evqRn5UlYSJDUDg92uDrAexQU5HsCt5/4SUJce/N4wz4ubgEAAHgTWrpRJj+nCwC8mLZwj+w+VDrGtJUFm7+VZdtXOV0SAAAAKhChG0X8vifd3EfVCTH32r28VlgNyco+Koczcx2uDvC+cd0P9xoh7Rq0lFmJ82VW0udOlwQAAIAKRuhGEYlbD8rug5nStU20XNOnuTSNi5TAAH+ZvWyL06UBXsXfP0Ce7PuQNIqMk7V7kmRX+j7pEd9V0nIzJGn/r06XB0tqxreVoHqxEhB6fChPaIsuZibzjHULnS4NAABUlTHdd9xxh/j5+cmIESNOeG3kyJHmNd3HbeLEidKkSROpWbOmdO/eXVauXHnmVaNC1QoNMvc5ucckJy9fnp6yUjb9/ofcenkb6dI6WuYv3SYffU0IAM5UeI0wc59zLFcigsNN4FadY9vJAz3uNLfr2l3hcJWoSP4h4ea+IC9HXPlHpVbHiyVqwJ8kqE6M2V77/KvNcwAA4L1Oq6U7Pj5ePv74Y3n55ZclJOR4N+ScnByZPn26NGrUyLPfjBkz5MEHH5RJkyaZwP3KK69Iv3795Ndff5UGDZi1tSro0SFWBvVuYR5v2Hp8CZvt+zLksUk/OFwZ4F26N+wsV7bqax4n7d8sB7IOyZAZ9zpdFiwKa32eRHYfaB5npySa+wPzXzc3AADgO05r9vKEhAQTvGfPnu3Zpo81cHfu3Nmz7aWXXpK7775bhg0bJm3btjXhOzQ0VKZMmVIx1eOMdWsTIzH1QmXJ2p3y2sx1TpcDeC2dnTw6PMpMlDb5pw+cLgeVQLuOB9aOkcykpXJwwZtOlwMAAKrbmO7hw4fL1KlT5ZZbbjHPNUhruF68eLF5npeXJ6tXr5ZHHnnE8zX+/v5yySWXyPLly0t939zcXHNzS08/PrEX7JgwY63TJQA+4c2V7ztdAirZgfkTnS4BAABU53W6b731Vlm6dKmkpKSY27Jly8w2t4MHD0p+fr5ER0cX+Tp9vnfv3lLfd/z48RIZGem5aYs6AAAAAAA+1dIdFRUlAwYMkGnTponL5TKP69evf8YFacu4jgMv3NJN8Lbn6Xt7SLO4SAmuEShpmbmyPHGPTPksSa7ve7bc3K+1TP/qFyZRAypAWFCo/Kn77dK0TrxEBNeS9JwMWZKyQmZsmCcXNulu1upenLxc3lj5ntOlooL41wyTqIGjJDimmfiHRkhBVppkJC6R1MUfSXiHPtJg4CjJ+HkRY7wBAPByZ7RkmHYxHzVqlGeW8sI0gAcEBMi+ffuKbNfnMTHHZ20tSXBwsLmhciTvSpfv1uwSEZeZUG1gr2ayc3+m02UBXic0qKacFREjC7culfTcTBnUpp8MbttfDuekS/bRHKfLgwX+waESVK+hpK/9RvKPpEvtHoOlTs9rJT8z1cxmDgAAfMMZhe7LL7/cjN3WZcJ0VvLCatSoIV26dJGFCxfKoEGDzLaCggLz3B3U4bx3PkuU8JAgCQsJkh4d4iQ+upaIy+V5PbZemDw1ooecHV9HtuxMlefeWyXpWXmO1gxUR4eyD8voL8aZnkEq0D9QhiUMkSa1G8qmA1vMNl1G7OFeI6RdVEvZm3lAXl7+juzLPOBw5Thdx9IPyc7J94u4Csxzv4AgqX/ZcKkR3VRydmwy2wLCIiT6+jES0qidHE3dK/vmvCTHUksfggUAAHxoTLfSluxNmzbJxo0bzePitJv422+/Le+++67Z795775WsrCwz4RqqjsmP9JV3Hr3UrMm9aPUO+XpFiue17u1jZEXiXvl9T5p0aBElA3o2dbRWoLoqcBV4Aref+JnZzNWGfb949ukQ01Z+O5QsGw/8Js3qNpJr2/Z3rF5UAA3b/wvcetZDWySYR9nJ6z27hDTtKLm7Nkv29o0SHNtc6vS8zqFiAQBAlWzpVhEREaW+dsMNN8iBAwdk7NixZvK0Tp06yZdffnnC5Gpw1jPTfpI6tYLlmj4t5MJOZ8mPG/Z4Xlu0eqfMW7pNco/mS9um9SS2fpijtQLVnbZw6/jtjjFtZcHmb80SYr2bnGdeW793o8zd9JWcE91aup7VQWLCo5wuFxUhIFAaDLxPQpt1krSVn0vWxqUS3uEi81J28s9y+Ic5EtK0g4S17CZBdUsffgUAAHwkdOvEaSczd+7cIs+1Kzndyau2pG2HPI/H3N5N+nZrJFt2HjbPdXI1lV9wvLUmwN/PoSqB6i80KOR49/EGLWVW4nyZlfR5kdd1rLfKL8g39/7+J/YgQvUb1226jzduL6lLZkjq9zOLvJ6fdXxZTFf+8XMunHMAALzOGbd0o/pKaNVAeic0lE3Jh0T8/GRgr+Ndx5N3pzldGuB1ggOD5cm+D0mjyDhZuydJdqXvkx7xXSUtN8Pp0mCJX1BNibv9aanRoJEc2bpG8g7tkrC2PSU/i/9jAQDwJYRuH6YTojWOrSXntY+VgAA/OZSWLbMWbjZLhA25pKXT5QFeJaJGmAncqnNsO3NTSfs3m6XC4H0CQmuZwK1CmyeYm8pOSZSM9Ysdrg4AAFQWP5d7Zp8qStfpjoyMlH4jp0tQcKjT5QBW7V42QVb/+K34oq4XdZdmI46HEviGJX+fIz8M7+l0GahkIxekyBfLVjldBgAAFZZV09LSTjrX2RnNXg4AAAAAAEpH6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwJFCqib0/vikBgdWmXOC0xMXUF18VWz9Gtk1a43QZqEQ1/YNl5IIUp8tAJasTHet0CQAAVCo/l8vlkiosPT1dIiMjJS0tTSIiIpwuBwAAAAAAKW9WpXs5AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAkkBbb4wzd/PggZK6b4/TZaAS/b7ngIQ2aO50GUCl2H8oWaIbNnC6DFSy2PoxMm/Wp06XAQBApSF0V2EauCde0djpMlCJrpy0Q+J63u90GUCl2D7nXmk2IsHpMlDJtk1a43QJAABUKrqXAwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgSaCtNwbKq9mjn5j75GdvlIhzB0itjn0lqG6M+Pn5y+73x0rO9iSnS4SXmffi1eZ+8Jh5El03VEYM7iCtm9SV3Lxj8t2aXTJlXqIcy3c5XSa8xMwb3jT393w6Ru7uerM0rRMvEcG1JD0nQ5akrJAZG+aJS/h5AwDAW9HSjSrFLzBIjmxZLcfSDjpdCnxAgL+fPD68u7RpUlc+/HKTrPl1vwy8oJnceGkrp0uDFwoNCpGzImJk4dal8u7aWSZoD27bX/qd3dvp0gAAgEW0dKNKOfz9LHNfs2ErCardwOly4OXaN68vcVHh8sP63TJn8VYJrhEgvTqeJVf2aiYffPmL0+XByxzKPiyjvxgnLtfxVu1A/0AZljBEmtRu6HRpAADAIlq6AfisJrER5v5Aara5z83Ll/SsPAkLCZLa4cEOVwdvU1CQ7wncfuInCXHtzeMN+7jAAwCAN6OlGwAK8XO6AHg9beEe2X2odIxpKws2fyvLtq9yuiQAAGARoRuAz/p9T7q5j6oTYu61e3mtsBqSlX1UDmfmOlwdvHVc98O9Rki7Bi1lVuJ8mZX0udMlAQCAqtS9/I477hA/Pz8ZMWLECa+NHDnSvKb7qCVLlsjAgQMlLi7ObJ87d27FVQ2vVTO+rdTq1FcCQo93+w1t0cU8B2xI3HpQdh/MlK5touWaPs1l5HUdJTDAXz5flux0afBC/v4B8mTfh0zgXrsnSXal75Me8V2lXQMm7gMAwJudckt3fHy8fPzxx/Lyyy9LSMjx1qGcnByZPn26NGrUyLNfVlaWdOzYUYYPHy6DBw+u2KrhNfxDws19QV6OuPKPSq2OF0utjhd5Xq99/vGlnTLWLXSsRniXWqFB5j4n95jk5OXL01NWyj3XnCO3Xt7GPJ+/dJt89PWvTpcJLxFeI8zc5xzLlYjgcGkUGWeed45tZ24qaf9mSdrPzxwAAN7qlEN3QkKCbN26VWbPni233HKL2aaPNXA3bdrUs1///v3NDShNWOvzJLL7QPM4OyXR3B+Y/7q5ATb06BArg3q3MI83bD2+LN32fRny2KQfHK4M3qh7w85yZau+nmB9IOuQDJlxr9NlAQCA6jB7ubZeT5061fN8ypQpMmzYsIqsCz5Au44H1o6RzKSlcnDBm06XAx/QrU2MxNQLlSVrd8prM9c5XQ68nM5OHh0eZSZKm/zTB06XAwAAqtNEarfeeqs88sgjkpKSYp4vW7bMdDlfvHjxGReUm5trbm7p6ccnOoL3OTB/otMlwMdMmLHW6RLgQ95c+b7TJQAAgOoauqOiomTAgAEybdo0s+aoPq5fv36FFDR+/HgZN25chbwXAAAAAADVcskw7WI+atQo83jixIprsdQW9AcffLBIS7dO3gbv418zTKIGjpLgmGbiHxohBVlpkpG4RFIXfyThHfpIg4GjJOPnRYzxRoV5+t4e0iwuUoJrBEpaZq4sT9wjUz5Lkuv7ni0392st07/6hUnUUGHCgkLlT91vl6Z14iUiuJak52TIkpQVMmPDPLmwSXezVvfi5OXyxsr3nC4VAABUxdB9+eWXS15enlkOrF+/fhVWUHBwsLnB+/kHh0pQvYaSvvYbyT+SLrV7DJY6Pa+V/MxUM5s5UNGSd6XLd2t2iYjLTKg2sFcz2bk/0+my4KVCg2rKWRExsnDrUknPzZRBbfrJ4Lb95XBOumQf5f84AAB8xWmH7oCAANm0aZPncXGZmZmyZcsWz/Pk5GRZt26d1K1bt8jSYvBdx9IPyc7J94u4Csxzv4AgqX/ZcKkR3VRydvzvZyssQqKvHyMhjdrJ0dS9sm/OS3Isda/DlaO6euezRAkPCZKwkCDp0SFO4qNribhcntdj64XJUyN6yNnxdWTLzlR57r1Vkp6V52jNqL4OZR+W0V+MM8OwVKB/oAxLGCJNajeUTQeO/37UZcQe7jVC2kW1lL2ZB+Tl5e/IvswDDlcOAAAcn73cLSIiwtxKsmrVKuncubO5Ke0yro/Hjh17Jt8S3kTD9v8Ct4ifhLZIMI+yk9d7dglp2lFyd22W7O0bJTi2udTpeZ1DxcJbTH6kr7zz6KXSpXW0LFq9Q75ecXxCSNW9fYysSNwrv+9Jkw4tomRAz/+/DCJwqgpcBZ7A7Sd+ZjZztWHfL559OsS0ld8OJcvGA79Js7qN5Nq2LLUJAIBPt3TrxGknM3fuXM/jPn36eP7YAE4qIFAaDLxPQpt1krSVn0vWxqUS3uEi81J28s9y+Ic5EtK0g4S17CZBdWOcrhbV3DPTfpI6tYLlmj4t5MJOZ8mPG/Z4Xlu0eqfMW7pNco/mS9um9SS2fpijtcI7aAu3jt/uGNNWFmz+1iwh1rvJeea19Xs3ytxNX8k50a2l61kdJCY8yulyAQBAVeleDlTUuG7Tfbxxe0ldMkNSv59Z5PX8rONLxrny8//3BScOZQBORdK2Q57HY27vJn27NZItOw+b5zq5msovON4DI8Dfz6Eq4S1Cg0KOdx9v0FJmJc6XWUmfF3ldx3qr/ILj/8f5838cAABeh9ANx/gF1ZS425+WGg0ayZGtayTv0C4Ja9tT8rPSnC4NXiihVQPpndBQNiUfEvHzk4G9jncdT97NzxvsCA4Mlif7PiSNIuNk7Z4k2ZW+T3rEd5W03AynSwMAAJWI0A3HBITWMoFbhTZPMDeVnZIoGesXO1wdvI1OiNY4tpac1z5WAgL85FBatsxauNksETbkkpZOlwcvFFEjzARu1Tm2nbmppP2bzVJhAADAN/i5qvjAa12nOzIyUtLS0kqdtM1b9e/ZVSZe0djpMlCJrpy0VJoPecvpMoBK8eOce+Wi8Vc7XQYq2bZJa2TVohVOlwEAQKVl1TOavRwAAAAAAJSO0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgSaCtN8aZqxMdKyMXpDhdBiqRK6im7F42wekygEpRMyBYtk1a43QZqGSx9WOcLgEAgEpF6K7Cps+e53QJAAAAAIAzQPdyAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAAPDVdbpdLpe5T09Pd7oUAAAAAACKZFR3Zq22ofvQoUPmPj4+3ulSAAAAAAAoIiMjQyIjI6Xahu66deua++3bt5/0QOBdV4z0IsuOHTskIiLC6XJQCTjnvodz7ps4776Hc+57OOe+x5fPucvlMoE7Li7upPtV+dDt73982LkGbl87ib5Ozzfn3Ldwzn0P59w3cd59D+fc93DOfY+vnvPIcjQMM5EaAAAAAACWELoBAAAAAPDV0B0cHCxPPPGEuYdv4Jz7Hs657+Gc+ybOu+/hnPsezrnv4ZyXzc9V1vzmAAAAAADAO1u6AQAAAACorgjdAAAAAABYQugGAAAAAMAXQ/fEiROlSZMmUrNmTenevbusXLnS6ZJgyfjx46Vbt25Sq1YtadCggQwaNEh+/fVXp8tCJXr22WfFz89PHnjgAadLgWW7du2SW2+9VerVqychISFyzjnnyKpVq5wuC5bk5+fL448/Lk2bNjXnu3nz5vLPf/5TmFLGuyxZskQGDhwocXFx5v/yuXPnFnldz/fYsWMlNjbW/Bxccskl8ttvvzlWL+ye86NHj8qYMWPM/+9hYWFmn9tvv112797taM2w+++8sBEjRph9XnnllUqtsaqqsqF7xowZ8uCDD5qZ8NasWSMdO3aUfv36yf79+50uDRZ89913MnLkSPnxxx/lm2++Mf9ZX3bZZZKVleV0aagEP/30k0yePFk6dOjgdCmwLDU1VXr27ClBQUHyxRdfyMaNG+XFF1+UOnXqOF0aLHnuuefkzTfflNdff102bdpknj///PPy2muvOV0aKpD+vta/1bTBpCR6zl999VWZNGmSrFixwgQx/bsuJyen0muF/XN+5MgR8/e7XnDT+9mzZ5vGlKuuusqRWlE5/87d5syZY/6m13COKj57ubZsa8un/pJWBQUFEh8fL/fdd5/87W9/c7o8WHbgwAHT4q1h/MILL3S6HFiUmZkpCQkJ8sYbb8hTTz0lnTp14qqoF9P/v5ctWybff/+906Wgklx55ZUSHR0t//73vz3brr32WtPa+cEHHzhaG+zQ1i39o1t7rSn9U1P/+P7LX/4iDz30kNmWlpZmfi6mTZsmN954o8MVo6LPeWkX2M8991xJSUmRRo0aVWp9qLxzrr3ZNMd99dVXMmDAANOD8QF6MVbNlu68vDxZvXq16Xrk5u/vb54vX77c0dpQOfSXsapbt67TpcAy7eGg/ykX/vcO7/XZZ59J165d5frrrzcX1jp37ixvv/2202XBoh49esjChQtl8+bN5vnPP/8sS5culf79+ztdGipJcnKy7N27t8j/85GRkeYPc/6u862/7TSo1a5d2+lSYIk2kt52223y8MMPS7t27Zwup0oJlCro4MGDZgyYXgEtTJ//8ssvjtWFyvsHq1fEtAtq+/btnS4HFn388cem25le/YZv2LZtm+lqrMOH/v73v5tz/+c//1lq1KghQ4cOdbo8WOrdkJ6eLq1bt5aAgADz+/3pp5+WW265xenSUEk0cKuS/q5zvwbvpsMIdIz3TTfdJBEREU6XA0t0+FBgYKD5vY5qELrh27TlMzEx0bSEwHvt2LFD7r//fjOGXydLhO9cVNOW7meeecY815Zu/feu4zwJ3d5p5syZ8uGHH8r06dNNy8e6devMhVXtbsw5B7yfztMzZMgQM8xAL7rCO2kv5QkTJpjGFO3RgGrQvbx+/frmavi+ffuKbNfnMTExjtUF+0aNGiXz58+XRYsWScOGDZ0uB5b/c9aJEXU8t14V1ZuO4deJdvSxtobB++jMxW3bti2yrU2bNrJ9+3bHaoJd2s1QW7t13K7OZKxdD0ePHm1WrYBvcP/txt91vhu4dRy3XmSnldt76Vwt+nedjtd3/12n513ncmjSpIn4uioZurWbYZcuXcwYsMKtI/r8/PPPd7Q22KFXPzVw64QM3377rVlaBt6tb9++smHDBtPq5b5pC6h2OdXHeuEN3keHjRRfDlDH+jZu3NixmmCXzmKs87IUpv++9fc6fIP+TtdwXfjvOh1yoLOY83ed93IHbl0a7r///a9ZJhLeSy+orl+/vsjfddqjSS+8fvXVV+Lrqmz3ch3vp93O9I9wnelQZzPWaeqHDRvmdGmw1KVcux5++umnZq1u9xgvnWhFZ7iF99HzXHzMvi4ho7+UGcvvvbSFUyfW0u7l+sfYypUr5a233jI3eCdd01XHcGvrh3YvX7t2rbz00ksyfPhwp0tDBa9EsWXLliKTp+kf3Tohqp57HVKgK1ScffbZJoTrUlL6B/nJZrtG9T3n2qvpuuuuM12NtQej9l5z/22nr2sDG7zv33nxCyu6PKhecGvVqpUD1VYxrirstddeczVq1MhVo0YN17nnnuv68ccfnS4JluiPYkm3qVOnOl0aKlHv3r1d999/v9NlwLJ58+a52rdv7woODna1bt3a9dZbbzldEixKT083/67193nNmjVdzZo1cz366KOu3Nxcp0tDBVq0aFGJv8eHDh1qXi8oKHA9/vjjrujoaPNvv2/fvq5ff/3V6bJh6ZwnJyeX+redfh288995cY0bN3a9/PLLlV5nVVRl1+kGAAAAAKC6q5JjugEAAAAA8AaEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAIAPePzxx+Wee+7xPO/Tp4888MADUh397W9/k/vuu8/pMgAAKBdCNwAApfDz8zvp7R//+IdUB3v37pUJEybIo48+Kt7goYceknfffVe2bdvmdCkAAJSJ0A0AQCn27Nnjub3yyisSERFRZJuGv+rgnXfekR49ekjjxo2dLkXy8vLO+D3q168v/fr1kzfffLNCagIAwCZCNwAApYiJifHcIiMjTet24W0ff/yxtGnTRmrWrCmtW7eWN954w/O1v//+u9l/5syZcsEFF0hISIh069ZNNm/eLD/99JN07dpVwsPDpX///nLgwAHP191xxx0yaNAgGTdunERFRZmgP2LEiCJh9T//+Y+cc8455j3r1asnl1xyiWRlZZV6HFrnwIEDT9heUFAgf/3rX6Vu3brmeIq33B8+fFjuuusuTx0XX3yx/PzzzyfUWph2Wdeu6276eNSoUWa7OyyrxMREc+z6GURHR8ttt90mBw8eLPcx6vHocQEAUNURugEAOA0ffvihjB07Vp5++mnZtGmTPPPMM2bctHZ7LuyJJ56Qxx57TNasWSOBgYFy8803m6Cr3b2///572bJli3mfwhYuXGjec/HixfLRRx/J7NmzTQhX2sJ+0003yfDhwz37DB48WFwuV4l1/vHHH7Jx40YT8ovTWsPCwmTFihXy/PPPy5NPPinffPON5/Xrr79e9u/fL1988YWsXr1aEhISpG/fvuY9T4V+nxo1asiyZctk0qRJJsxrgO/cubOsWrVKvvzyS9m3b58MGTKk3Md47rnnys6dO83FDQAAqrJApwsAAKA60jD94osvmjComjZtasLt5MmTZejQoZ79tAu6u3X3/vvvN2FSQ3XPnj3NtjvvvFOmTZtW5L01oE6ZMkVCQ0OlXbt2Jgw//PDD8s9//tME0mPHjpnv6+4uri3Cpdm+fbsJq3FxcSe81qFDB3Mc6uyzz5bXX3/d1HbppZfK0qVLZeXKlSZ0BwcHm31eeOEFmTt3rmmFLjwpW1n0vTXUuz311FMmcOuFCjc93vj4eNMTIDMzs8xjdB9PSkqKNGnSpNy1AABQ2QjdAACcIu3mvHXrVhOY7777bs92DYraDb14sHXTbtTFA6Ru02BbWMeOHU3gdjv//PNNEN2xY4d5TVub9T00zF922WVy3XXXSZ06dUqsNTs729xrF/jiCtemYmNjPbVoN3L9ntq1u/j76bGfii5duhR5ru+9aNEi07W8OH1vPaayjlG7nasjR46cUi0AAFQ2QjcAAKdIw6h6++23pXv37kVeCwgIKPI8KCjI81jHeJe0TcdWl5e+v3YB/+GHH+Trr7+W1157zcxKrl3EtbW9OB1HrVJTU83Y7NJqK16LHqOGcO3aXVzt2rXNvb+//wnd2o8ePXrC/tqFvTB9bx2T/dxzz52wr37P8hyju4t78WMCAKCqYUw3AACnSFuntXuzLlnVokWLIreSgu+p0pZgdwu1+vHHH02rsHa/dodj7Z6u47zXrl1ruqPPmTOnxPdq3ry5mQRNu76fCh2/rUuN6Tj04sfoDvIaeLW7e2Hr1q0r13snJSWZbuHF39sd0Ms6Rp2ITS8aaPd7AACqMkI3AACnQcPg+PHj5dVXXzXjkDds2CBTp06Vl1566YzfW2cq167rGpQXLFhgxl3rDODasqytvToWWicg0/HaOsmazn6us6iXRL9GZ/7WMdqnQr9Gu7Xr7OTa2qwTlmnLs7Y46/dWOhmaPn7vvffkt99+M3VqGC7LyJEjTUu1jm/Xmdy1S/lXX30lw4YNk/z8/HIdo05C554VHgCAqozQDQDAadCltHT9aw3aOva4d+/eZkK0imjp1vHMOvnYhRdeKDfccINcddVVnuW8tNV6yZIlcsUVV0jLli3NzOg6oZsuv3WyWnV5rVPpxq4tzRr4tQYNw/q9brzxRjNxmXtsuo631hnbdTZ2XQ4tIyNDbr/99jLfW3sJ6EzmGrB1vLZ+frqkmHZb14sE5TlGPZ7C4+kBAKiq/FylrTECAAAqna59rUtq6SzhFUV/1evY89GjR5vW5epOlzD7y1/+IuvXrzfd3wEAqMpo6QYAwMtpq/Vbb71lZlf3ltnjtYcBgRsAUB3w2woAAB/QqVMnc/MGunwYAADVBd3LAQAAAACwhO7lAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAiB3/D3+LejJbVR1aAAAAAElFTkSuQmCC", + "image/png": "iVBORw0KGgoAAAANSUhEUgAAA90AAAJOCAYAAACqS2TfAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjgsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvwVt1zgAAAAlwSFlzAAAPYQAAD2EBqD+naQAAYRhJREFUeJzt3Qd4VFX+//HvpJJCQgspErp0KQFEAQVFRUQUUbGLYPnhgqu4uqyr4uKqqGtDRUFdwIYCK6AgtkUQQQRpQgKKQAy9GtJIgWT+z/dkZ/5JSEiAnEwy8349zzwzc+dm5txzJ5DPPc3hdDqdAgAAAAAAKp1f5b8lAAAAAAAgdAMAAAAAYBEt3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAGDVP/7xD3E4HNRyNVJQUCAdOnSQp59+2tNF8WlLliwxvxv/+c9/yt33xhtvlKFDh1ZJuQAAlYvQDQA4ZcnJyTJ69Ghp1aqVhIaGmlu7du1k1KhRsmHDhiqv0U2bNplw//vvv4unNG3a1ASo0m45OTlmn+nTp5vnq1evPuGiRGm3yZMnF/uMrKws+ec//ykdO3Y0dR4ZGSkXXHCBvPfee+J0Oitc1o8++kh27txpzmFJ27Ztk//7v/+T5s2bS61atSQiIkJ69eolEydOlOzsbPFlepHiqquukujoaHN+9NxVxKWXXmr2L62+K2rs2LHyySefyM8//3za7wEA8IwAD30uAKCGWrBggdxwww0SEBAgt9xyi3Tq1En8/Pzkl19+kTlz5sibb75pQnmTJk2qNHSPHz9e+vbta8Kvp3Tu3Fn+8pe/nLA9KCio3J/VegsPDy+2rUePHu7H+/fvl379+snmzZtNq6cGOA3zGsSGDRsmCxculA8//FD8/f3L/ax//etf5j00tBf1+eefy/XXXy/BwcFy++23m9bwvLw8WbZsmTz88MOSlJQkb731lviqxx57TGJiYqRLly7y1VdfVehn9HdixYoVZ/zZ+pndunWTF1980VxkAQDUHIRuAECFaSuohjUN1IsWLZLY2Nhirz/33HPyxhtvmBDui8466yy59dZbT+tnr7vuOmnQoEGZr2uw1sA9d+5c09rq8uc//9kE4hdeeMEEM20RPZl169aZ1lINb0XphRLXuf3222+LnVvtwbB161YTyn2Z1pFe1Dl06JBERUWVu79eFNGLMHpOxo0bd8afr93Ln3jiCfM7VvICDQCg+vLNv4oAAKfl+eefN12cp02bdkLgVtr6rSEwPj7+pO9z/Phx0026RYsWplVVg8zf//53yc3NLbZfWV14df877rjD3WVbW2fVRRdd5O6areNlXTSktG/f3nxWXFycCZFHjhwp9p7aSq4tu9pqru+j3bc1ROsxe9qPP/5oWlb1mIsGbpcJEybI2WefbS56lNcFfN68eabl/cILLyy2XY8zMzNT/v3vf5d6blu2bCn333+/+7mru/Ts2bPN0IKQkBA5//zzZePGjeb1KVOmmJ/RLupatyW7/n///ffmvDVu3NicF/3OjBkzplj5Dxw4YMKt/nzR7vN6ASAsLMz0uKhKp9qLQutUx88/9NBDJ91P99Gu640aNTL1pT0a9BhL66auv3/ffPPNKZcdAOA5hG4AwCl1LdcgVbTb8+m46667TMtfQkKCvPzyy9KnTx8THLWl9VRpeNSgrzS4v//+++bWtm1bs01Du4ZsDdvaunvttdeaQHjZZZfJsWPHir1XamqqXH755abLvO7bpk0b00r5xRdfVKgs+n7aClr0dvTo0Qr97B9//FHs57QsLvPnzzf32uW7NHqx4+abbzY/s3z58pN+zg8//GAuLgQGBhbbrp+h47h79uwpFaXBWVtytRVe61lb4q+88kqZNGmSvPrqq/KnP/3JtMJr9+oRI0YU+1kN61o39957r7z22mvSv39/c1/0GBs2bGi63X/33XfmNVdA1YsPtWvXNhdTTvV8lHXT961MO3bskGeffdZcCNELEiej+2kPBg3njzzyiLnIokM3SnJd3CjvHAMAqhknAAAVkJaWpk2NzsGDB5/wWmpqqvPgwYPu29GjR92vPfHEE+bnXNavX2+e33XXXcXe46GHHjLbv/32W/c2fa4/X1KTJk2cw4YNcz+fPXu22Xfx4sXF9jtw4IAzKCjIedlllznz8/Pd219//XWz/9SpU93b+vTpY7a999577m25ubnOmJgY57XXXltu/WiZ9OdL3oqWf9q0aWbbTz/9dEL9lLzp+7lones2reeyzJkzx+zz6quvnrScjRo1OuF4XOf26quvdlaU7h8cHOxMTk52b5syZYrZrnWWnp7u3v7II4+Y7UX3LfodcZkwYYLT4XA4U1JSim2/6aabnKGhoc4tW7Y4//Wvf5n3mjdvXrll1O9DaXVb2q1o2cqj3/Gyvpsu1113nbNnz57u57r/qFGjSi1f27ZtzXfNZeLEiWb7xo0bT3jfVq1aOQcMGFDhsgIAPI8x3QCACklPTzf3pY0l1e6/RWdV1om6yupSqxN+qQcffLDYdm0x1XHJOm5Yu3dXhv/+979mIrAHHnig2Djzu+++27SK62cNHz7cvV2PreiYbO2Gfe6558r27dsr9HnaA+Cpp54qtk1bjytCJ0TTmcJdiraOZmRkmHtt3S2L6zXXeSrL4cOHpW7dusW2uX7mZO9fGu0GXbTLtasHhPYmKPperu1aj679ix6fdpnWbuXayq75VMeda7dzl9dff90MF9Bx71u2bJHbbrtNrr766nLLpz0WKtoVWydIqyyLFy8253PlypUV2l+/g0Un29MZ6V31pb0SitJzpy3zAICag9ANAKgQV4jScb8laXdtDYY6w3Z5E4mlpKSYAKzd1EuGnjp16pjXK4vrvVq3bl1suwYcDcMlP0vH1JZcU1xDTkWXQdOJ0C655JLTKqt2ky9rIjVX3Wsdax2VpiLB3KXk8mKusO96j4oqGoyVazb0kmP6XduLdpnX7tc6xOCzzz4rtl2lpaUVe16vXj3TXV3HgOtyXfq4IvTcne75OF06X4EOd9ALA927dz+tenRdFClZL65zx7r3AFCzELoBABWiwUkn2EpMTDzhNVdL5qmsk30mwSE/P19sKGu5rVNZA9sGHZ+uE6Bp+C85AZqL68KAjvs9mfr1658Q5jR065j30s7t6dRXefWo508nBdNx7DpmXsfO68Rou3fvNuO1Sxtf7VqiS8u+a9euMi8+FKW9HPQzKkInbKvIcmvl0eW8fv31V3MhquTvg17U0G06Vl0n6jud750ev06aBwCoOZhIDQBQYQMHDjSzKq9ateq0a02XpNJQ9dtvvxXbrq3kOqN40fW9tcWv5CzjGqT27t1boQDvei8NQSXfo6rXEj8TOjmZKmt9Zg2xM2bMMPXVq1evk76XBlw99tI+Q5eEq4w1pcujM5xrN3GdrE5Dt3YV1xZpDf6l+fLLL+Wdd96Rv/71ryYc68Rt2qJcHp00Ti8UVeS2c+fOSjk2bcHXCdz0PDRr1sx9c50/ffz111+f1nvrMWs5XZMEAgBqBkI3AKDCNPRoC53ORK0h+XRahK+44gpz/8orrxTb/tJLL7mDvYsuKbZ06dJi+7311lsntHRrK6kqGdA1yGlXcu2OXLRsuiyWdmEu+lnVmY511mPRpdp0BvmSHn30URNi9fyUN1O2LuulLdoll2fTn9V61JnlSzu3GsgnTpxYCUfz/1t2i54TfVza++s51TLp2PpnnnnGhO+1a9eaxxUd012RW2WN6dYZ+HUm8pI313dfH5/u7P+6nJ2u/X0qM8wDADyP7uUAgArTbq3aonrTTTeZcdK6rJEGGw1M2nqqr+l4bR0bXRbdX1sqNTxroNLlwrTl/N1335XBgwcXm0RNw9bIkSPNxFzaHVkna9NuxiXHPnfu3NkEOV2eScO0rvt88cUXm268ugTT+PHjzVJgusa1tnrrUlM63ra88efVibaS6sRl2iqsy4PpZFsanOfMmWMmGdM1q3V5rvLoz+sa6boMly6bVvQCh54/fR9tSdWlu3QSL+0VoC3GusSXa230M6Wt7fp5OtmedinX7u068VhpY5h1bXCd/E0nxdNzrOdRvxc6YZ0ei36fqmpMty5Fp/MAuJaB0wtCronzdAy39pzQY9NbabSVW7/jp0svDuhFL/1dAADUHIRuAMAp0aCj3YO1a7B2k506darp3q2BQ1uONSSfLAgpba3UicymT59uWv60lVHD8RNPPFFsP51lXMO8tkxrF2MNmho8NHwWpT8/efJks9b3nXfeaVrCdQZpDd26frR2SdYZsMeMGWMm5brnnntMS2nJtaqrM+0CrRcntN41AGtI1fW5O3bsaOpRQ3JFxsl37drV/MysWbOKhW6lFyV0bLjOPv/pp5+aNbL1Aobur5+r56MyaL3ruuA64Zies1q1ask111wjo0ePLvbd0UnW9GKDa830or0i9HugF29++umnKjuP+j3UixUu+h3Tm+rdu7f14Qp63ocMGXLKs8wDADzLoeuGebgMAACgCmmL7ahRo8z444pMSAbPW79+vSQkJJiu9dqzAwBQcxC6AQDwMTqRnbZe6zABHQ+O6k/Hiut50x4KAICahdANAAAAAIAlzF4OAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAAX12nW2fq3LNnj1mTsiLrjwIAAAAAYJuuvp2RkSFxcXHi5+dXc0O3Bu74+HhPFwMAAAAAgBPs3LlTGjVqJDU2dGsLt+tAIiIiPF0cAAAAAAAkPT3dNBC7MmuNDd2uLuUauAndAAAAAIDqpLxh0EykBgAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWVPt1ul0uvPhK8Q+oMcUFTktcTAOZP28WtQfAa908ZJCk7t/r6WKgCm0+cFAaNIqhzn1IbIMYmT/7U08XA6g2akyKjTnvXgkMDvV0MQCr9iyfSA0D8GoauCdd0cTTxUAV6jl1lzQfmUCd+5Dtk9d6ughAtUL3cgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALAmw9caoWea/eLW5HzJ2vkTXC5WRQzpKm6b1JDfvuHy3drdMnZ8ox/Odni4mAAA1QvNHPzH3yc/eKBHnDpTanfpJYL0YcTj8ZM/74yRnR5Kni4hKNuuGN839PZ+Olbu73SzN6sZLRHBtSc/JkKUpK2XmxvniFP6WAnwRLd0oxt/PIY+P6CFtm9aTD7/cLGt/PSCDLmguN17ampoCAOA0OAIC5ejWNXI87RD15wNCA0PkrIgYWbRtmby7brYJ2kPaDZD+Z/fxdNEAeAgt3SimQ4sGEhcVLj9s2CNzl2yT4CB/6d3pLLmyd3P54MtfqC0AAE7Rke9nm/tajVpLYJ2G1J+XO5x9RMZ8MV6czsJW7QC/ABmeMFSa1mnk6aIB8BBaulFM09gIc38wNdvc5+blS3pWnoSFBEqd8GBqCwAA4CQKCvLdgdshDkmI62Aeb9xP4wXgq2jpRrkc1BEAAMCp/ZHtFyCjegyTTjHtZOGWb2X5jtXUIOCjCN0o5ve96eY+qm6Iudfu5bXDgiQr+5gcycyltgAAACowrvvh3iOlfcNWMjtxgcxO+pw6A3wYoRvFJG47JHsOZUq3ttFyTd8W0iwuUgL8/WTO8q3UFAAAp6FWfDsJrB8r/qGFQ7hCW3Y1M5lnrF9EfXohPz9/ebLfQ9I4Mk7W7U2S3en7pWd8N0nLzZCkA796ungAasKY7jvuuEMcDoeMHDnyhNdGjRplXtN9XCZNmiRNmzaVWrVqSY8ePWTVqlVnXmpUqtqhgeY+J/e45OTly9NTV8nm3/+QWy9vK13bRMuCZdvlo6/5TwIAgIrwCwk39wV5OeLMPya1O10sUQP/JIF1Y8z2OudfbZ7De4QHhZn7nOO5EhEcbgK36hLbXh7oeae5Xdf+Cg+XEkCNaumOj4+Xjz/+WF5++WUJCSnshpyTkyMzZsyQxo0bu/ebOXOmPPjggzJ58mQTuF955RXp37+//Prrr9KwIbN3Vgc9O8bK4D4tzeON2wqXMtmxP0Mem/yDh0sGAEDNE9bmPInsMcg8zk5JNPcHF7xubvBOPRp1kStb9zOPkw5skYNZh2XozHs9XSwANX328oSEBBO858yZ496mjzVwd+nSxb3tpZdekrvvvluGDx8u7dq1M+E7NDRUpk6dWjmlxxnr3jZGYuqHytJ1u+S1WeupUQAAzoB2HQ+oEyOZScvk0MI3qUsfoLOTR4dHmYnSpvz0gaeLA8CbxnSPGDFCpk2bJrfccot5rkFaw/WSJUvM87y8PFmzZo088sgj7p/x8/OTSy65RFasWFHm++bm5pqbS3p64cResGPizHVULQAAleTggknUpY95c9X7ni4CAG9dp/vWW2+VZcuWSUpKirktX77cbHM5dOiQ5OfnS3R0dLGf0+f79u0r830nTJggkZGR7pu2qAMAAAAA4FMt3VFRUTJw4ECZPn26OJ1O87hBgwZnXCBtGddx4EVbugne9jx9b09pHhcpwUEBkpaZKysS98rUz5Lk+n5ny83928iMr35hEjUAACrAr1aYRA0aLcExzcUvNEIKstIkI3GppC75SMI79pWGg0ZLxs+LGd/tZcICQ+VPPW6XZnXjJSK4tqTnZMjSlJUyc+N8ubBpD7NW95LkFfLGqvc8XVQANXHJMO1iPnr0aPcs5UVpAPf395f9+/cX267PY2IKZ+8sTXBwsLmhaiTvTpfv1u4WEaeZUG1Q7+ay60Am1Q8AwCnyCw6VwPqNJH3dN5J/NF3q9BwidXtdK/mZqWYmc3in0MBaclZEjCzatkzSczNlcNv+MqTdADmSky7ZxzjvAM4wdF9++eVm7LYuE6azkhcVFBQkXbt2lUWLFsngwYPNtoKCAvPcFdThee98lijhIYESFhIoPTvGSXx0bRGn0/16bP0weWpkTzk7vq5s3ZUqz723WtKz8jxaZgAAqqPj6Ydl15T7RZwF5rnDP1AaXDZCgqKbSc7OzWabf1iERF8/VkIat5djqftk/9yX5Hhq2cPuUP0dzj4iY74Yb3p+qgC/ABmeMFSa1mkkmw9uNdt0GbGHe4+U9lGtZF/mQXl5xTuyP/Ogh0sOoNqP6Vbakr1582bZtGmTeVySdhN/++235d133zX73XvvvZKVlWUmXEP1MeWRfvLOo5eaNbkXr9kpX69Mcb/Wo0OMrEzcJ7/vTZOOLaNkYK9mHi0rAADVlobt/wVuEYeEtkwwj7KTN7h3CWnWSXJ3b5HsHZskOLaF1O11nYcKi8pS4CxwB26HOMxs5mrj/l/c+3SMaSe/HU6WTQd/k+b1Gsu17QZwAgAfckYt3SoiIqLM12644QY5ePCgjBs3zkye1rlzZ/nyyy9PmFwNnvXM9J+kbu1guaZvS7mw81ny48a97tcWr9kl85dtl9xj+dKuWX2JbRDm0bICAFDt+QdIw0H3SWjzzpK26nPJ2rRMwjteZF7KTv5ZjvwwV0KadZSwVt0lsF7ZQ+5Qs2gLt47f7hTTThZu+dYsIdan6XnmtQ37Nsm8zV/JOdFtpNtZHSUmPMrTxQVQnUO3Tpx2MvPmzSv2XLuS0528ekvaftj9eOzt3aVf98ayddcR81wnV1P5BYVX7v39HB4qJQAANWNct+k+3qSDpC6dKanfzyr2en5W4VKozvz8//3AiT0FUfOEBoYUdh9v2EpmJy6Q2UmfF3tdx3qr/ILC8+7HeQd8yhm3dKPmSmjdUPokNJLNyYdFHA4Z1Luw63jynjRPFw0AgBrHEVhL4m5/WoIaNpaj29ZK3uHdEtaul+Rn8f+qNwsOCJYn+z0kjSPjZN3eJNmdvl96xneTtNwMTxcNQDVB6PZhOiFak9jacl6HWPH3d8jhtGyZvWiLWSJs6CWtPF08AABqFP/Q2iZwq9AWCeamslMSJWPDEg+XDrZEBIWZwK26xLY3N5V0YItZKgwAHE7XzA/VlK7THRkZKf1HzZDA4FBPFwewas/yibLmx2+pZQBea0CvbjLpiiaeLgaqUM+py+XCZ66hzn3I9slrZfXilZ4uBlBlWTUtLe2kc52d0ezlAAAAAACgbIRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsCpIbY9+Ob4h9QY4oLnJa4mAbUHACvVjc6VkYtTPF0MVCFavkFy/bJa6lzHxLbIMbTRQCqFYfT6XRKNZaeni6RkZGSlpYmERERni4OAAAAAABS0axK93IAAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlAbbeGMCpGzR4qOzZd4iqg084emCbNI2N8nQxUMXqRsfKjDnzqXfAiw26/mrZe2ifp4uBKhTbIEbmz/6UOi8DoRuoRjRwx/W639PFAKrEtln3yKQrmlDbPmbUwhRPFwGAZRq4m49MoJ59yPbJaz1dhGqN7uUAAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFgSYOuNAaC6mv/i1eZ+yNj5El0vVEYO6ShtmtaT3Lzj8t3a3TJ1fqIcz3d6upjwEs0f/cTcJz97o0ScO1Bqd+ongfVixOHwkz3vj5OcHUmeLiIA4DTMuuFNc3/Pp2Pl7m43S7O68RIRXFvSczJkacpKmblxvjiFvydASzcAH+bv55DHR/SQtk3ryYdfbpa1vx6QQRc0lxsvbe3posFLOQIC5ejWNXI87ZCniwIAqCShgSFyVkSMLNq2TN5dN9sE7SHtBkj/s/tQxzBo6Qbgszq0aCBxUeHyw4Y9MnfJNgkO8pfenc6SK3s3lw++/MXTxYMXOvL9bHNfq1FrCazT0NPFAQBUgsPZR2TMF+PF6Sxs1Q7wC5DhCUOlaZ1G1C8MxnQD8FlNYyPM/cHUbHOfm5cv6Vl5EhYSKHXCgz1cOgAAUBMUFOS7A7dDHJIQ18E83rifC/goREs3ABThoDYAAMBp0BbuUT2GSaeYdrJwy7eyfMdq6hEGoRuAz/p9b7q5j6obYu61e3ntsCDJyj4mRzJzPVw6AABQk8Z1P9x7pLRv2EpmJy6Q2Umfe7pIqKndy++44w5xOBwycuTIE14bNWqUeU33UUuXLpVBgwZJXFyc2T5v3rzKKzUAVILEbYdkz6FM6dY2Wq7p20JGXddJAvz95PPlydQvrKgV305qd+4n/qGFQxtCW3Y1zwEANZefn7882e8hE7jX7U2S3en7pWd8N2nfkIlZcZot3fHx8fLxxx/Lyy+/LCEhha1DOTk5MmPGDGncuLF7v6ysLOnUqZOMGDFChgwZcqofAwBW1A4NNPc5ucclJy9fnp66Su655hy59fK25vmCZdvlo69/pfZRKfxCws19QV6OOPOPSe1OF0vtThe5X69zfuHydRnrF1HjAFCDhAeFmfuc47kSERwujSPjzPMuse3NTSUd2CJJB/ibAqcRuhMSEmTbtm0yZ84cueWWW8w2fayBu1mzZu79BgwYYG4AUF307Bgrg/u0NI83bitcsmnH/gx5bPIPHi4ZvFFYm/Mksscg8zg7JdHcH1zwurkBAGquHo26yJWt+7mD9cGswzJ05r2eLha8bfZybb2eNm2a+/nUqVNl+PDhlVkuAKh03dvGSEz9UFm6bpe8Nms9NQyrtOt4QJ0YyUxaJocWvkltA4CX0NnJo8OjzERpU376wNPFgbdOpHbrrbfKI488IikpKeb58uXLTZfzJUuWnHGBcnNzzc0lPb1woiMAOFMTZ66jElFlDi6YRG0DgBd6c9X7ni4CfCF0R0VFycCBA2X69OlmTTp93KBBg0op0IQJE2T8+PGV8l4AAAAAANTIJcO0i/no0aPN40mTKu9qvragP/jgg8VaunXyNgA4U0/f21Oax0VKcFCApGXmyorEvTL1syS5vt/ZcnP/NjLjq1+YRA2Vxq9WmEQNGi3BMc3FLzRCCrLSJCNxqaQu+UjCO/aVhoNGS8bPixnjDQA1TFhgqPypx+3SrG68RATXlvScDFmaslJmbpwvFzbtYdbqXpK8Qt5Y9Z6ni4qaHrovv/xyycvLM8uB9e/fv9IKFBwcbG4AUNmSd6fLd2t3i4jTTKg2qHdz2XUgk4qGFX7BoRJYv5Gkr/tG8o+mS52eQ6Rur2slPzPVzGYOAKiZQgNryVkRMbJo2zJJz82UwW37y5B2A+RITrpkH+Pfd1Ri6Pb395fNmze7H5eUmZkpW7dudT9PTk6W9evXS7169YotLQYAVeWdzxIlPCRQwkICpWfHOImPri3idLpfj60fJk+N7Clnx9eVrbtS5bn3Vkt6Vh4nCKflePph2TXlfhFngXnu8A+UBpeNkKDoZpKz83//f4ZFSPT1YyWkcXs5lrpP9s99SY6n7qPGAaAaO5x9RMZ8Md4Ms1UBfgEyPGGoNK3TSDYfLMw/uozYw71HSvuoVrIv86C8vOId2Z950MMlR42avdwlIiLC3EqzevVq6dKli7kp7TKuj8eNG3cmHwkAZ2TKI/3knUcvla5tomXxmp3y9crCCSFVjw4xsjJxn/y+N006toySgb3+/zKIwCnTsP2/wC3ikNCWCeZRdvIG9y4hzTpJ7u4tkr1jkwTHtpC6va6jogGgmitwFrgDt0McZjZztXH/L+59Osa0k98OJ8umg79J83qN5dp2LKXsy06ppVsnTjuZefPmuR/37dvX/WUEgOrimek/Sd3awXJN35ZyYeez5MeNe92vLV6zS+Yv2y65x/KlXbP6EtsgzKNlhZfwD5CGg+6T0OadJW3V55K1aZmEd7zIvJSd/LMc+WGuhDTrKGGtuktgvRhPlxYAUEHawq3jtzvFtJOFW741S4j1aXqeeW3Dvk0yb/NXck50G+l2VkeJCY+iXn3YaXcvB4CaKGn7Yffjsbd3l37dG8vWXUfMc51cTeUXFLZO+vs5PFRKeNO4btN9vEkHSV06U1K/n1Xs9fyswmUxnfn5//uBE4drAQCqn9DAkMLu4w1byezEBTI76fNir+tYb5VfUPjvux//vvs0QjcAn5DQuqH0SWgkm5MPizgcMqh3Ydfx5D1pni4avJQjsJbE3f60BDVsLEe3rZW8w7slrF0vyc/iOwcANVlwQLA82e8haRwZJ+v2Jsnu9P3SM76bpOVmeLpoqKYI3QB8gk6I1iS2tpzXIVb8/R1yOC1bZi/aYpYIG3pJK08XD17IP7S2CdwqtEWCuanslETJ2LDEw6UDAJyuiKAwE7hVl9j25qaSDmwxS4UBJTmc1Xzgta7THRkZKWlpaWVO2gZ4i67nXSxxve73dDGAKrFt1j2yYGRvatvHjFqYIl8sX+3pYgCwqNtFPaT5yMILjfAN2yevldWLV4qvSa9gVj2j2csBAAAAAEDZCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlgTYemMApy4upoHsWT6RqoNPcAbWklELUzxdDFSxutGx1Dng5WIbxMj2yWs9XQxU8TlH2RxOp9Mp1Vh6erpERkZKWlqaREREeLo4AAAAAABIRbMq3csBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwJIAqeZcy4jrGmgAAAAAAFQHrozqyqw1NnQfPnzY3MfHx3u6KAAAAAAAFJORkSGRkZFSY0N3vXr1zP2OHTtOeiDwritGepFl586dEhER4enioApwzn0P59w3cd59D+fc93DOfY8vn3On02kCd1xc3En3q/ah28+vcNi5Bm5fO4m+Ts8359y3cM59D+fcN3HefQ/n3Pdwzn2Pr57zyAo0DDORGgAAAAAAlhC6AQAAAADw1dAdHBwsTzzxhLmHb+Cc+x7Oue/hnPsmzrvv4Zz7Hs657+Gcl8/hLG9+cwAAAAAA4J0t3QAAAAAA1FSEbgAAAAAALCF0AwAAAABgCaEbAAAf8Pjjj8s999zjft63b1954IEHpCb629/+Jvfdd5+niwEAQIUQugEAKIPD4Tjp7R//+EeNqLt9+/bJxIkT5dFHHxVv8NBDD8m7774r27dv93RRAAAoF6EbAIAy7N2713175ZVXJCIiotg2DX81wTvvvCM9e/aUJk2aeLookpeXd8bv0aBBA+nfv7+8+eablVImAABsInQDAFCGmJgY9y0yMtK0bhfd9vHHH0vbtm2lVq1a0qZNG3njjTfcP/v777+b/WfNmiUXXHCBhISESPfu3WXLli3y008/Sbdu3SQ8PFwGDBggBw8edP/cHXfcIYMHD5bx48dLVFSUCfojR44sFlb/85//yDnnnGPes379+nLJJZdIVlZWmedRyzlo0KATthcUFMhf//pXqVevnjmeki33R44ckbvuustdjosvvlh+/vnnE8palHZZ167rLvp49OjRZrsrLKvExERz7FoH0dHRctttt8mhQ4cqfIx6PHpcAABUd4RuAABOw4cffijjxo2Tp59+WjZv3izPPPOMGTet3Z6LeuKJJ+Sxxx6TtWvXSkBAgNx8880m6Gp37++//162bt1q3qeoRYsWmfdcsmSJfPTRRzJnzhwTwpW2sN90000yYsQI9z5DhgwRp9NZajn/+OMP2bRpkwn5JWlZw8LCZOXKlfL888/Lk08+Kd9884379euvv14OHDggX3zxhaxZs0YSEhKkX79+5j1PhX5OUFCQLF++XCZPnmzCvAb4Ll26yOrVq+XLL7+U/fv3y9ChQyt8jOeee67s2rXLXNwAAKA6C/B0AQAAqIk0TL/44osmDKpmzZqZcDtlyhQZNmyYez/tgu5q3b3//vtNmNRQ3atXL7PtzjvvlOnTpxd7bw2oU6dOldDQUGnfvr0Jww8//LD885//NIH0+PHj5nNd3cW1RbgsO3bsMGE1Li7uhNc6duxojkOdffbZ8vrrr5uyXXrppbJs2TJZtWqVCd3BwcFmnxdeeEHmzZtnWqGLTspWHn1vDfUuTz31lAnceqHCRY83Pj7e9ATIzMws9xhdx5OSkiJNmzatcFkAAKhqhG4AAE6RdnPetm2bCcx33323e7sGRe2GXjLYumg36pIBUrdpsC2qU6dOJnC7nH/++SaI7ty507ymrc36HhrmL7vsMrnuuuukbt26pZY1Ozvb3GsX+JKKlk3Fxsa6y6LdyPUztWt3yffTYz8VXbt2LfZc33vx4sWma3lJ+t56TOUdo3Y7V0ePHj2lsgAAUNUI3QAAnCINo+rtt9+WHj16FHvN39+/2PPAwED3Yx3jXdo2HVtdUfr+2gX8hx9+kK+//lpee+01Myu5dhHX1vaSdBy1Sk1NNWOzyypbybLoMWoI167dJdWpU8fc+/n5ndCt/dixYyfsr13Yi9L31jHZzz333An76mdW5BhdXdxLHhMAANUNY7oBADhF2jqt3Zt1yaqWLVsWu5UWfE+VtgS7WqjVjz/+aFqFtfu1Kxxr93Qd571u3TrTHX3u3LmlvleLFi3MJGja9f1U6PhtXWpMx6GXPEZXkNfAq93di1q/fn2F3jspKcl0Cy/53q6AXt4x6kRsetFAu98DAFCdEboBADgNGgYnTJggr776qhmHvHHjRpk2bZq89NJLZ1yfOlO5dl3XoLxw4UIz7lpnANeWZW3t1bHQOgGZjtfWSdZ09nOdRb00+jM687eO0T4V+jParV1nJ9fWZp2wTFuetcVZP1vpZGj6+L333pPffvvNlFPDcHlGjRplWqp1fLvO5K5dyr/66isZPny45OfnV+gYdRI616zwAABUZ4RuAABOgy6lpetfa9DWscd9+vQxE6JVRku3jmfWyccuvPBCueGGG+Sqq65yL+elrdZLly6VK664Qlq1amVmRtcJ3XT5rZOVVZfXOpVu7NrSrIFfy6BhWD/rxhtvNBOXucam63hrnbFdZ2PX5dAyMjLk9ttvL/e9tZeAzmSuAVvHa2v96ZJi2m1dLxJU5Bj1eIqOpwcAoLpyOMtaYwQAAFQ5Xftal9TSWcIri/5Xr2PPx4wZY1qXazpdwuwvf/mLbNiwwXR/BwCgOqOlGwAAL6et1m+99ZaZXd1bZo/XHgYEbgBATcDlYQAAfEDnzp3NzRvo8mEAANQUdC8HAAAAAMASupcDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAMAZcDgc8o9//KPaf/aqVaskKChIUlJSrJfL1yxZssSci//85z/l7nvjjTfK0KFDq6RcAIDqgdANALBOA0l5t6LhccyYMZKQkCD16tWT0NBQadu2rXk9MzPTI2dr4cKFHgvWleXRRx+Vm266SZo0aXLCa3PnzpUBAwZIgwYNTDCPi4szwfDbb78VX/ff//5XLrroIlM3derUkXPPPVfef//9036/sWPHyieffCI///xzpZYTAFB9BXi6AAAA73eykKJhdtu2bdKjRw/3tp9++kkuuOACGT58uNSqVUvWrVsnzz77rAlAS5cuFT8/vyoP3ZMmTSo1eGdnZ0tAQPX+73T9+vWm7n744Ydi251Op4wYMUKmT58uXbp0kQcffFBiYmJk7969Joj369dPli9fLj179hRf9Nlnn8ngwYPl/PPPN+deLw7NmjVLbr/9djl06JC5OHSqtJ67desmL774orz33ntWyg0AqF6q918JAACvcOutt5a6/Z133jGB+7777jMtrS7Lli07Yd8WLVrIQw89ZLpJn3feeVJd6EWB6m7atGnSuHHjE+pNg58G7gceeEBeeuklEyqLtozrxZLqfkHBptdff11iY2NNi39wcLDZ9n//93/Spk0bU2+nE7qV9iJ44okn5I033pDw8PBKLjUAoLqhezkAwCOSkpLkz3/+s2n5+9e//lXu/k2bNjX3R44cKXffAwcOyJ133inR0dEmFHfq1EnefffdYvv8/vvvJmS+8MIL8vLLL5tu1yEhIdKnTx9JTEx073fHHXeYVm5VtDu8S8mu8a4W0S1btpiLDZGRkRIVFSWPP/64aVneuXOnXH311RIREWFalTX4FpWXlyfjxo2Trl27mp8NCwszrf6LFy+W0zVv3jy5+OKLi5VbW+gnTJhgAqTWQdHXXG677TbTnVppyNR99IKInjc9Ju1urSFUy6znRVuA69ata25//etfzfEWpZ+jreb169c3da3HWHIctF4g0M+ZOnVqse3PPPOM2a69DqpKenq6ORZX4FZ6EUK7mmv5SyooKJCnn35aGjVqZL532lNg69atJ+x36aWXSlZWlnzzzTfWjwEA4Hm+e/kaAOAxR48eNa19/v7+8vHHHxcLNS7Hjx83QU4DnYbgxx57TGrXru0OgWXRMNm3b18TdkaPHi3NmjWT2bNnm/Cs73f//fcX21+7+GZkZMioUaMkJydHJk6caALqxo0bTWjXULlnzx4TkE5lLO8NN9xgxqJrt/jPP/9cnnrqKTNGfcqUKeb9n3vuOfnwww9N63337t3lwgsvdAc97QGg46/vvvtuU7Z///vf0r9/f9PK37lzZzkVu3fvlh07dpgx8kVpeP7jjz9MK7eeh4rSXgl6sWD8+PHy448/yltvvWXCt3Zd19Z0DccajPVCSocOHUwQd9G6veqqq+SWW24x51XP/fXXXy8LFiyQgQMHmn10SMGcOXNMV3cNp/Hx8eZc6OfphZQrrrjipOXTcf96HssTGBhoLmqcjH6P9DzpBZNhw4aZ0D9jxgxZvXq16WZekp5rHfqg5zQtLU2ef/55c6wrV64stl+7du1MaNeu+9dcc025ZQUA1HBOAACq2IgRI7QJ1Pnuu++Wuc+KFSvMPq5b69atnYsXLy73vV955RWz/wcffODelpeX5zz//POd4eHhzvT0dLMtOTnZ7BcSEuLctWuXe9+VK1ea7WPGjHFvGzVqlNlWGt3+xBNPuJ/rY912zz33uLcdP37c2ahRI6fD4XA+++yz7u2pqanm84cNG1Zs39zc3GKfoftFR0ebejvZZ5fmv//9r9lv/vz5xbZPnDjRbJ87d66zIqZNm2b279+/v7OgoMC9XetVj2vkyJEnHG+fPn2KvcfRo0eLPdfz0qFDB+fFF19cbPvevXud9erVc1566aWmLrp06eJs3LixMy0trdxyal0W/d6UdStZttJkZmY6hw4dao7P9XOhoaHOefPmFdtPv5f6Wtu2bYudO1cdb9y48YT3btWqlXPAgAHllgEAUPPR0g0AqFLaUqhdh7XrctFW0JK0NVBbl7Ubrrai6kRgFZm9XFtZtSVWW4qLtmpql2jd9t1338mVV17pfk0nyjrrrLPcz7UlXSd10/fRcc6n66677nI/1pZknTxr165dprXWRVuIW7duLdu3by+2r6vlWbsra+u83uvPr1279pTLcfjwYXOv3aSL0hZ1pb0HToWWv2hXdK2rFStWFDsu1/GuWbOm2M8W7ZKdmpoq+fn5puv8Rx99VGw/PX/apV/Pl76uE8Hpd0G75JdHu7WXNYdAUSXrozTaA6NVq1Zy3XXXyZAhQ0x5tWVf31/LU3KMvLbS6+zvLlp2pedXW/1Lfr5OxgYA8H6EbgBAlfntt99k5MiRJsjoJFInowHrkksuMY91DLSGdb3X4KljtMui61CfffbZJ8xwrl29Xa8XpfuWpOUrrfvwqdCu1kVpV2Yd56vjgUtudwVjFx1/rmO9f/nlFzl27Jh7u3aVP10lx1e7Aqx2Xz/T41LaDbzkdg3WRWk3cu1mryE6NzfXvb208eS6nvUHH3xguubfc889Znx0RejFGr1VBh2eoF3o9Tvn+j7psIj27dubYQolu42XrBtXsC9ZD67zUdpxAwC8DxOpAQCqhIYsHefsGst7qrM2a0uj0p+tCUobJ13W2OmigViDpo4/19nadSz3l19+aVpVdRy4tnifKp20rLTgpxOoKR0vfSrKOobSthc9ru+//96M59YLD3rBRXsS6HHdfPPNJ1wQUHohQsdOq02bNlX42HUs9b59+8q96Xj2k9Hvqda/jjUvegFHe03oTPtaNt2nvDooWQ8uej5KXoABAHgnQjcAoEro5FK63rZOLqUzlp9OaNfgpaHqZHQWcm1RLxnStNXY9XpRum9JOvO4a7Z0VZUtkjqbd/Pmzc1kYtoFXydQ0xb/ikwOVhpXuE5OTi62vXfv3qYlVrt2a7dp2z755BMTuL/66iuzNrgGV1dPhtLoxHbaCq8zrOukb6+88kqFPkdboHWZr/Juros4ZdHQr5P5lVY32vtAv1+nW2/6vjqLvav3BQDAuxG6AQDWzZ0716x5rC2dOrb6ZHQMc9Eu1S46o7fSscIno7Nba0vmzJkzi4Wc1157zbSu65JgJZfT0hm+XXSGcO02XHTdcF22y1U221ytpUVbR7U8Om76dOh4de367Wo1dgkNDZWxY8fK5s2bzX1prbHa6q71UVnHpRcvigZVXbZN67+0Cw96/nQ28L/97W+mq7nOXq8XQyoypltb0Mu7lVyqraSGDRuaMff63S3aoq3zCsyfP99czCht2bCK0JZ7vYiiy6cBALwfY7oBAFbt3bvXTLKloUvH5WqQK412pz7//PNlyZIlJpjr5FU63loDj3ZN1pZfDdzlTZKl4391WS7toq0TeWmLtYY4XZ5JW0tLThzWsmVL0+p77733mtZ03Ue7ZGt4c9H1pJWWS1ue9Vg0CNqgk7zpsepSUtq1WVuoJ0+ebMYpV2QiudLoWHgNjyXHET/88MNmvXQNoLoOuNa5TmKmFy00DGvg1knsKoMei05Md/nll5su5bqWuk6WpvW/YcMG9366Xc/FRRddZMZUK71go+XTc6qt3iXH69sY063nWHtnaNjXCdN00j+9YKBdznVCvLK+xxWhoV8veuiSaAAA70foBgBY9euvv7rHE5dcI7soXQdZQ/c555xjAtenn35qArsGRQ3k48aNMyGx6OzQpdHWRw3u2kKqE5LpLN06Q/i0adNMaCtJw5SGOA3bGvh09nINedoF2UW7Iuv61DqeXMOWlslW6NYyaujVCwfaFVsDpH6mrjWux3U6tDu3HpNeeNALDC563LpOuYZynZX7hRdeMPUVFRVl1g3XoQB6TiqDjknXwKqt17o2uE4Kp2tga2t30dDtuvih58t1gUAvgmj5tJxaxqIXRGx69NFHTTl1fXFdJ1zL1bFjR3MR59prrz3t99Vzqd+pU505HgBQMzl03TBPFwIAgKqmYU8D1b/+9S/TounttJdBXFycvP/++54uik/TmdsTEhLMjOidO3f2dHEAAFWAMd0AAPiAZ555xoyTLrlkGqqWtvRrN34CNwD4DrqXAwDgA3r06HHCEleoejVlyTsAQOWhpRsAAAAAAEsY0w0AAAAAgCW0dAMAAAAAYAmhGwAAAAAAX51IraCgQPbs2WPWsnSt1wkAAAAAgCfp6tsZGRlmSU4/P7+aG7o1cMfHx3u6GAAAAAAAnGDnzp3SqFEjqbGhW1u4XQcSERHh6eIAAAAAACDp6emmgdiVWWts6HZ1KdfATegGAAAAAFQn5Q2DZiI1AAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCk2q/T7XLhxVeKf0CNKS5wWuJiGsj8ebN8svYGXX+17D20z9PFQBU6tGuftG0YRZ37mLrRsTJjznxPFwMAgCpTY1JszHn3SmBwqKeLAVi1Z/lEn61hDdzNRyZ4uhioQrv+PlcmXdGEOvcxoxameLoIAABUKbqXAwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgSYCtN0bNMv/Fq839kLHzJbpeqIwc0lHaNK0nuXnH5bu1u2Xq/EQ5nu/0dDGBGm/WDW+a+3s+HSt3d7tZmtWNl4jg2pKekyFLU1bKzI3zxSn8rnmT5o9+Yu6Tn71RIs4dKLU79ZPAejHicPjJnvfHSc6OJE8XEQAAWERLN4rx93PI4yN6SNum9eTDLzfL2l8PyKALmsuNl7ampoBKFBoYImdFxMiibcvk3XWzTdAe0m6A9D+7D/XsxRwBgXJ06xo5nnbI00UBAABVhJZuFNOhRQOJiwqXHzbskblLtklwkL/07nSWXNm7uXzw5S/UFlBJDmcfkTFfjBens7BVO8AvQIYnDJWmdRpRx17syPezzX2tRq0lsE5DTxcHAABUAVq6UUzT2AhzfzA129zn5uVLelaehIUESp3wYGoLqCQFBfnuwO0QhyTEdTCPN+7n4hYAAIA3oaUb5XJQR4C9f4T9AmRUj2HSKaadLNzyrSzfsZraBgAA8CKEbhTz+950cx9VN8Tca/fy2mFBkpV9TI5k5lJbQCWP636490hp37CVzE5cILOTPqd+AQAAvAyhG8Ukbjskew5lSre20XJN3xbSLC5SAvz9ZM7yrdQUUIn8/PzlyX4PSePIOFm3N0l2p++XnvHdJC03Q5IO/Epde6la8e0ksH6s+IcWDuUJbdnVzGSesX6Rp4sGAACqy5juO+64QxwOh4wcOfKE10aNGmVe031cJk2aJE2bNpVatWpJjx49ZNWqVWdealSq2qGB5j4n97jk5OXL01NXyebf/5BbL28rXdtEy4Jl2+WjrwkBwJkKDwor/F07nisRweEmcKsuse3lgZ53mtt17a+gor2IX0i4uS/IyxFn/jGp3eliiRr4JwmsG2O21zn/avMcAAB4r9Nq6Y6Pj5ePP/5YXn75ZQkJKeyGnJOTIzNmzJDGjRu795s5c6Y8+OCDMnnyZBO4X3nlFenfv7/8+uuv0rAhs7ZWBz07xsrgPi3N443bCpew2bE/Qx6b/IOHSwZ4lx6NusiVrfuZx0kHtsjBrMMydOa9ni4WLAprc55E9hhkHmenJJr7gwteNzcAAOA7Tmv28oSEBBO858yZ496mjzVwd+nSxb3tpZdekrvvvluGDx8u7dq1M+E7NDRUpk6dWjmlxxnr3jZGYuqHytJ1u+S1WeupUcASnZ08OjzKTJQ25acPqGcfoF3HA+rESGbSMjm08E1PFwcAANS0Md0jRoyQadOmyS233GKea5DWcL1kyRLzPC8vT9asWSOPPPKI+2f8/PzkkksukRUrVpT5vrm5uebmkp5eOLEX7Jg4cx1VC1SBN1e9Tz37mIMLJnm6CAAAoCav033rrbfKsmXLJCUlxdyWL19utrkcOnRI8vPzJTo6utjP6fN9+/aV+b4TJkyQyMhI901b1AEAAAAA8KmW7qioKBk4cKBMnz5dnE6nedygQYMzLpC2jOs48KIt3QRve56+t6c0j4uU4KAAScvMlRWJe2XqZ0lyfb+z5eb+bWTGV78wiRpQCcICQ+VPPW6XZnXjJSK4tqTnZMjSlJUyc+N8ubBpD7NW95LkFfLGqveoby/hVytMogaNluCY5uIXGiEFWWmSkbhUUpd8JOEd+0rDQaMl4+fFjPEGAMDLndGSYdrFfPTo0e5ZyovSAO7v7y/79+8vtl2fx8QUztpamuDgYHND1UjenS7frd0tIk4zodqg3s1l14FMqh+oZKGBteSsiBhZtG2ZpOdmyuC2/WVIuwFyJCddso/lUN9eyC84VALrN5L0dd9I/tF0qdNziNTtda3kZ6aa2cwBAIBvOKPQffnll5ux27pMmM5KXlRQUJB07dpVFi1aJIMHDzbbCgoKzHNXUIfnvfNZooSHBEpYSKD07Bgn8dG1RZxO9+ux9cPkqZE95ez4urJ1V6o8995qSc/K82iZgZrocPYRGfPFeNMzSAX4BcjwhKHStE4j2Xxwq9mmy4g93HuktI9qJfsyD8rLK96R/ZkHPVxynK7j6Ydl15T7RZwF5rnDP1AaXDZCgqKbSc7OzWabf1iERF8/VkIat5djqftk/9yX5Hhq2UOwAACAD43pVtqSvXnzZtm0aZN5XJJ2E3/77bfl3XffNfvde++9kpWVZSZcQ/Ux5ZF+8s6jl5o1uRev2Slfr0xxv9ajQ4ysTNwnv+9Nk44to2Rgr2YeLStQUxU4C9yB2yEOM5u52rj/F/c+HWPayW+Hk2XTwd+keb3Gcm27AR4rLyqBhu3/BW4966EtE8yj7OQN7l1CmnWS3N1bJHvHJgmObSF1e11H1QMA4GXOqKVbRURElPnaDTfcIAcPHpRx48aZydM6d+4sX3755QmTq8Gznpn+k9StHSzX9G0pF3Y+S37cuNf92uI1u2T+su2Seyxf2jWrL7ENwjxaVqCm0xZuHb/dKaadLNzyrVlCrE/T88xrG/Ztknmbv5JzottIt7M6Skx4lKeLi8rgHyANB90noc07S9qqzyVr0zIJ73iReSk7+Wc58sNcCWnWUcJadZfAemUPvwIAAD4SunXitJOZN29esefalZzu5NVb0vbD7sdjb+8u/bo3lq27jpjnOrmayi8obK3x93N4qJRAzRcaGFLYfbxhK5mduEBmJ31e7HUd663yC/LNvZ/fiT2IUPPGdZvu4006SOrSmZL6/axir+dnFS6L6cwvPOfCOQcAwOuccUs3aq6E1g2lT0Ij2Zx8WMThkEG9C7uOJ+9J83TRAK8THBAsT/Z7SBpHxsm6vUmyO32/9IzvJmm5GZ4uGixxBNaSuNuflqCGjeXotrWSd3i3hLXrJflZ/BsLAIAvIXT7MJ0QrUlsbTmvQ6z4+zvkcFq2zF60xSwRNvSSVp4uHuBVIoLCTOBWXWLbm5tKOrDFLBUG7+MfWtsEbhXaIsHcVHZKomRsWOLh0gEAgKricLpm9qmmdJ3uyMhI6T9qhgQGh3q6OIBVe5ZPlDU/fuuTtdztoh7SfGRhKIFvWPr3ufLDiF6eLgaq2KiFKfLF8tXUOwCgxnNl1bS0tJPOdXZGs5cDAAAAAICyEboBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALAmQGmLfj2+Kf0CNKS5wWuJiGvhszcU2iJHtk9d6uhioQrX8gmXUwhTq3MfUjY71dBEAAKhSDqfT6ZRqLD09XSIjIyUtLU0iIiI8XRwAAAAAAKSiWZXu5QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsCbL0xztzNQwZJ6v69VKUP+X3vQQlt2MLTxQCqxIHDyRLdqCG17WNiG8TI/NmferoYAABUGUJ3NaaBe9IVTTxdDFShKyfvlLhe91Pn8Ak75t4rzUcmeLoYqGLbJ6+lzgEAPoXu5QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAIRuAAAAAABqFlq6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwJsvTFQUc0f/cTcJz97o0ScO1Bqd+ongfVixOHwkz3vj5OcHUlUJirV/BevNvdDxs6X6HqhMnJIR2nTtJ7k5h2X79bulqnzE+V4vpNaR6WYdcOb5v6eT8fK3d1ulmZ14yUiuLak52TI0pSVMnPjfHEK3zcAALwVLd2oVhwBgXJ06xo5nnbI00WBD/D3c8jjI3pI26b15MMvN8vaXw/IoAuay42XtvZ00eCFQgND5KyIGFm0bZm8u262CdpD2g2Q/mf38XTRAACARbR0o1o58v1sc1+rUWsJrNPQ08WBl+vQooHERYXLDxv2yNwl2yQ4yF96dzpLruzdXD748hdPFw9e5nD2ERnzxXhxOgtbtQP8AmR4wlBpWqeRp4sGAAAsoqUbgM9qGhth7g+mZpv73Lx8Sc/Kk7CQQKkTHuzh0sHbFBTkuwO3QxySENfBPN64nws8AAB4M1q6AaAIB7UB2//x+gXIqB7DpFNMO1m45VtZvmM1dQ4AgBcjdAPwWb/vTTf3UXVDzL12L68dFiRZ2cfkSGauh0sHbx3X/XDvkdK+YSuZnbhAZid97ukiAQCA6tS9/I477hCHwyEjR4484bVRo0aZ13QftXTpUhk0aJDExcWZ7fPmzau8UsNr1YpvJ7U79xP/0MJuv6Etu5rngA2J2w7JnkOZ0q1ttFzTt4WMuq6TBPj7yefLk6lwVDo/P395st9DJnCv25sku9P3S8/4btK+IRP3AQDgzU65pTs+Pl4+/vhjefnllyUkpLB1KCcnR2bMmCGNGzd275eVlSWdOnWSESNGyJAhQyq31PAafiHh5r4gL0ec+cekdqeLpXani9yv1zm/cGmnjPWLPFZGeJfaoYHmPif3uOTk5cvTU1fJPdecI7de3tY8X7Bsu3z09a+eLia8RHhQmLnPOZ4rEcHh0jgyzjzvEtve3FTSgS2SdIDvHAAA3uqUQ3dCQoJs27ZN5syZI7fccovZpo81cDdr1sy934ABA8wNKEtYm/Mksscg8zg7JdHcH1zwurkBNvTsGCuD+7Q0jzduK1yWbsf+DHls8g9UOCpdj0Zd5MrW/dzB+mDWYRk6815qGgAAH3Nas5dr6/W0adPcz6dOnSrDhw+vzHLBB2jX8YA6MZKZtEwOLXzT08WBD+jeNkZi6ofK0nW75LVZ6z1dHHg5nZ08OjzKTJQ25acPPF0cAABQkyZSu/XWW+WRRx6RlJQU83z58uWmy/mSJUvOuEC5ubnm5pKeXjjREbzPwQWTPF0E+JiJM9d5ugjwIW+uet/TRQAAADU1dEdFRcnAgQNl+vTpZs1RfdygQYNKKdCECRNk/PjxlfJeAAAAAADUyCXDtIv56NGjzeNJkyqvxVJb0B988MFiLd06eRu8j1+tMIkaNFqCY5qLX2iEFGSlSUbiUkld8pGEd+wrDQeNloyfFzPGG5Xm6Xt7SvO4SAkOCpC0zFxZkbhXpn6WJNf3O1tu7t9GZnz1C5OoodKEBYbKn3rcLs3qxktEcG1Jz8mQpSkrZebG+XJh0x5mre4lySvkjVXvUesAAHix0w7dl19+ueTl5ZnlwPr3719pBQoODjY3eD+/4FAJrN9I0td9I/lH06VOzyFSt9e1kp+ZamYzBypb8u50+W7tbhFxmgnVBvVuLrsOZFLRsCI0sJacFREji7Ytk/TcTBnctr8MaTdAjuSkS/Yx/o0DAMBXnHbo9vf3l82bN7sfl5SZmSlbt251P09OTpb169dLvXr1ii0tBt91PP2w7Jpyv4izwDx3+AdKg8tGSFB0M8nZ+b/vVliERF8/VkIat5djqftk/9yX5HjqPg+XHDXVO58lSnhIoISFBErPjnESH11bxOl0vx5bP0yeGtlTzo6vK1t3pcpz762W9Kw8j5YZNdfh7CMy5ovxZhiWCvALkOEJQ6VpnUay+WDh/4+6jNjDvUdK+6hWsi/zoLy84h3Zn3nQwyUHAAAen73cJSIiwtxKs3r1aunSpYu5Ke0yro/HjRt3Jh8Jb6Jh+3+BW8QhoS0TzKPs5A3uXUKadZLc3Vske8cmCY5tIXV7XeehwsJbTHmkn7zz6KXStU20LF6zU75eWTghpOrRIUZWJu6T3/emSceWUTKw1/9fBhE4VQXOAnfgdojDzGauNu7/xb1Px5h28tvhZNl08DdpXq+xXNuOpTYBAPDplm6dOO1k5s2b537ct29f9x8bwEn5B0jDQfdJaPPOkrbqc8natEzCO15kXspO/lmO/DBXQpp1lLBW3SWwXgyViTPyzPSfpG7tYLmmb0u5sPNZ8uPGve7XFq/ZJfOXbZfcY/nSrll9iW0QRm3jjGkLt47f7hTTThZu+dYsIdan6XnmtQ37Nsm8zV/JOdFtpNtZHSUmPIoaBwDAy5x293KgssZ1m+7jTTpI6tKZkvr9rGKv52cVLhnnzM//3w+cOJQBOBVJ2w+7H4+9vbv0695Ytu46Yp7r5Grme1dQ2APD389B5eKMhAaGFHYfb9hKZicukNlJnxd7Xcd6F37nCv+N8+PfOAAAvA6hGx7jCKwlcbc/LUENG8vRbWsl7/BuCWvXS/Kz0jgrqHQJrRtKn4RGsjn5sIjDIYN6F3YdT97D9w12BAcEy5P9HpLGkXGybm+S7E7fLz3ju0labgZVDgCADyF0w2P8Q2ubwK1CWySYm8pOSZSMDUs4M6hUOiFak9jacl6HWPH3d8jhtGyZvWiLWSJs6CWtqG1UuoigMBO4VZfY9uamkg5sMUuFAQAA3+BwVvOB17pOd2RkpKSlpZU5aZu3GtCrm0y6oomni4EqdOXkZdJi6FvUOXzCj3PvlYsmXO3pYqCKbZ+8VlYvXkm9AwBqvIpm1TOavRwAAAAAAJSN0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgCaEbAAAAAABLCN0AAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAAAAAMASQjcAAAAAAJYQugEAAAAAsITQDQAAAACAJYRuAAAAAAAsIXQDAAAAAGAJoRsAAAAAAEsI3QAAAAAAWELoBgAAAADAEkI3AAAAAACWELoBAAAAALCE0A0AAAAAgCWEbgAAAAAALCF0AwAAAABgSYCtN8aZqxsdK6MWplCVPsQZWEv2LJ/o6WIAVaKWf7Bsn7yW2vYxsQ1iPF0EAACqFKG7GpsxZ76niwAAAAAAOAN0LwcAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAAX12n2+l0mvv09HRPFwUAAAAAgGIZ1ZVZa2zoPnz4sLmPj4/3dFEAAAAAACgmIyNDIiMjpcaG7nr16pn7HTt2nPRA4F1XjPQiy86dOyUiIsLTxUEV4Jz7Hs65b+K8+x7Oue/hnPseXz7nTqfTBO64uLiT7lftQ7efX+Gwcw3cvnYSfZ2eb865b+Gc+x7OuW/ivPsezrnv4Zz7Hl8955EVaBhmIjUAAAAAACwhdAMAAAAA4KuhOzg4WJ544glzD9/AOfc9nHPfwzn3TZx338M59z2cc9/DOS+fw1ne/OYAAAAAAMA7W7oBAAAAAKipCN0AAAAAAFhC6AYAAAAAwBdD96RJk6Rp06ZSq1Yt6dGjh6xatcrTRYIlEyZMkO7du0vt2rWlYcOGMnjwYPn111+pbx/y7LPPisPhkAceeMDTRYFlu3fvlltvvVXq168vISEhcs4558jq1aupdy+Vn58vjz/+uDRr1syc7xYtWsg///lPYUoZ77J06VIZNGiQxMXFmX/L582bV+x1Pd/jxo2T2NhY8z245JJL5LfffvNYeWH3nB87dkzGjh1r/n0PCwsz+9x+++2yZ88eqt6Lf8+LGjlypNnnlVdeqdIyVlfVNnTPnDlTHnzwQTNz+dq1a6VTp07Sv39/OXDggKeLBgu+++47GTVqlPz444/yzTffmH+sL7vsMsnKyqK+fcBPP/0kU6ZMkY4dO3q6KLAsNTVVevXqJYGBgfLFF1/Ipk2b5MUXX5S6detS917queeekzfffFNef/112bx5s3n+/PPPy2uvvebpoqES6f/X+reaNpiURs/5q6++KpMnT5aVK1eaIKZ/1+Xk5HAevPCcHz161Pz9rhfc9H7OnDmmMeWqq67ySFlRNb/nLnPnzjV/02s4RzWfvVxbtrXlU/+TVgUFBRIfHy/33Xef/O1vf/N08WDZwYMHTYu3hvELL7yQ+vZimZmZkpCQIG+88YY89dRT0rlzZ66KejH993v58uXy/fffe7ooqCJXXnmlREdHy7///W/3tmuvvda0dn7wwQecBy+krVv6R7f2WlP6p6b+8f2Xv/xFHnroIbMtLS3NfC+mT58uN954o4dLjMo+52VdYD/33HMlJSVFGjduTKV76TnX3mya47766isZOHCg6cH4AL0Yq2dLd15enqxZs8Z0PXLx8/Mzz1esWOHRsqFq6H/Gql69elS5l9MeDvqPctHfd3ivzz77TLp16ybXX3+9ubDWpUsXefvttz1dLFjUs2dPWbRokWzZssU8//nnn2XZsmUyYMAA6t1HJCcny759+4r9Ox8ZGWn+MOfvOt/6206DWp06dTxdFFiijaS33XabPPzww9K+fXvquYgAqYYOHTpkxoDpFdCi9Pkvv/zisXKh6n5h9YqYdkHt0KED1e7FPv74Y9PtTK9+wzds377ddDXW4UN///vfzbn/85//LEFBQTJs2DBPFw+Wejekp6dLmzZtxN/f3/z//vTTT8stt9xCffsIDdyqtL/rXK/Bu+kwAh3jfdNNN0lERISniwNLdPhQQECA+X8dNSB0w7dpy2diYqJpCYH32rlzp9x///1mDL9OlgjfuaimLd3PPPOMea4t3fr7ruM8Cd3eadasWfLhhx/KjBkzTMvH+vXrzYVV7W7MOQe8n87TM3ToUDPMQC+6wjtpL+WJEyeaxhTt0YAa0L28QYMG5mr4/v37i23X5zExMR4rF+wbPXq0LFiwQBYvXiyNGjWiyr38H2edGFHHc+tVUb3pGH6daEcfa2sYvI/OXNyuXbti29q2bSs7duzwWJlgl3Yz1NZuHberMxlr18MxY8aYVSvgG1x/u/F3ne8Gbh3HrRfZaeX2XjpXi/5dp+P1XX/X6XnXuRyaNm0qvq5ahm7tZti1a1czBqxo64g+P//88z1aNtihVz81cOuEDN9++61ZWgberV+/frJx40bT6uW6aQuodjnVx3rhDd5Hh42UXA5Qx/o2adLEY2WCXTqLsc7LUpT+fuv/6/AN+n+6Bu+if9fpkAOdxZy/67yXK3Dr0nD//e9/zTKR8F56QXXDhg3F/q7THk164fWrr74SX1dtu5freD/tdqZ/hOtMh7rGm05TP3z4cE8XDZa6lGvXw08//dSs1e0a46UTregMt/A+ep5LjtnXJWT0P2XG8nsvbeHUibW0e7n+MbZq1Sp56623zA3eSdd01THc2vqh3cvXrVsnL730kowYMcLTRUMlr0SxdevWYpOn6R/dOiGqnnsdUqArVJx99tkmhOtSUvoH+clmu0bNPefaq+m6664zXY21B6P2XnP9baevawMbvO/3vOSFFV0eVC+4tW7d2gOlrWac1dhrr73mbNy4sTMoKMh57rnnOn/88UdPFwmW6FextNu0adOocx/Sp08f5/333+/pYsCy+fPnOzt06OAMDg52tmnTxvnWW29R514sPT3d/F7r/+e1atVyNm/e3Pnoo486c3NzPV00VKLFixeX+v/4sGHDzOsFBQXOxx9/3BkdHW1+9/v16+f89ddfOQdees6Tk5PL/NtOfw7e+XteUpMmTZwvv/xylZezOqq263QDAAAAAFDTVcsx3QAAAAAAeANCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAABYQugGAMAHPP7443LPPfe4n/ft21ceeOABqYn+9re/yX333efpYgAAUCGEbgAAyuBwOE56+8c//lEj6m7fvn0yceJEefTRR8UbPPTQQ/Luu+/K9u3bPV0UAADKRegGAKAMe/fudd9eeeUViYiIKLZNw19N8M4770jPnj2lSZMmni6K5OXlnfF7NGjQQPr37y9vvvlmpZQJAACbCN0AAJQhJibGfYuMjDSt20W3ffzxx9K2bVupVauWtGnTRt544w33z/7+++9m/1mzZskFF1wgISEh0r17d9myZYv89NNP0q1bNwkPD5cBAwbIwYMH3T93xx13yODBg2X8+PESFRVlgv7IkSOLhdX//Oc/cs4555j3rF+/vlxyySWSlZVV5nnUcg4aNOiE7QUFBfLXv/5V6tWrZ46nZMv9kSNH5K677nKX4+KLL5aff/75hLIWpV3Wteu6iz4ePXq02e4KyyoxMdEcu9ZBdHS03HbbbXLo0KEKH6Mejx4XAADVHaEbAIDT8OGHH8q4cePk6aefls2bN8szzzxjxk1rt+einnjiCXnsscdk7dq1EhAQIDfffLMJutrd+/vvv5etW7ea9ylq0aJF5j2XLFkiH330kcyZM8eEcKUt7DfddJOMGDHCvc+QIUPE6XSWWs4//vhDNm3aZEJ+SVrWsLAwWblypTz//PPy5JNPyjfffON+/frrr5cDBw7IF198IWvWrJGEhATp16+fec9ToZ8TFBQky5cvl8mTJ5swrwG+S5cusnr1avnyyy9l//79MnTo0Aof47nnniu7du0yFzcAAKjOAjxdAAAAaiIN0y+++KIJg6pZs2Ym3E6ZMkWGDRvm3k+7oLtad++//34TJjVU9+rVy2y78847Zfr06cXeWwPq1KlTJTQ0VNq3b2/C8MMPPyz//Oc/TSA9fvy4+VxXd3FtES7Ljh07TFiNi4s74bWOHTua41Bnn322vP7666Zsl156qSxbtkxWrVplQndwcLDZ54UXXpB58+aZVuiik7KVR99bQ73LU089ZQK3Xqhw0eONj483PQEyMzPLPUbX8aSkpEjTpk0rXBYAAKoaoRsAgFOk3Zy3bdtmAvPdd9/t3q5BUbuhlwy2LtqNumSA1G0abIvq1KmTCdwu559/vgmiO3fuNK9pa7O+h4b5yy67TK677jqpW7duqWXNzs4299oFvqSiZVOxsbHusmg3cv1M7dpd8v302E9F165diz3X9168eLHpWl6SvrceU3nHqN3O1dGjR0+pLAAAVDVCNwAAp0jDqHr77belR48exV7z9/cv9jwwMND9WMd4l7ZNx1ZXlL6/dgH/4Ycf5Ouvv5bXXnvNzEquXcS1tb0kHUetUlNTzdjssspWsix6jBrCtWt3SXXq1DH3fn5+J3RrP3bs2An7axf2ovS9dUz2c889d8K++pkVOUZXF/eSxwQAQHXDmG4AAE6Rtk5r92Zdsqply5bFbqUF31OlLcGuFmr1448/mlZh7X7tCsfaPV3Hea9bt850R587d26p79WiRQszCZp2fT8VOn5blxrTceglj9EV5DXwanf3otavX1+h905KSjLdwku+tyugl3eMOhGbXjTQ7vcAAFRnhG4AAE6DhsEJEybIq6++asYhb9y4UaZNmyYvvfTSGdenzlSuXdc1KC9cuNCMu9YZwLVlWVt7dSy0TkCm47V1kjWd/VxnUS+N/ozO/K1jtE+F/ox2a9fZybW1WScs05ZnbXHWz1Y6GZo+fu+99+S3334z5dQwXJ5Ro0aZlmod364zuWuX8q+++kqGDx8u+fn5FTpGnYTONSs8AADVGaEbAIDToEtp6frXGrR17HGfPn3MhGiV0dKt45l18rELL7xQbrjhBrnqqqvcy3lpq/XSpUvliiuukFatWpmZ0XVCN11+62Rl1eW1TqUbu7Y0a+DXMmgY1s+68cYbzcRlrrHpOt5aZ2zX2dh1ObSMjAy5/fbby31v7SWgM5lrwNbx2lp/uqSYdlvXiwQVOUY9nqLj6QEAqK4czrLWGAEAAFVO177WJbV0lvDKov/V69jzMWPGmNblmk6XMPvLX/4iGzZsMN3fAQCozmjpBgDAy2mr9VtvvWVmV/eW2eO1hwGBGwBQE3B5GAAAH9C5c2dz8wa6fBgAADUF3csBAAAAALCE7uUAAAAAAFhC6AYAAAAAwBJCNwAAAAAAlhC6AQAAAACwhNANAAAAAIAlhG4AAAAAACwhdAMAAAAAYAmhGwAAAAAASwjdAAAAAACIHf8Pf4t6MstQw/gAAAAASUVORK5CYII=", "text/plain": [ "
" ] @@ -579,52 +549,28 @@ "source": [ "COLORS = {\"J0\": \"#4C72B0\", \"J1\": \"#DD8452\", \"J2\": \"#55A868\", \"J3\": \"#C44E52\"}\n", "\n", - "\n", - "\n", "def draw_gantt(ax, schedule, title, machine_names, xmax):\n", - "\n", " for mi, m in enumerate(machine_names):\n", - "\n", " for j in schedule:\n", - "\n", " for (mach, s, d) in schedule[j]:\n", - "\n", " if mach == m:\n", - "\n", " ax.barh(mi, d, left=s, height=0.6,\n", - "\n", " color=COLORS.get(j, \"gray\"), edgecolor=\"black\", linewidth=0.5)\n", - "\n", " ax.text(s + d / 2, mi, f\"{j}\\n{d}h\", ha=\"center\", va=\"center\",\n", - "\n", " fontsize=8, color=\"white\", fontweight=\"bold\")\n", - "\n", " ax.set_yticks(range(len(machine_names)))\n", - "\n", " ax.set_yticklabels(machine_names)\n", - "\n", " ax.set_xlabel(\"Temps (heures)\")\n", - "\n", " ax.set_title(title)\n", - "\n", " ax.set_xlim(0, xmax + 1)\n", - "\n", " ax.invert_yaxis()\n", "\n", - "\n", - "\n", "xmax = max(greedy_cmax, opt_cmax)\n", - "\n", "fig, axes = plt.subplots(2, 1, figsize=(10, 6), sharex=True)\n", - "\n", "draw_gantt(axes[0], greedy_schedule, f\"Glouton FIFO (Cmax = {greedy_cmax}h)\", MACHINES, xmax)\n", - "\n", "draw_gantt(axes[1], opt_schedule, f\"Z3 optimal (Cmax = {opt_cmax}h)\", MACHINES, xmax)\n", - "\n", "fig.tight_layout()\n", - "\n", "plt.show()\n", - "\n", "print(\"Diagramme de Gantt : glouton (haut) vs optimal (bas).\")" ] }, @@ -632,7 +578,13 @@ "cell_type": "markdown", "id": "c370df18", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003361, + "end_time": "2026-09-26T19:41:59.589200", + "exception": false, + "start_time": "2026-09-26T19:41:59.585839", + "status": "completed" + }, "tags": [] }, "source": [ @@ -649,7 +601,13 @@ "cell_type": "markdown", "id": "c12", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.006171, + "end_time": "2026-09-26T19:41:59.598647", + "exception": false, + "start_time": "2026-09-26T19:41:59.592476", + "status": "completed" + }, "tags": [] }, "source": [ @@ -664,18 +622,20 @@ "cell_type": "markdown", "id": "c13", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.00473, + "end_time": "2026-09-26T19:41:59.607419", + "exception": false, + "start_time": "2026-09-26T19:41:59.602689", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 1 -- Ajout d'un quatrieme job\n", "\n", - "\n", - "\n", "**Objectif** : ajouter un job `J3 = [(\"M1\", 1), (\"M0\", 3)]` (1h sur M1 puis 3h sur M0) et re-resoudre. Observez comment le makespan optimal augmente (ou non) et comment Z3 re-entrelace les opérations.\n", "\n", - "\n", - "\n", "**Indices** : copiez le dict `jobs` dans `jobs_4` avec l'entree J3 supplementaire ; appelez `solve_jobshop(jobs_4, MACHINES)`." ] }, @@ -685,12 +645,18 @@ "id": "c14", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.314462Z", - "iopub.status.busy": "2026-07-17T20:08:24.314197Z", - "iopub.status.idle": "2026-07-17T20:08:24.317402Z", - "shell.execute_reply": "2026-07-17T20:08:24.316843Z" + "iopub.execute_input": "2026-09-26T19:41:59.620005Z", + "iopub.status.busy": "2026-09-26T19:41:59.619570Z", + "iopub.status.idle": "2026-09-26T19:41:59.626897Z", + "shell.execute_reply": "2026-09-26T19:41:59.625122Z" + }, + "papermill": { + "duration": 0.015871, + "end_time": "2026-09-26T19:41:59.627994", + "exception": false, + "start_time": "2026-09-26T19:41:59.612123", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -704,25 +670,15 @@ ], "source": [ "# Exercice 1 : ajoutez un quatrieme job J3 et re-resolvez.\n", - "\n", "# Etape 1 : definissez jobs_4 = dict(jobs) puis jobs_4[\"J3\"] = [(\"M1\", 1), (\"M0\", 3)].\n", - "\n", "# Etape 2 : resolvez via solve_jobshop(jobs_4, MACHINES).\n", - "\n", "# Etape 3 : comparez le nouveau Cmax a l'optimum 3-jobs (opt_cmax).\n", "\n", - "\n", - "\n", "def resoudre_4_jobs():\n", - "\n", " \"\"\"Retourne (schedule, cmax) pour l'instance 3 jobs + J3.\"\"\"\n", - "\n", " # TODO etudiant : construire jobs_4 et appeler solve_jobshop\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 1 a completer : ajouter un 4eme job et mesurer le nouveau Cmax optimal.\")" ] }, @@ -730,18 +686,20 @@ "cell_type": "markdown", "id": "c15", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.005117, + "end_time": "2026-09-26T19:41:59.636580", + "exception": false, + "start_time": "2026-09-26T19:41:59.631463", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 2 -- Contrainte d'urgence (deadline)\n", "\n", - "\n", - "\n", "**Objectif** : imposer que le job `J0` termine avant $t = 7$ (deadline). Ajoutez cette contrainte au modèle et verifyez que le makespan optimal augmente (la deadline force un ordonnancement moins efficace).\n", "\n", - "\n", - "\n", "**Indices** : la fin de J0 est `start[\"J0\"][-1] + duree_derniere_op` ; ajoutez `opt.add(... <= 7)` avant `opt.minimize`. Modifiez `solve_jobshop` ou créez une variante." ] }, @@ -751,12 +709,18 @@ "id": "c16", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.319307Z", - "iopub.status.busy": "2026-07-17T20:08:24.319148Z", - "iopub.status.idle": "2026-07-17T20:08:24.322397Z", - "shell.execute_reply": "2026-07-17T20:08:24.321875Z" + "iopub.execute_input": "2026-09-26T19:41:59.647617Z", + "iopub.status.busy": "2026-09-26T19:41:59.647322Z", + "iopub.status.idle": "2026-09-26T19:41:59.652445Z", + "shell.execute_reply": "2026-09-26T19:41:59.650962Z" + }, + "papermill": { + "duration": 0.014053, + "end_time": "2026-09-26T19:41:59.654305", + "exception": false, + "start_time": "2026-09-26T19:41:59.640252", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -770,25 +734,15 @@ ], "source": [ "# Exercice 2 : ajoutez une deadline (J0 doit terminer avant t=7).\n", - "\n", "# Indice : opt.add(start[\"J0\"][-1] + jobs[\"J0\"][-1][1] <= 7) avant opt.minimize.\n", - "\n", "# Etape 1 : copiez solve_jobshop en solve_jobshop_deadline(jobs, machines, deadline_j0=7).\n", - "\n", "# Etape 2 : resolvez et comparez le Cmax a opt_cmax (sans deadline).\n", "\n", - "\n", - "\n", "def solve_jobshop_deadline(jobs, machine_names, deadline_j0=7):\n", - "\n", " \"\"\"Job-shop avec une deadline sur J0.\"\"\"\n", - "\n", " # TODO etudiant : modeliser + ajouter la deadline + minimiser\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 2 a completer : mesurer le surcout d'une deadline sur J0.\")" ] }, @@ -796,18 +750,20 @@ "cell_type": "markdown", "id": "c17", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.004922, + "end_time": "2026-09-26T19:41:59.663244", + "exception": false, + "start_time": "2026-09-26T19:41:59.658322", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 3 -- Extension a 3 machines\n", "\n", - "\n", - "\n", "**Objectif** : etendre l'instance a 3 machines (M0, M1, M2) avec des jobs a 3 opérations chacun, et verifyez que `solve_jobshop` generalize sans modification de code (le modèle est paramètre par les données).\n", "\n", - "\n", - "\n", "**Indices** : definissez `MACHINES_3 = [\"M0\", \"M1\", \"M2\"]` et des `jobs_3` ou chaque job a 3 opérations sur des machines distinctes ; la fonction `solve_jobshop` gere déjà le cas general." ] }, @@ -817,12 +773,18 @@ "id": "c18", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:24.323894Z", - "iopub.status.busy": "2026-07-17T20:08:24.323753Z", - "iopub.status.idle": "2026-07-17T20:08:24.326358Z", - "shell.execute_reply": "2026-07-17T20:08:24.325880Z" + "iopub.execute_input": "2026-09-26T19:41:59.677465Z", + "iopub.status.busy": "2026-09-26T19:41:59.676783Z", + "iopub.status.idle": "2026-09-26T19:41:59.682916Z", + "shell.execute_reply": "2026-09-26T19:41:59.681556Z" + }, + "papermill": { + "duration": 0.015625, + "end_time": "2026-09-26T19:41:59.684541", + "exception": false, + "start_time": "2026-09-26T19:41:59.668916", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -836,27 +798,16 @@ ], "source": [ "# Exercice 3 : etendez l'instance a 3 machines, 3 operations par job.\n", - "\n", "# Indice : MACHINES_3 = [\"M0\", \"M1\", \"M2\"], jobs_3 = {j: [(m1,d1),(m2,d2),(m3,d3)], ...}.\n", - "\n", "# Etape 1 : definissez jobs_3 (3 jobs, chacun 3 operations sur des machines distinctes).\n", - "\n", "# Etape 2 : resolvez via solve_jobshop(jobs_3, MACHINES_3).\n", - "\n", "# Question : le temps de resolution grimpe-t-il avec 3 machines ? Mesurez-le.\n", "\n", - "\n", - "\n", "def resoudre_3_machines():\n", - "\n", " \"\"\"Retourne (schedule, cmax) pour une instance 3 machines.\"\"\"\n", - "\n", " # TODO etudiant : definir jobs_3 + MACHINES_3 et appeler solve_jobshop\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 3 a completer : generaliser a 3 machines et observer le temps de resolution.\")" ] }, @@ -864,35 +815,45 @@ "cell_type": "markdown", "id": "c19", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.006428, + "end_time": "2026-09-26T19:41:59.697666", + "exception": false, + "start_time": "2026-09-26T19:41:59.691238", + "status": "completed" + }, "tags": [] }, "source": [ "## Conclusion\n", "\n", - "\n", - "\n", "Le job-shop scheduling illustre le gain du **declaratif** sur une classe de problemes ou l'heuristique gloutonne est structurellement sous-optimale :\n", "\n", - "\n", - "\n", "- La **contrainte disjonctive** `Or(s_a + d_a <= s_b, s_b + d_b <= s_a)` (exclusion mutuelle sur une machine) est difficile a coder en imperatif sans enumerer tous les ordres possibles ; Z3 la traite nativement.\n", - "\n", "- `Optimize.minimize` trouve le makespan **optimal** (prouvablement minimal), la ou FIFO se contente d'un ordonnancement realisable mais myope.\n", - "\n", "- Le modèle est **paramètre par les données** : ajouter un job, une machine ou une deadline se fait en modifiant l'instance ou en ajoutant une contrainte, sans re-ecrire l'algorithme de resolution.\n", "\n", - "\n", - "\n", "**Limites** : sur de très grandes instances (dizaines de jobs x dizaines de machines), le solveur peut devenir lent — c'est le prix de l'optimalite garantie. Dans ce cas, on combine souvent Z3 avec des heuristiques (fournir un ordonnancement glouton comme borne superieure aide le solveur a pruner).\n", "\n", - "\n", - "\n", "Suite logique : retour a la [serie Z3-Python](README.md), ou explorez la version C# [Z3.Linq](../Z3-Linq2Z3/README.md) qui aborde le même problème via une couche declarative LINQ." ] } ], "metadata": { + "cost": { + "api_provider": "none", + "api_usd_est": 0.0, + "cpu_min": 6, + "external_account": null, + "free_alternative": null, + "gpu_required": false, + "metadata_written": null, + "network": false, + "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU).", + "reduced_pedagogical": null, + "reproducibility": "HIGH", + "validator": "manual" + }, "kernelspec": { "display_name": "Python 3", "language": "python", @@ -908,23 +869,21 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.13.7" + "version": "3.13.13" }, - "cost": { - "api_usd_est": 0.0, - "api_provider": "none", - "cpu_min": 6, - "gpu_required": false, - "network": false, - "external_account": null, - "free_alternative": null, - "reduced_pedagogical": null, - "reproducibility": "HIGH", - "metadata_written": null, - "validator": "manual", - "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU)." + "papermill": { + "default_parameters": {}, + "duration": 4.394621, + "end_time": "2026-09-26T19:42:00.046437", + "environment_variables": {}, + "exception": null, + "input_path": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb", + "output_path": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-08-Ordonnancement-Python.ipynb", + "parameters": {}, + "start_time": "2026-09-26T19:41:55.651816", + "version": "2.6.0" } }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb index fdd932cf78..c1001164f3 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb @@ -4,30 +4,26 @@ "cell_type": "markdown", "id": "c0", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.00425, + "end_time": "2026-09-26T19:42:11.446042", + "exception": false, + "start_time": "2026-09-26T19:42:11.441792", + "status": "completed" + }, "tags": [] }, "source": [ "# Z3-Python-09 : L'enigme d'Einstein (Zebra puzzle)\n", "\n", - "\n", - "\n", "[← Serie Z3-Python](README.md) | [Z3-Python-08 (ordonnancement) →](Z3-08-Ordonnancement-Python.ipynb)\n", "\n", - "\n", - "\n", "## Le problème\n", "\n", - "\n", - "\n", "L'**enigme d'Einstein** (ou *Zebra puzzle*) est un classique de logique : 5 maisons alignees, chacune habitee par une personne de nationalite, couleur, boisson, cigarette et animal différents. On dispose de **15 indices** (le Britannique vit dans la rouge, le Danois boit du the, la verte est a gauche de la blanche, etc.) et la question est : **qui possede le poisson ?**\n", "\n", - "\n", - "\n", "A la main, la resolution procede par deductions progressives sur un tableau - c'est long et trompeur. L'espace de recherche brut est enorme : chaque attribut est une permutation des 5 maisons, soit $(5!)^5 = 24\\,883\\,200\\,000$ combinaisons. Une **enumeration exhaustive** (brute force) testant les 15 indices pour chaque combinaison prend plusieurs minutes.\n", "\n", - "\n", - "\n", "C'est typiquement la ou un solveur SMT comme Z3 **fait la différence** : on decrit les 25 variables (position de chaque valeur), le domaine, les 5 contraintes de permutation (`Distinct`) et les 15 indices, et `Solver` trouve l'unique solution en **quelques millisecondes**. Ce notebook porte en Python l'exemple C# [18_Einsteins_Riddle](../Z3-Linq2Z3/18_Einsteins_Riddle.ipynb) de la serie sœur Z3.Linq." ] }, @@ -37,12 +33,18 @@ "id": "c1", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.702196Z", - "iopub.status.busy": "2026-07-17T20:08:35.702060Z", - "iopub.status.idle": "2026-07-17T20:08:35.724900Z", - "shell.execute_reply": "2026-07-17T20:08:35.724328Z" + "iopub.execute_input": "2026-09-26T19:42:11.454637Z", + "iopub.status.busy": "2026-09-26T19:42:11.454353Z", + "iopub.status.idle": "2026-09-26T19:42:11.486036Z", + "shell.execute_reply": "2026-09-26T19:42:11.485228Z" + }, + "papermill": { + "duration": 0.037272, + "end_time": "2026-09-26T19:42:11.486991", + "exception": false, + "start_time": "2026-09-26T19:42:11.449719", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -56,13 +58,9 @@ ], "source": [ "# Imports : z3 (solveur SMT) + time (benchmark).\n", - "\n", "import time\n", - "\n", "import z3\n", "\n", - "\n", - "\n", "print(\"z3 version :\", z3.get_version_string())" ] }, @@ -70,38 +68,30 @@ "cell_type": "markdown", "id": "c2", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003452, + "end_time": "2026-09-26T19:42:11.493832", + "exception": false, + "start_time": "2026-09-26T19:42:11.490380", + "status": "completed" + }, "tags": [] }, "source": [ "## Modelisation : l'encodage par position\n", "\n", - "\n", - "\n", "L'astuce centrale consiste a **inverser le point de vue**. Au lieu de demander « quelle couleur a la maison *k* ? », on définit pour chaque valeur d'attribut une variable entiere egale a la **position** (numéro de maison 0..4) ou elle se trouve :\n", "\n", - "\n", - "\n", "- `Brit`, `Swede`, `Dane`, `Norwegian`, `German` : position de chaque nationalite\n", - "\n", "- `Red`, `Green`, `White`, `Yellow`, `Blue` : position de chaque couleur\n", - "\n", "- `Tea`, `Coffee`, `Milk`, `Water`, `Beer` : position de chaque boisson\n", - "\n", "- `PallMall`, `Dunhill`, `Blend`, `BlueMaster`, `Prince` : position de chaque cigarette\n", - "\n", "- `Dog`, `Bird`, `Cat`, `Horse`, `Fish` : position de chaque animal\n", "\n", - "\n", - "\n", "Soit **25 variables entieres**. Les contraintes se traduisent alors très naturellement :\n", "\n", - "\n", - "\n", "1. **Domaine** : chaque variable $\\in \\{0,1,2,3,4\\}$.\n", - "\n", "2. **Permutation** : dans chaque groupe d'attributs, les 5 positions sont deux a deux distinctes (`Distinct`) - chaque valeur occupe une maison différente.\n", - "\n", "3. **Les 15 indices** : des egalites de position (`Brit == Red` : le Britannique et la rouge sont dans la même maison) ou des **adjacences** (`|Blend - Cat| == 1` : le fumeur de Blend est voisin du Chat)." ] }, @@ -111,12 +101,18 @@ "id": "c3", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.726659Z", - "iopub.status.busy": "2026-07-17T20:08:35.726514Z", - "iopub.status.idle": "2026-07-17T20:08:35.732200Z", - "shell.execute_reply": "2026-07-17T20:08:35.731643Z" + "iopub.execute_input": "2026-09-26T19:42:11.501887Z", + "iopub.status.busy": "2026-09-26T19:42:11.501590Z", + "iopub.status.idle": "2026-09-26T19:42:11.509307Z", + "shell.execute_reply": "2026-09-26T19:42:11.508425Z" + }, + "papermill": { + "duration": 0.012997, + "end_time": "2026-09-26T19:42:11.510081", + "exception": false, + "start_time": "2026-09-26T19:42:11.497084", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -130,85 +126,45 @@ ], "source": [ "def build_einstein_solver():\n", - "\n", " \"\"\"Construit le solveur Z3 de l'enigme d'Einstein (25 vars de position, 15 indices).\n", - "\n", " Retourne (solver, var_dict, group_labels) pour reuse dans les exercices.\"\"\"\n", - "\n", " s = z3.Solver()\n", - "\n", " # 25 variables de position (0..4) : une par valeur d'attribut.\n", - "\n", " groups = {\n", - "\n", " \"Nationalite\": [\"Brit\", \"Swede\", \"Dane\", \"Norwegian\", \"German\"],\n", - "\n", " \"Couleur\": [\"Red\", \"Green\", \"White\", \"Yellow\", \"Blue\"],\n", - "\n", " \"Boisson\": [\"Tea\", \"Coffee\", \"Milk\", \"Water\", \"Beer\"],\n", - "\n", " \"Cigarette\": [\"PallMall\", \"Dunhill\", \"Blend\", \"BlueMaster\", \"Prince\"],\n", - "\n", " \"Animal\": [\"Dog\", \"Bird\", \"Cat\", \"Horse\", \"Fish\"],\n", - "\n", " }\n", - "\n", " v = {n: z3.Int(n) for grp in groups.values() for n in grp}\n", "\n", - "\n", - "\n", " # (1) Domaine 0..4 pour les 25 variables\n", - "\n", " for var in v.values():\n", - "\n", " s.add(var >= 0, var <= 4)\n", "\n", - "\n", - "\n", " # (2) Permutation : les 5 valeurs d'un meme attribut occupent des maisons distinctes\n", - "\n", " for grp in groups.values():\n", - "\n", " s.add(z3.Distinct([v[n] for n in grp]))\n", "\n", - "\n", - "\n", " # (3) Les 15 indices\n", - "\n", " s.add(v[\"Brit\"] == v[\"Red\"]) # 1. le Britannique vit dans la rouge\n", - "\n", " s.add(v[\"Swede\"] == v[\"Dog\"]) # 2. le Suedois eleve des chiens\n", - "\n", " s.add(v[\"Dane\"] == v[\"Tea\"]) # 3. le Danois boit du the\n", - "\n", " s.add(v[\"Green\"] == v[\"White\"] - 1) # 4. la verte est juste a gauche de la blanche\n", - "\n", " s.add(v[\"Green\"] == v[\"Coffee\"]) # 5. la verte boit du cafe\n", - "\n", " s.add(v[\"PallMall\"] == v[\"Bird\"]) # 6. Pall Mall eleve des oiseaux\n", - "\n", " s.add(v[\"Yellow\"] == v[\"Dunhill\"]) # 7. la jaune fume du Dunhill\n", - "\n", " s.add(v[\"Milk\"] == 2) # 8. la maison du milieu boit du lait\n", - "\n", " s.add(v[\"Norwegian\"] == 0) # 9. le Norvegien dans la 1ere maison\n", - "\n", " s.add(z3.Or(v[\"Blend\"] - v[\"Cat\"] == 1, v[\"Cat\"] - v[\"Blend\"] == 1)) # 10. Blend voisin du Chat\n", - "\n", " s.add(z3.Or(v[\"Horse\"] - v[\"Dunhill\"] == 1, v[\"Dunhill\"] - v[\"Horse\"] == 1)) # 11. Cheval voisin du Dunhill\n", - "\n", " s.add(v[\"BlueMaster\"] == v[\"Beer\"]) # 12. BlueMaster boit de la biere\n", - "\n", " s.add(v[\"German\"] == v[\"Prince\"]) # 13. l'Allemand fume du Prince\n", - "\n", " s.add(z3.Or(v[\"Norwegian\"] - v[\"Blue\"] == 1, v[\"Blue\"] - v[\"Norwegian\"] == 1)) # 14. Norvegien voisin de la bleue\n", - "\n", " s.add(z3.Or(v[\"Blend\"] - v[\"Water\"] == 1, v[\"Water\"] - v[\"Blend\"] == 1)) # 15. Blend voisin de l'Eau\n", - "\n", " return s, v, groups\n", "\n", - "\n", - "\n", "print(\"Modele encode : 25 variables de position, 5 groupes Distinct, 15 indices.\")" ] }, @@ -216,7 +172,13 @@ "cell_type": "markdown", "id": "c4", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002397, + "end_time": "2026-09-26T19:42:11.515568", + "exception": false, + "start_time": "2026-09-26T19:42:11.513171", + "status": "completed" + }, "tags": [] }, "source": [ @@ -233,12 +195,18 @@ "id": "c5", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.733732Z", - "iopub.status.busy": "2026-07-17T20:08:35.733597Z", - "iopub.status.idle": "2026-07-17T20:08:35.773723Z", - "shell.execute_reply": "2026-07-17T20:08:35.773128Z" + "iopub.execute_input": "2026-09-26T19:42:11.522418Z", + "iopub.status.busy": "2026-09-26T19:42:11.522159Z", + "iopub.status.idle": "2026-09-26T19:42:11.559685Z", + "shell.execute_reply": "2026-09-26T19:42:11.558732Z" + }, + "papermill": { + "duration": 0.042821, + "end_time": "2026-09-26T19:42:11.560574", + "exception": false, + "start_time": "2026-09-26T19:42:11.517753", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -260,73 +228,39 @@ ], "source": [ "# Labels francais pour l'affichage (associes au nom de variable).\n", - "\n", "LABELS_FR = {\n", - "\n", " \"Nationalite\": [(\"Britannique\", \"Brit\"), (\"Suedois\", \"Swede\"), (\"Danois\", \"Dane\"), (\"Norvegien\", \"Norwegian\"), (\"Allemand\", \"German\")],\n", - "\n", " \"Couleur\": [(\"Rouge\", \"Red\"), (\"Verte\", \"Green\"), (\"Blanche\", \"White\"), (\"Jaune\", \"Yellow\"), (\"Bleue\", \"Blue\")],\n", - "\n", " \"Boisson\": [(\"The\", \"Tea\"), (\"Cafe\", \"Coffee\"), (\"Lait\", \"Milk\"), (\"Eau\", \"Water\"), (\"Biere\", \"Beer\")],\n", - "\n", " \"Cigarette\": [(\"Pall Mall\", \"PallMall\"), (\"Dunhill\", \"Dunhill\"), (\"Blend\", \"Blend\"), (\"BlueMaster\", \"BlueMaster\"), (\"Prince\", \"Prince\")],\n", - "\n", " \"Animal\": [(\"Chien\", \"Dog\"), (\"Oiseau\", \"Bird\"), (\"Chat\", \"Cat\"), (\"Cheval\", \"Horse\"), (\"Poisson\", \"Fish\")],\n", - "\n", "}\n", "\n", - "\n", - "\n", "def solve_and_display():\n", - "\n", " \"\"\"Resout l'enigme et affiche le tableau des 5 maisons.\"\"\"\n", - "\n", " s, v, _ = build_einstein_solver()\n", - "\n", " assert s.check() == z3.sat, \"UNSAT (inattendu pour cette enigme)\"\n", - "\n", " m = s.model()\n", - "\n", " pos = {n: m[v[n]].as_long() for n in v} # nom de variable -> position (0..4)\n", "\n", - "\n", - "\n", " def val_at(group, h):\n", - "\n", " \"\"\"Retourne le label francais de la valeur du groupe present a la maison h.\"\"\"\n", - "\n", " for fr, key in LABELS_FR[group]:\n", - "\n", " if pos[key] == h:\n", - "\n", " return fr\n", - "\n", " return \"?\"\n", "\n", - "\n", - "\n", " cols = [\"Maison\", \"Nationalite\", \"Couleur\", \"Boisson\", \"Cigarette\", \"Animal\"]\n", - "\n", " widths = [7, 13, 9, 9, 13, 9]\n", - "\n", " print(\" \".join(c.ljust(w) for c, w in zip(cols, widths)))\n", - "\n", " print(\" \" + \"-\" * (sum(widths) + 2 * (len(cols) - 1)))\n", - "\n", " for h in range(5):\n", - "\n", " row = [str(h + 1)] + [val_at(g, h) for g in [\"Nationalite\", \"Couleur\", \"Boisson\", \"Cigarette\", \"Animal\"]]\n", - "\n", " print(\" \".join(c.ljust(w) for c, w in zip(row, widths)))\n", - "\n", " print()\n", - "\n", " print(f\">>> Reponse : c'est le {val_at('Nationalite', pos['Fish'])} qui possede le Poisson (maison {pos['Fish'] + 1}).\")\n", - "\n", " return m, v\n", "\n", - "\n", - "\n", "solution_model, solution_vars = solve_and_display()" ] }, @@ -334,18 +268,20 @@ "cell_type": "markdown", "id": "c6", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002208, + "end_time": "2026-09-26T19:42:11.565211", + "exception": false, + "start_time": "2026-09-26T19:42:11.563003", + "status": "completed" + }, "tags": [] }, "source": [ "## Interpretation\n", "\n", - "\n", - "\n", "Z3 trouve l'unique solution en quelques millisecondes. La resolution humaine procederait par deductions progressives - on place le Norvegien en 1 (`Norwegian == 0`), le lait en 3 (`Milk == 2`), puis on propage les egalites et adjacences - mais c'est précisément ce travail de **propagation de contraintes** que le solveur automatise, sans erreur ni oubli.\n", "\n", - "\n", - "\n", "La reponse a la question « qui possede le poisson ? » tombe directement du modèle extrait. Notons qu'**aucun indice ne parle du poisson** : c'est par elimination (les 4 autres animaux sont localises par les indices) que sa position se deduit." ] }, @@ -353,7 +289,13 @@ "cell_type": "markdown", "id": "a96124b0", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002248, + "end_time": "2026-09-26T19:42:11.569779", + "exception": false, + "start_time": "2026-09-26T19:42:11.567531", + "status": "completed" + }, "tags": [] }, "source": [ @@ -373,7 +315,13 @@ "cell_type": "markdown", "id": "c7", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002207, + "end_time": "2026-09-26T19:42:11.574407", + "exception": false, + "start_time": "2026-09-26T19:42:11.572200", + "status": "completed" + }, "tags": [] }, "source": [ @@ -390,12 +338,18 @@ "id": "c8", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.775979Z", - "iopub.status.busy": "2026-07-17T20:08:35.775768Z", - "iopub.status.idle": "2026-07-17T20:08:35.808713Z", - "shell.execute_reply": "2026-07-17T20:08:35.807672Z" + "iopub.execute_input": "2026-09-26T19:42:11.580594Z", + "iopub.status.busy": "2026-09-26T19:42:11.580243Z", + "iopub.status.idle": "2026-09-26T19:42:11.615383Z", + "shell.execute_reply": "2026-09-26T19:42:11.614527Z" + }, + "papermill": { + "duration": 0.039966, + "end_time": "2026-09-26T19:42:11.616656", + "exception": false, + "start_time": "2026-09-26T19:42:11.576690", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -405,7 +359,7 @@ "text": [ "Espace de recherche brut : (5!)^5 = 24,883,200,000 combinaisons\n", "Brute force estime (~1e8/s) : 248.8 s (hors test des 15 indices)\n", - "Z3 solve temps : 11.8 ms\n", + "Z3 solve temps : 13.8 ms\n", "Solution unique (UNSAT si nie) : True\n", " -> Z3 resout en millisecondes un espace de ~25 milliards, et prouve l'unicite sans enumeration.\n" ] @@ -413,49 +367,27 @@ ], "source": [ "# (1) Espace de recherche brut\n", - "\n", "import math\n", - "\n", "space = math.factorial(5) ** 5 # (5!)^5 = 24_883_200_000\n", - "\n", "brute_seconds = space / 1e8 # a ~1e8 tests/s, sans compter le test des 15 indices\n", "\n", - "\n", - "\n", "# (2) Chronometre la resolution Z3\n", - "\n", "t0 = time.perf_counter()\n", - "\n", "s1, v1, _ = build_einstein_solver()\n", - "\n", "assert s1.check() == z3.sat\n", - "\n", "m1 = s1.model()\n", - "\n", "z3_ms = (time.perf_counter() - t0) * 1000\n", "\n", - "\n", - "\n", "# (3) Unicite : on nie le temoin trouve (au moins une variable differe) -> on attend unsat\n", - "\n", "s2, v2, _ = build_einstein_solver()\n", - "\n", "negation = z3.Or([v2[n] != m1[v1[n]].as_long() for n in v2]) # une solution differente existe-t-elle ?\n", - "\n", "s2.add(negation)\n", - "\n", "unique = (s2.check() == z3.unsat)\n", "\n", - "\n", - "\n", "print(f\"Espace de recherche brut : (5!)^5 = {space:,} combinaisons\")\n", - "\n", "print(f\"Brute force estime (~1e8/s) : {brute_seconds:.1f} s (hors test des 15 indices)\")\n", - "\n", "print(f\"Z3 solve temps : {z3_ms:.1f} ms\")\n", - "\n", "print(f\"Solution unique (UNSAT si nie) : {unique}\")\n", - "\n", "print(f\" -> Z3 resout en millisecondes un espace de ~{space/1e9:.0f} milliards, et prouve l'unicite sans enumeration.\")" ] }, @@ -463,18 +395,20 @@ "cell_type": "markdown", "id": "c9", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.004405, + "end_time": "2026-09-26T19:42:11.625656", + "exception": false, + "start_time": "2026-09-26T19:42:11.621251", + "status": "completed" + }, "tags": [] }, "source": [ "## Lecture du benchmark\n", "\n", - "\n", - "\n", "Sur cette enigme, l'ecart est **frappant** : Z3 resout les 25 variables entrelacees en quelques millisecondes, alors que la brute force doit affronter **~25 milliards** de combinaisons (soit plusieurs minutes même a cadence elevee, et bien plus avec le test des 15 indices a chaque candidat).\n", "\n", - "\n", - "\n", "La **propagation** fait tout le travail : `Norwegian == 0` et `Milk == 2` sont des ancres imposees par les indices 9 et 8, puis les egalites de position et les adjacences reduisent les domaines restants jusqu'a ce qu'il ne reste qu'une seule combinaison coherente. C'est exactement la mecanique qu'un humain deployerait a la main sur le tableau - mais le solveur la realise sans erreur et la **prouve complete** (unicite via `unsat` sur la negation)." ] }, @@ -482,7 +416,13 @@ "cell_type": "markdown", "id": "c10", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003857, + "end_time": "2026-09-26T19:42:11.633602", + "exception": false, + "start_time": "2026-09-26T19:42:11.629745", + "status": "completed" + }, "tags": [] }, "source": [ @@ -497,18 +437,20 @@ "cell_type": "markdown", "id": "c11", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.003771, + "end_time": "2026-09-26T19:42:11.641137", + "exception": false, + "start_time": "2026-09-26T19:42:11.637366", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 1 -- Un 16e indice : le Chat boit de l'Eau\n", "\n", - "\n", - "\n", "**Objectif** : ajouter l'indice `Cat == Water` (le Chat et l'Eau sont dans la même maison) et observer si l'enigme reste satisfaisable (`sat`) ou devient contradictoire (`unsat`).\n", "\n", - "\n", - "\n", "**Indices** : reprenez `build_einstein_solver()`, ajoutez `s.add(v[\"Cat\"] == v[\"Water\"])` avant `check()`. Que se passe-t-il ? (Pensez a comparer avec la solution trouvee plus haut : le Chat et l'Eau y sont-ils dans la même maison ?)" ] }, @@ -518,12 +460,18 @@ "id": "c12", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.811242Z", - "iopub.status.busy": "2026-07-17T20:08:35.811048Z", - "iopub.status.idle": "2026-07-17T20:08:35.814578Z", - "shell.execute_reply": "2026-07-17T20:08:35.813942Z" + "iopub.execute_input": "2026-09-26T19:42:11.648376Z", + "iopub.status.busy": "2026-09-26T19:42:11.648108Z", + "iopub.status.idle": "2026-09-26T19:42:11.651685Z", + "shell.execute_reply": "2026-09-26T19:42:11.651105Z" + }, + "papermill": { + "duration": 0.007817, + "end_time": "2026-09-26T19:42:11.652545", + "exception": false, + "start_time": "2026-09-26T19:42:11.644728", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -537,25 +485,15 @@ ], "source": [ "# Exercice 1 : ajoutez l'indice Cat == Water et testez la satisfiabilite.\n", - "\n", "# Etape 1 : reprenez build_einstein_solver() -> s, v, _.\n", - "\n", "# Etape 2 : s.add(v[\"Cat\"] == v[\"Water\"]).\n", - "\n", "# Etape 3 : s.check() -> sat ou unsat ?\n", "\n", - "\n", - "\n", "def tester_chat_eau():\n", - "\n", " \"\"\"Retourne 'sat' ou 'unsat' apres ajout de l'indice Cat == Water.\"\"\"\n", - "\n", " # TODO etudiant : construire le solveur, ajouter l'indice, retourner le verdict\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 1 a completer : ajoutez Cat == Water et testez la satisfiabilite.\")" ] }, @@ -563,18 +501,20 @@ "cell_type": "markdown", "id": "c13", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002534, + "end_time": "2026-09-26T19:42:11.657789", + "exception": false, + "start_time": "2026-09-26T19:42:11.655255", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 2 -- Enumerer toutes les solutions\n", "\n", - "\n", - "\n", "**Objectif** : enumerer **toutes** les solutions de l'enigme par **blocage iteratif** (on resout, on compte, on ajoute une contrainte interdisant le temoin trouve, on re-resout) jusqu'a `unsat`. Le compte attendu est 1 (solution unique), ce qui confirme le benchmark ci-dessus.\n", "\n", - "\n", - "\n", "**Indices** : boucle `while s.check() == z3.sat` ; a chaque tour, comptez++, puis `s.add(z3.Or([v[n] != m[v[n]].as_long() for n in v]))` pour interdire le temoin courant et forcer une solution différente au tour suivant." ] }, @@ -584,12 +524,18 @@ "id": "c14", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.817038Z", - "iopub.status.busy": "2026-07-17T20:08:35.816880Z", - "iopub.status.idle": "2026-07-17T20:08:35.819923Z", - "shell.execute_reply": "2026-07-17T20:08:35.819326Z" + "iopub.execute_input": "2026-09-26T19:42:11.664879Z", + "iopub.status.busy": "2026-09-26T19:42:11.664628Z", + "iopub.status.idle": "2026-09-26T19:42:11.668009Z", + "shell.execute_reply": "2026-09-26T19:42:11.667377Z" + }, + "papermill": { + "duration": 0.00891, + "end_time": "2026-09-26T19:42:11.669365", + "exception": false, + "start_time": "2026-09-26T19:42:11.660455", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -603,25 +549,15 @@ ], "source": [ "# Exercice 2 : enumerer toutes les solutions par blocage iteratif.\n", - "\n", "# Etape 1 : s, v, _ = build_einstein_solver().\n", - "\n", "# Etape 2 : while s.check() == z3.sat: compte += 1; m = s.model(); s.add(z3.Or([v[n] != m[v[n]].as_long() for n in v])).\n", - "\n", "# Etape 3 : afficher le compte (attendu : 1).\n", "\n", - "\n", - "\n", "def compter_solutions():\n", - "\n", " \"\"\"Retourne le nombre total de solutions de l'enigme (attendu : 1).\"\"\"\n", - "\n", " # TODO etudiant : boucle de blocage iteratif\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 2 a completer : enumerer toutes les solutions par blocage iteratif.\")" ] }, @@ -629,18 +565,20 @@ "cell_type": "markdown", "id": "c15", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.004779, + "end_time": "2026-09-26T19:42:11.678781", + "exception": false, + "start_time": "2026-09-26T19:42:11.674002", + "status": "completed" + }, "tags": [] }, "source": [ "### Exercice 3 -- Mini-Zebra a 4 maisons / 4 attributs\n", "\n", - "\n", - "\n", "**Objectif** : modeliser une **mini-enigme** a 4 maisons et 4 attributs (4 nationalites, 4 couleurs, 4 animaux) avec 8 indices de votre choix, et verifyez que `build_einstein_solver` se generalise (le modèle est paramètre par les données).\n", "\n", - "\n", - "\n", "**Indices** : definissez `groups_4` avec 4 valeurs par attribut, domaine `0..3`, 3 groupes `Distinct`, puis 8 indices (identites de position + adjacences) inventes. Inspirez-vous de la structure de `build_einstein_solver`." ] }, @@ -650,12 +588,18 @@ "id": "c16", "metadata": { "execution": { - "iopub.execute_input": "2026-07-17T20:08:35.821726Z", - "iopub.status.busy": "2026-07-17T20:08:35.821583Z", - "iopub.status.idle": "2026-07-17T20:08:35.824868Z", - "shell.execute_reply": "2026-07-17T20:08:35.824276Z" + "iopub.execute_input": "2026-09-26T19:42:11.689087Z", + "iopub.status.busy": "2026-09-26T19:42:11.688799Z", + "iopub.status.idle": "2026-09-26T19:42:11.692943Z", + "shell.execute_reply": "2026-09-26T19:42:11.692201Z" + }, + "papermill": { + "duration": 0.01081, + "end_time": "2026-09-26T19:42:11.693920", + "exception": false, + "start_time": "2026-09-26T19:42:11.683110", + "status": "completed" }, - "papermill": {}, "tags": [] }, "outputs": [ @@ -669,27 +613,16 @@ ], "source": [ "# Exercice 3 : modelisez un mini-Zebra a 4 maisons / 4 attributs.\n", - "\n", "# Indice : groups_4 = {\"Nat\": [...4...], \"Couleur\": [...4...], \"Animal\": [...4...]}, domaine 0..3.\n", - "\n", "# Etape 1 : definissez groups_4 (4 valeurs par attribut) et un solveur avec domaine 0..3 + 3 Distinct.\n", - "\n", "# Etape 2 : ajoutez 8 indices (identites + adjacences) de votre choix.\n", - "\n", "# Etape 3 : check() -> solution unique ?\n", "\n", - "\n", - "\n", "def resoudre_mini_zebra():\n", - "\n", " \"\"\"Retourne (solver, var_dict) pour une mini-enigme 4 maisons / 4 attributs.\"\"\"\n", - "\n", " # TODO etudiant : definir groups_4 + solveur + 8 indices\n", - "\n", " return None\n", "\n", - "\n", - "\n", "print(\"Exercice 3 a completer : modelisez un mini-Zebra a 4 maisons / 4 attributs.\")" ] }, @@ -697,35 +630,45 @@ "cell_type": "markdown", "id": "c17", "metadata": { - "papermill": {}, + "papermill": { + "duration": 0.002645, + "end_time": "2026-09-26T19:42:11.700879", + "exception": false, + "start_time": "2026-09-26T19:42:11.698234", + "status": "completed" + }, "tags": [] }, "source": [ "## Conclusion\n", "\n", - "\n", - "\n", "L'enigme d'Einstein illustre le gain du **declaratif** sur une classe de problemes ou l'approche humaine (deduction progressive sur un tableau) et l'approche naive (brute force) sont toutes deux laborieuses :\n", "\n", - "\n", - "\n", "- L'**encodage par position** (une variable entiere = position de chaque valeur) transforme un puzzle apparemment qualitatif en un système de contraintes arithmetiques : egalites (`Brit == Red`), adjacences (`|Blend - Cat| == 1`), permutations (`Distinct`).\n", - "\n", "- La **propagation de contraintes** resout les 25 variables entrelacees en millisecondes la ou la brute force affronte ~25 milliards de combinaisons ; le solveur **prouve l'unicite** en niant le temoin et en observant `unsat`.\n", - "\n", "- Le modèle est **paramètre par les données** : ajouter un indice, un attribut ou une maison se fait en modifiant l'instance, sans re-ecrire l'algorithme de resolution.\n", "\n", - "\n", - "\n", "**Contraste avec le job-shop (notebook 08)** : ici `Solver` suffit (on cherche une solution realisable, pas un optimum) - c'est la **satisfiabilite** pure, la ou l'ordonnancement relevait de l'**optimisation** (`Optimize.minimize` du makespan). Les deux postures du solveur, posees au notebook 01, trouvent ici leur illustration complementaire.\n", "\n", - "\n", - "\n", "Suite logique : retour a la [serie Z3-Python](README.md), ou explorez la version C# [Z3.Linq](../Z3-Linq2Z3/README.md) qui aborde la même enigme via la couche declarative LINQ." ] } ], "metadata": { + "cost": { + "api_provider": "none", + "api_usd_est": 0.0, + "cpu_min": 5, + "external_account": null, + "free_alternative": null, + "gpu_required": false, + "metadata_written": null, + "network": false, + "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU).", + "reduced_pedagogical": null, + "reproducibility": "HIGH", + "validator": "manual" + }, "kernelspec": { "display_name": "Python 3", "language": "python", @@ -741,23 +684,21 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.13.7" + "version": "3.13.13" }, - "cost": { - "api_usd_est": 0.0, - "api_provider": "none", - "cpu_min": 5, - "gpu_required": false, - "network": false, - "external_account": null, - "free_alternative": null, - "reduced_pedagogical": null, - "reproducibility": "HIGH", - "metadata_written": null, - "validator": "manual", - "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU)." + "papermill": { + "default_parameters": {}, + "duration": 2.374682, + "end_time": "2026-09-26T19:42:11.941082", + "environment_variables": {}, + "exception": null, + "input_path": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb", + "output_path": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-09-Enigme-Einstein-Python.ipynb", + "parameters": {}, + "start_time": "2026-09-26T19:42:09.566400", + "version": "2.6.0" } }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-10-Cryptarithmetic-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-10-Cryptarithmetic-Python.ipynb index 9504182380..ee021ee898 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-10-Cryptarithmetic-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-10-Cryptarithmetic-Python.ipynb @@ -363,29 +363,17 @@ "metadata": {}, "source": [ "### Exercice 1 - DONALD + GERALD = ROBERT\n", - "\n", "Modelisez le cryptarithme `DONALD + GERALD = ROBERT` (10 lettres distinctes : D, O, N, A, L, G, E, R, B, T).\n", "\n", - "\n", - "\n", "**Étapes** :\n", - "\n", "1. Variables `Ints` pour les 10 lettres, domaine `{0..9}`.\n", - "\n", "2. `Distinct` sur les 10 lettres.\n", - "\n", "3. Tetes non nulles : `D > 0`, `G > 0`, `R > 0`.\n", - "\n", "4. Equation positionnelle :\n", - "\n", " - `DONALD = 100000*D + 10000*O + 1000*N + 100*A + 10*L + L`\n", - "\n", " - `GERALD = 100000*G + 10000*E + 1000*R + 100*A + 10*L + D`\n", - "\n", " - `ROBERT = 100000*R + 10000*O + 1000*B + 100*E + 10*R + T`\n", "\n", - "\n", - "\n", "**Indice** : notez que `L` apparait deux fois dans DONALD (unite et dizaine) et `R` deux fois dans ROBERT - le solveur s'en occupe, il suffit d'ecrire l'equation positionnelle correcte." ] }, @@ -428,18 +416,12 @@ "metadata": {}, "source": [ "### Exercice 2 - Verifier l'unicite de la solution\n", - "\n", "Combien de solutions admet `SEND + MORE = MONEY` ? On sait qu'il y en a au moins une (cellule 3). Pour **prouver l'unicite**, on ajoute une contrainte qui **nie** la solution trouvee et on re-teste : si `unsat`, la solution etait unique.\n", "\n", - "\n", - "\n", "**Étapes** :\n", - "\n", "1. Re-resoudre `SEND + MORE = MONEY`, recupere le modèle `m`.\n", - "\n", "2. Ajouter la contrainte de negation : `Or(S != m[S], E != m[E], ...)` (au moins une lettre differe).\n", - "\n", - "3. Re-checker : si `unsat` -> unique ; si `sat` -> il existe une autre solution (compter par itération).\n" + "3. Re-checker : si `unsat` -> unique ; si `sat` -> il existe une autre solution (compter par itération)." ] }, { @@ -479,21 +461,13 @@ "metadata": {}, "source": [ "### Exercice 3 - Cryptarithme avec produit (multiplication)\n", - "\n", "Generalisez a la **multiplication** : `ABC * D = DBC`, ou `ABC = 100*A + 10*B + C` et `DBC = 100*D + 10*B + C`.\n", "\n", - "\n", - "\n", "**Étapes** :\n", - "\n", "1. Variables `A, B, C, D = Ints('A B C D')`, domaine `{0..9}`.\n", - "\n", "2. `Distinct(A, B, C, D)`, têtes `A > 0` et `D > 0`.\n", - "\n", "3. Equation : `(100*A + 10*B + C) * D == (100*D + 10*B + C)`.\n", "\n", - "\n", - "\n", "**Indice** : c'est la même structure que l'addition, mais l'opérateur `*` remplace `+`. Z3 traite les deux aussi bien (théorie arithmetique lineaire + non-lineaire)." ] }, @@ -534,16 +508,27 @@ "metadata": {}, "source": [ "## Conclusion\n", - "\n", "Les cryptarithmes illustrent un avantage central du **paradigme declaretif** : on exprime ce qu'on cherche (une affectation de chiffres distincts satisfaisant une equation positionnelle), pas **comment** le chercher. Le solveur Z3 se charge de la recherche via propagation de contraintes - instantanement la ou la brute force enumere des millions de candidats.\n", "\n", - "\n", - "\n", "Cette serie Z3-Python (notebooks 01 a 10) couvre maintenant le spectre complet : satisfaction de contraintes (01, 02), tactiques (03), chaînes/regex (04), quantificateurs (05), optimisation avancee (06), style declaratif (07), ordonnancement NP-difficile (08), CSP logique (09), et ici l'**arithmetique symbolique** sur entiers (10). Le pont avec la serie sœur Z3.Linq (C#) se fait via les mêmes exemples portes entre Microsoft.Z3 et pyz3." ] } ], "metadata": { + "cost": { + "api_provider": "none", + "api_usd_est": 0.0, + "cpu_min": 5, + "external_account": null, + "free_alternative": null, + "gpu_required": false, + "metadata_written": null, + "network": false, + "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU).", + "reduced_pedagogical": null, + "reproducibility": "HIGH", + "validator": "manual" + }, "kernelspec": { "display_name": "Python 3", "language": "python", @@ -560,20 +545,6 @@ "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.13.3" - }, - "cost": { - "api_usd_est": 0.0, - "api_provider": "none", - "cpu_min": 5, - "gpu_required": false, - "network": false, - "external_account": null, - "free_alternative": null, - "reduced_pedagogical": null, - "reproducibility": "HIGH", - "metadata_written": null, - "validator": "manual", - "notes": "Local execution via Z3 SMT solver (z3-solver Python package). Deterministic constraint solving: Z3 is deterministic given the same assertions and version. Runs entirely locally (no external API, no GPU)." } }, "nbformat": 4, diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb index e0f11e9f44..fd8fad6927 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb @@ -387,11 +387,8 @@ "metadata": {}, "source": [ "### Exercice 1 - Racine cubique de 2\n", - "\n", "Trouvez `c` tel que `c^3 = 2`, avec `c > 0`. La racine cubique de 2 est aussi un irrationnel algebrique, mais de **degré 3** (vs degré 2 pour la racine carree). Affichez le temoin et comparez la notation.\n", "\n", - "\n", - "\n", "**Étapes** : `c = Real('c')`, ajouter `c * c * c == 2` et `c > 0`, checker, afficher le modèle." ] }, @@ -432,15 +429,10 @@ "metadata": {}, "source": [ "### Exercice 2 - Discriminant et nombre de racines\n", - "\n", "Un trinome `q^2 + bq + c = 0` a des racines reelles ssi son **discriminant** `D = b^2 - 4c >= 0`.\n", - "\n", "- (a) Prouvez que `q^2 - 3q + 2 = 0` a une racine reelle (`sat` ; deux racines : 1 et 2).\n", - "\n", "- (b) Prouvez que `q^2 + q + 1 = 0` n'en a aucune (`unsat` ; D = -3 < 0).\n", "\n", - "\n", - "\n", "**Étapes** : pour chaque polynome, encoder `= 0` et checker. Le verdict `sat`/`unsat` confirme le signe du discriminant." ] }, @@ -482,11 +474,8 @@ "metadata": {}, "source": [ "### Exercice 3 - Distance minimale (optimisation sur les reels)\n", - "\n", "Minimisez `px^2 + py^2` sous la contrainte `px + py = 4` (point de la droite le plus proche de l'origine). La solution exacte est `px = py = 2`, distance minimale `sqrt(8)`.\n", "\n", - "\n", - "\n", "**Indice** : utilisez `Optimize()` avec `.minimize(px*px + py*py)`. **Note** : l'optimisation non-lineaire sur les reels est delicate (Z3 peut renvoyer un point sous-optimal) ; si le minimum trouve n'est pas 8, reflechissez a pourquoi (la théorie non-lineaire reelle est decidable mais l'optimisation globale reste dure)." ] }, @@ -528,33 +517,30 @@ "metadata": {}, "source": [ "## Conclusion\n", - "\n", "La théorie des reels de Z3 transforme le solveur en outil de **raisonnement algebrique exact**. La ou le calcul numérique flottant (`float`, `math.sqrt`) introduit des erreurs d'arrondi et ne peut jamais prouver une absence de solution, la théorie SMT `Real` offre : solutions rationnelles exactes, irrationnels algebriques (racine de 2 comme `root-obj`), et preuves d'impossibilite sur R tout entier (`unsat` pour `x^2 + 1 = 0`).\n", "\n", - "\n", - "\n", "Cette serie Z3-Python (notebooks 01 a 12) couvre maintenant l'eventail complet : entiers (01-06, 10, 11), satisfaction de contraintes (08 ordonnancement, 09 CSP logique, 11 graphes), tactiques (03), et ici l'**arithmetique reelle exacte** (12). Le pont avec la serie souer Z3.Linq (C#) se fait via les mêmes exemples portes entre Microsoft.Z3 et pyz3." ] } ], "metadata": { "cost": { - "api_usd_est": 0.0, "api_provider": "none", - "qcc_tokens_est": 0, + "api_usd_est": 0.0, "cpu_min": 1, + "external_account": false, + "free_alternative": "self", "gpu_min": 0, "gpu_required": false, - "vram_gb": 0, - "vram_tier": "none", + "metadata_written": "2026-08-03", "network": true, - "external_account": false, - "free_alternative": "self", + "notes": "Z3 SMT real arithmetic (nonlinear real constraints). Deterministic SMT. CPU-only. 8/8 cells executed.", + "qcc_tokens_est": 0, "reduced_pedagogical": false, "reproducibility": "HIGH", - "metadata_written": "2026-08-03", "validator": "check_cost_metadata.py", - "notes": "Z3 SMT real arithmetic (nonlinear real constraints). Deterministic SMT. CPU-only. 8/8 cells executed." + "vram_gb": 0, + "vram_tier": "none" }, "kernelspec": { "display_name": "Python 3", diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb index 0769b49d41..1057298a42 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb @@ -558,11 +558,8 @@ "metadata": {}, "source": [ "### Exercice 1 - Deborde signe mais pas non signe\n", - "\n", "Trouvez `a, b` tels que `a + b` deborde en **signe** (la somme devient negative, `somme < 0` signed) mais PAS en non signe (`somme >= a` unsigned reste vrai). Indice : choisissez `a, b` proches de `2^31 - 1` (la limite positive d'un int32 signe).\n", "\n", - "\n", - "\n", "**Étapes** : `a, b = BitVecVal(..., 32)` ; verifier `UGE(somme, a)` vrai (pas de debord non signe) MAIS `simplify(somme < 0)` ... attention, `< 0` en pyz3 sur BitVec est signe par defaut." ] }, @@ -603,11 +600,8 @@ "metadata": {}, "source": [ "### Exercice 2 - Borne exacte du debordement pour `t + t`\n", - "\n", "Pour `a = b = t`, a partir de quelle plus petite valeur de `t` l'addition `t + t` deborde-t-elle (en unsigned) ? Prouvez que `t >= 2^31` implique debordement, et que `t = 2^31 - 1` ne deborde pas.\n", "\n", - "\n", - "\n", "**Étapes** : `tt = t + t` ; `debord = ULT(tt, t)` ; solver avec `t >= 2^31` -> `sat` ; avec `t == 2^31 - 1` -> pas de debord." ] }, @@ -648,11 +642,8 @@ "metadata": {}, "source": [ "### Exercice 3 - Prouver que `65536 * 65536` deborde en BV32\n", - "\n", "`65536 = 2^16`, donc `65536 * 65536 = 2^32`, qui en uint32 vaut exactement `0` (enveloppe complet). Prouvez que le produit deborde : `produit < 65536` (unsigned), ou directement `produit == 0`.\n", "\n", - "\n", - "\n", "**Étapes** : `m1 = m2 = BitVecVal(65536, 32)` ; `produit = m1 * m2` ; `solver.add(produit == 0)` -> `sat` (preuve que le produit enveloppe a 0)." ] }, @@ -693,33 +684,30 @@ "metadata": {}, "source": [ "## Conclusion\n", - "\n", "La théorie des bit-vectors de Z3 est l'outil canonique de la **verification formelle de code**. La ou `Int` (entiers non bornes) rend le debordement inexpressible, `BitVec` modelise l'arithmetique machine exacte (modulo 2^n) et permet de **prouver** des proprietes de surete ou d'inevitabilite sur tout le domaine des entrees.\n", "\n", - "\n", - "\n", "Cette serie Z3-Python (notebooks 01 a 14) couvre maintenant les grandes théories du solveur : entiers et optimisation (01-11), reels exacts (12), diagnostic par UNSAT cores (13), et ici l'**arithmetique machine bornee** (14). Chacune exerce une capacite distincte qu'aucune approche numérique classique ne peut reproduire : decision exacte, non pas approximation." ] } ], "metadata": { "cost": { - "api_usd_est": 0.0, "api_provider": "none", - "qcc_tokens_est": 0, + "api_usd_est": 0.0, "cpu_min": 1, + "external_account": false, + "free_alternative": "self", "gpu_min": 0, "gpu_required": false, - "vram_gb": 0, - "vram_tier": "none", + "metadata_written": "2026-08-03", "network": true, - "external_account": false, - "free_alternative": "self", + "notes": "Z3 BitVec overflow detection. Deterministic SMT. CPU-only. 10/10 cells executed.", + "qcc_tokens_est": 0, "reduced_pedagogical": false, "reproducibility": "HIGH", - "metadata_written": "2026-08-03", "validator": "check_cost_metadata.py", - "notes": "Z3 BitVec overflow detection. Deterministic SMT. CPU-only. 10/10 cells executed." + "vram_gb": 0, + "vram_tier": "none" }, "kernelspec": { "display_name": "Python 3", diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb index 5a40ee4835..9738e45912 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb @@ -731,11 +731,8 @@ }, "source": [ "### Exercice 1 - Core sur un conflit cache (2 coupables parmi 4)\n", - "\n", "Construisez 4 contraintes sur `z` dont 2 sont compatibles et 2 en conflit (ex : `z <= 3`, `z >= 0`, `z == 7`, `z != 9`). Obtenez le core et verifiez qu'il ne contient **que** les 2 coupables.\n", "\n", - "\n", - "\n", "**Étapes** : `z = Int('z')`, 4 `assert_and_track` etiquetes, `check()`, afficher `unsat_core()` (doit exclure les 2 compatibles)." ] }, @@ -793,11 +790,8 @@ }, "source": [ "### Exercice 2 - Planning : identifier puis relacher la coupable\n", - "\n", "Encodez un planning sur `j` : (a) `j >= 8`, (b) `j <= 18`, (c) `j != 3`, (d) `j == 3`. Obtenez le core, identifiez la coupable, puis **relachez-la** (re-checkez le sous-ensemble sans elle) -> le système devient SATISFIABLE.\n", "\n", - "\n", - "\n", "**Étapes** : core = {j!=3, j=3} ; retirer l'une des deux du solver ; re-`check()` -> `sat`." ] }, @@ -855,11 +849,8 @@ }, "source": [ "### Exercice 3 - Core minimal parmi 10 contraintes\n", - "\n", "Construisez 10 contraintes sur `k` : 3 conflictuelles (`k == 1`, `k == 2`, `k == 3`) + 7 compatibles (`k >= 0`, `k <= 100`, etc.). Le core doit valoir exactement **3** (les 3 incompatibles), les 7 compatibles etant ecartees.\n", "\n", - "\n", - "\n", "**Étapes** : 10 `assert_and_track` ; `check()` ; compter `len(unsat_core())` -> attendu 3." ] }, @@ -917,11 +908,8 @@ }, "source": [ "## Conclusion\n", - "\n", "Le UNSAT core transforme le solveur d'oracle binaire en **outil de diagnostic**. La ou `unsat` dit seulement ' impossible ', `unsat_core()` dit ' impossible **a cause de ces contraintes-la** ' - le sous-ensemble minimal responsible du conflit. Sur une specification surcontrainte, ce diagnostic est directement actionnable : il pointe la contrainte a relacher.\n", "\n", - "\n", - "\n", "Cette serie Z3-Python (notebooks 01 a 13) couvre maintenant les **trois postures** du solveur : **decider** (sat/unsat, 01-11), **optimiser** (Optimize, 06/08), et ici **expliquer** (unsat_core, 13). La ou l'ingenieur classique debug a l'aveugle un système insatisfiable, le solveur SMT isole chirurgicalement la cause - la différence entre un oracle et un partenaire de raisonnement." ] }