3sat.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# Simple Quantum Implementation using Qiskit Aqua for Boolean satisfiability problems\n",
    "\n",
    "\n",
    "\n",
    "This Jupyter notebook demonstrates how easy it is to use quantum algorithms from [Qiskit Aqua](https://qiskit.org/aqua) to solve Boolean satisfiability problems [(SAT)](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem). \n",
    "\n",
    "It is based on the Qiskit tutorial [Using Grover search for 3-SAT problems](https://github.com/Qiskit/qiskit-tutorials/blob/master/community/aqua/optimization/grover.ipynb) by [Jay Gambetta](https://github.com/jaygambetta) and [Richard Chen](https://github.com/chunfuchen) and a hands-on workshop by David Mesterhazy.\n",
    "\n",
    "Implemented by [Jan-R. Lahmann](http://twitter.com/JanLahmann) using Qiskit, binder and RISE."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Boolean Satisfiabilty problems (SAT)\n",
    "\n",
    "The Boolean satisfiability problem [(SAT)](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) considers a Boolean expression with N boolean variables involving negation (NOT, $\\neg$), conjunction (AND, $\\wedge$) and disjunction (OR, $\\vee$), as in the following (simple) example:  \n",
    "$$ f(x_1, x_2) = (x_1 \\vee x_2) \\wedge (x_1 \\vee \\neg x_2) . $$\n",
    "\n",
    "The problem is to determine whether there is any assignment of values (TRUE, FALSE) to the Boolean variables which makes the formula true. \n",
    "\n",
    "It's something like trying to flip a bunch of switches to find the setting that makes a light bulb turn on.  \n",
    "SAT is of central importance in many areas of computer science, including complexity theory, algorithmics, cryptography, artificial intelligence, circuit design, and automatic theorem proving."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "SAT was the first problem proven to be NP-complete.  \n",
    "This means that all problems in the [complexity class NP](https://en.wikipedia.org/wiki/NP_(complexity)) are at most as difficult to solve as SAT. \n",
    "\n",
    "There is no known classical algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists.  \n",
    "Whether Boolean satisfiability problems have a classical algorithm that is polynomial in time is equivalent to the [P vs. NP problem](https://en.wikipedia.org/wiki/P_versus_NP_problem).  \n",
    "\n",
    "\n",
    "While [Grover's quantum search algorithm](https://en.wikipedia.org/wiki/Grover's_algorithm) does not provide exponential speed-up to this problem, it may nevertheless provide some speed-up in contrast to classical black-box search strategies.\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Basic definitions and terminology\n",
    "\n",
    "\n",
    "A *literal* is either a variable, or the negation of a variable.  \n",
    "A *clause* is a disjunction (OR, $\\vee$) of literals, or a single literal.  \n",
    "A formula is in *conjunctive normal form* [(CNF)](https://en.wikipedia.org/wiki/Conjunctive_normal_form) if it is a conjunction (AND, $\\wedge$) of clauses, or a single clause.  \n",
    "\n",
    "A problem in conjunctive normal form is called *3-SAT* if each clause is limited to at most three literals.  \n",
    "3-SAT is also NP-complete.\n",
    "\n",
    "Example for 3-SAT: $ (x_1 ∨ ¬x_2) ∧ (¬x_1 ∨ x_2 ∨ x_3) ∧ ¬x_1 $.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Solving 3-SAT using Qiskit Aqua \n",
    "\n",
    "We will show how to solve a 3-SAT problem using quantum algorithms from [Qiskit Aqua](https://qiskit.org/aqua).\n",
    "\n",
    "Let us consider three Boolean variables $x_1, x_2, x_3$ and a Boolean function $f$ given by:\n",
    "\n",
    "\\begin{align*} \n",
    "f(x_1, x_2, x_3) \\;= &\\;\\;\\;\\;\n",
    "\\;(\\neg x_1 \\vee \\neg x_2 \\vee \\neg x_3)  \\\\\n",
    "&\\;\\; \\wedge \\; ( x_1 \\vee \\neg x_2 \\vee  x_3) \\\\\n",
    "&\\;\\; \\wedge \\;( x_1 \\vee  x_2 \\vee \\neg x_3) \\\\\n",
    "&\\;\\; \\wedge \\;( x_1 \\vee \\neg x_2 \\vee \\neg x_3) \\\\\n",
    "&\\;\\; \\wedge \\;(\\neg x_1 \\vee  x_2 \\vee  x_3) \n",
    "\\end{align*}\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "It is common, to state 3-SAT problems in [DIMACS CNF format](https://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html):\n",
    "\n",
    "1. The file may begin with comment lines. \n",
    "* The \"problem\" line begins with \"p\", followed by the problem type \"cnf\", the number of variables and the number of clauses.\n",
    "* The remainder of the file contains lines defining the clauses.\n",
    "* A clause is defined by listing the index of each positive literal, and the negative index of each negative literal. \n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [],
   "source": [
    "# import Qiskit quantum libraries\n",
    "from qiskit.visualization import plot_histogram\n",
    "from qiskit.utils import QuantumInstance\n",
    "from qiskit.algorithms import Grover\n",
    "from qiskit.circuit.library import PhaseOracle\n",
    "from qiskit import Aer\n",
    "from qiskit.algorithms import AmplificationProblem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "c This is an example DIMACS 3-sat file with 3 satisfying solutions: 1 -2 3 0, -1 -2 -3 0, 1 2 -3 0\n",
      "p cnf 3 5\n",
      "-1 -2 -3 0\n",
      "1 -2 3 0\n",
      "1 2 -3 0\n",
      "1 -2 -3 0\n",
      "-1 2 3 0\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# import the problem in DIMACS CNF format\n",
    "import os\n",
    "import wget\n",
    "if not '3sat3-5.cnf' in os.listdir():\n",
    "    wget.download('https://raw.githubusercontent.com/Qiskit/qiskit-tutorials/master/community/aqua/optimization/3sat3-5.cnf')\n",
    "with open('3sat3-5.cnf', 'r') as f:\n",
    "    sat_cnf = f.read()\n",
    "    oracle = PhaseOracle.from_dimacs_file(\"3sat3-5.cnf\")\n",
    "print(sat_cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "To apply a quantum algorithm from Qiskit Aqua to this problem, we simply need to import the Qiskit libraries and run the algorithm with the appropriate parameters."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAoAAAAHICAYAAADeLlu/AAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMywgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/NK7nSAAAACXBIWXMAAA9hAAAPYQGoP6dpAABgyElEQVR4nO3deVhU1eM/8PcdQHYQF0AUIXNBTcENUHPBDdPcckGtUDO1Ukutvia5Zm6lZqXmrpiammaWCogC4oLg+jEtFVdwQcGFLWSb8/uD39wYWQRnYAbm/Xqenpxzz9x7zmEY3nc9khBCgIiIiIgMhkLXDSAiIiKi8sUASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGGNdN6AyUyqVuHfvHqytrSFJkq6bQ0RERJWYEAKpqalwcnKCQlH8MT4GwDJ07949ODs767oZREREZEDi4+NRp06dYuswAJYha2trAHk/CBsbGx23hoiIiCqzlJQUODs7y/mjOAyAZUh12tfGxoYBkIiIiMpFSS47400gRERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiIDwwBIREREZGAYAImIiIgMjN4GwFOnTqFXr16oWrUqLC0t4e3tjZ07d5b4/UFBQRg6dCjc3NxQtWpVWFhYwM3NDaNHj8bVq1cL1I+NjcX8+fPRsWNHODk5oUqVKnB2doa/vz8uX76sza4RERER6ZQkhBC6bsTzwsPD4evrCzMzMwwdOhTW1tbYvXs3bt++jcWLF+PTTz994TomTpyIP//8E15eXnBycoKJiQn++ecfBAUFwdjYGAcOHECXLl3k+kOHDsWOHTvw2muv4fXXX4eNjQ3++usvBAUFwdzcHMHBwejYsWOp+pGSkgJbW1skJyfDxsam1ONAREREVFKlyR16FwBzcnLg5uaGO3fu4OTJk/Dw8AAAJCcnw9PTE7du3cLVq1fh4uJS7HqePXsGMzOzAuWHDx9Gt27d0Lp1a5w6dUou37RpE9zd3dGiRQu1+tu3b8ewYcPQpEkTXLp0qVR9YQAkIiKi8lKa3KF3p4DDwsJw/fp1DB8+XA5/AGBra4uAgABkZWUhMDDwhespLPwBQNeuXWFnZ4dr166plY8cObJA+APyjgw2bNgQf//9N5KSkkrXGSIiIiI9pHcBMCIiAgDQo0ePAst8fX0BAEeOHHnp9UdFReHJkyd47bXXSvweExMTAICxsfFLb5eIiIhIX+hdoomNjQUANGjQoMAyR0dHWFlZyXVK4uDBgzhx4gQyMzMRGxuLffv2oUaNGvjuu+9K9P6YmBhcunQJbdq0QdWqVYutm5mZiczMTPl1SkoKACA7OxvZ2dkAAIVCASMjI+Tm5kKpVMp1VeU5OTnIf1beyMgICoWiyHLVelVUITUnJ6dE5SYmJlAqlcjNzZXLJEmCsbFxkeVFtZ19Yp/YJ/aJfWKf2Cfd9ak09C4AJicnA8g75VsYGxsbuU5JHDx4EEuWLJFf169fH9u3b0erVq1K1JYRI0ZAoVDgm2++eWH9BQsWYM6cOYW2wcLCAgBQt25dtGjRAhcuXEBcXJxcp1GjRnBzc0NMTAwSExPlcg8PD7i4uCAyMhKpqalyedu2bWFvb4+DBw+qfcB8fHxgbm6OAwcOqLWhV69eyMjIQHh4uFxmbGyM3r17IykpCVFRUXK5tbU1unTpgvj4eJw/f14ur1mzJtq1a4fY2FhcuXJFLmef2Cf2iX1in9gn9kn3fXJyckJJ6d1NID169EBoaChiY2NRv379Astr166NtLS0UoVAAEhLS8Pff/+Nr776CocOHcKGDRswfPjwIutnZGSgd+/eCA8Px7x58xAQEPDCbRR2BNDZ2RlJSUnyxZiGtjfCPrFP7BP7xD6xT+xT+fQpPT294t4FPHjwYOzatQunT58u9CidtbU17Ozs1FJvaeTk5KB169a4du0abt68iZo1axao8+zZM/Tt2xehoaGYNm0a5s+f/1Lb4l3AREREVF4q9F3Aqmv/CrvOLyEhAWlpaYVeH1hSxsbG8PHxQXp6Ok6fPl1geUZGhhz+/u///u+lwx8RERGRvtK7ANipUycAedfNPS8kJEStzsu6d+8egP/u7lXJyMhAv379EBoais8++wyLFi3SaDvlYcWKFXB1dYWZmRm8vLwQExNTZN21a9eiQ4cOsLOzg52dHbp161ag/oMHDzBy5Eg4OTnBwsICPXv2LBDGnz17hvHjx6N69eqwsrLCwIED8eDBgzLpHxEREWmf3gXArl27ol69eti2bZvaxZDJycmYP38+qlSpAn9/f7n8/v37uHz5coFrAgs7ugfkhcg9e/agatWqaNu2rVz+7NkzOfxNmTIF3377rXY7VgZ27NiBKVOmYNasWTh79izc3d3h6+uLhw8fFlo/IiICw4YNQ3h4OKKiouDs7IwePXrg7t27AAAhBPr3748bN25g7969OHfuHFxcXNCtWzekp6fL65k8eTL+/PNP/Prrrzhy5Aju3buHt956q1z6TERERJrTu2sAgdJNBTdy5EgEBgZi48aNGDlypFwuSRJee+01NG/eHHXq1EF6ejouXLiAo0ePwsTEBDt27MCAAQMKrMfR0RHjxo0rtF0jR46Eq6triftR1tcAenl5oU2bNli+fDkAQKlUwtnZGRMnTsQXX3zxwvfn5ubCzs4Oy5cvh7+/P65evYpGjRrh4sWLaNq0qbxOR0dHzJ8/H++//z6Sk5NRs2ZNbNu2DYMGDQIAXL58GY0bN0ZUVBS8vb213k8iIiJ6sdLkDr17DAyQd1v1sWPHMGvWLOzYsQPZ2dlo1qwZFi1aBD8/vxKtY/78+QgPD8eRI0eQmJgIhUKBunXrYuzYsZg0aRIaN26sVv/WrVsA8q4zLOxRLgDQuXPnUgXAspSVlYUzZ85g2rRpcplCoUC3bt3Ubi8vzr///ovs7GxUq1YNAOQ7mPPPoqJQKGBqaopjx47h/fffx5kzZ5CdnY1u3brJddzc3FC3bl0GQCIiogpCLwMgAHh6eiIoKOiF9TZt2oRNmzYVKJ82bZpaOHoR1QwkFUVSUhJyc3Ph4OCgVu7g4IDLly+XaB1Tp06Fk5OTHOZUQW7atGlYvXo1LC0t8d133+HOnTu4f/8+gLyAXKVKlQIPxXZwcEBCQoLmHSMiIqIyp3fXAFL5WLhwIbZv3449e/bIR/xMTEzw22+/4erVq6hWrRosLCwQHh6ON954o9RPGCci0jVt3ySXlpaGCRMmoE6dOjA3N0eTJk2watWqAuuKiopCly5dYGlpCRsbG3Ts2BEZGRla7x+RJvhXvYKqUaMGjIyMCtx9++DBAzg6Ohb73sWLF2PhwoU4ePAgmjdvrrasVatWOH/+PJ4+fYr79+8jODgYjx49Qr169QDkTceXlZWFp0+flnq7RETlRds3yQHAlClTEBwcjC1btuCff/7BpEmTMGHCBPzxxx9ynaioKPTs2RM9evRATEwMTp06hQkTJnAnmvSPoDKTnJwsAIjk5OQyWb+np6eYMGGC/Do3N1fUrl1bLFiwoMj3LFq0SNjY2IioqKgSbePq1atCoVCIkJAQIYQQT58+FSYmJmLXrl1yncuXLwsAJV4nEVFZ8/T0FOPHj5df5+bmCicnp2K/H/PLyckR1tbWIjAwUC5r2rSp+Oqrr9TqtWzZUnz55Zfyay8vLzF9+nQNW0/0ckqTO7hLUoFNmTIFa9euRWBgIP755x98+OGHSE9Px6hRowAA/v7+atdBLlq0CDNmzMCGDRvg6uqKhIQE+eHaKr/++isiIiLkR8F0794d/fv3R48ePQDkzdE8evRoTJkyBeHh4Thz5gxGjRqFtm3b8gYQItILqpvk8t+spulNcgDQrl07/PHHH7h79y6EEAgPD8fVq1fl78eHDx8iOjoa9vb2aNeuHRwcHNCpUyccO3ZMux0k0gK9vQmEXszPzw+JiYmYOXMmEhIS4OHhgeDgYPnGkLi4OLXTDj/99BOysrLkx7eozJo1C7NnzwaQ91zFKVOm4MGDB6hVqxb8/f0xY8YMtfrfffcdFAoFBg4ciMzMTPj6+mLlypVl21kiohIqi5vkAODHH3/E2LFjUadOHRgbG0OhUGDt2rXo2LEjAODGjRsAgNmzZ2Px4sXw8PDA5s2b0bVrV1y8eFGjWayItI0BsIKbMGECJkyYUOiy5+9sVj3qpjgff/wxPv7442LrmJmZYcWKFVixYkVJm0lEVGGobpKLiIhQeyzWjz/+iJMnT+KPP/6Ai4sLIiMjMX78eDkoKpVKAMC4cePkMzEtWrTA4cOHsWHDBixYsEAn/SEqDAMgERFVKtq4Se7QoUNqN8llZGQgICAAe/bsQe/evQEAzZs3x/nz57F48WJ069YNtWrVAgA0adJEbZ2NGzdGXFycNrpGpDW8BpCIiCqVKlWqoFWrVjh8+LBcplQqcfjwYbUpQJ/3zTffYO7cuQgODkbr1q3VlmVnZyM7O7vA3bxGRkbykT9XV1c4OTnhypUranWuXr0KFxcXTbtFpFU8AkhERJXOlClTMGLECLRu3Rqenp5YtmxZgZvkateuLZ+WXbRoEWbOnIlt27bJN8kBgJWVFaysrGBjY4NOnTrh888/h7m5OVxcXHDkyBFs3rwZS5cuBZA3Bennn3+OWbNmwd3dHR4eHggMDMTly5exa9cu3QwEUREYAImIqNIpi5vktm/fjmnTpuHtt9/G48eP4eLignnz5uGDDz6Q60+aNAnPnj3D5MmT8fjxY7i7uyM0NBSvvvpq2XeaqBQkIYTQdSMqq9JMykxERESkidLkDl4DSERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiCqVFStWwNXVFWZmZvDy8kJMTEyRddeuXYsOHTrAzs4OdnZ26NatW4H6kiQV+t+3334LIG+KxdGjR+OVV16Bubk5Xn31VcyaNQtZWVll2k8iIk0wABJRpbFjxw5MmTIFs2bNwtmzZ+Hu7g5fX188fPiw0PoREREYNmwYwsPDERUVBWdnZ/To0QN3796V69y/f1/tvw0bNkCSJAwcOBAAcPnyZSiVSqxevRqXLl3Cd999h1WrViEgIKBc+kxE9DL4HMAyxOcAEpUvLy8vtGnTBsuXLweQN/2Xs7MzJk6ciC+++OKF78/NzYWdnR2WL18Of3//Quv0798fqampatOMPe/bb7/FTz/9hBs3brxcR4iIXgKfA0hEBicrKwtnzpxBt27d5DKFQoFu3bohKiqqROv4999/kZ2djWrVqhW6/MGDB9i/fz9Gjx5d7HqSk5OLXAcRkT5gACSiSiEpKQm5ubnyVF8qDg4O8ryuLzJ16lQ4OTmphcj8AgMDYW1tjbfeeqvIdVy7dg0//vgjxo0bV/LGExGVM84FTEQEYOHChdi+fTsiIiJgZmZWaJ0NGzbg7bffLnL53bt30bNnTwwePBhjxowpy+YSEWmEAZCIKoUaNWrAyMgIDx48UCt/8OABHB0di33v4sWLsXDhQhw6dAjNmzcvtM7Ro0dx5coV7Nixo9Dl9+7dg4+PD9q1a4c1a9a8XCeIiMoJTwETUaVQpUoVtGrVSu3mDKVSicOHD6Nt27ZFvu+bb77B3LlzERwcjNatWxdZb/369WjVqhXc3d0LLLt79y46d+6MVq1aYePGjVAo+NVKRPqNRwAruDHLdN0CYO0kXbeAKM+UKVMwYsQItG7dGp6enli2bBnS09MxatQoAIC/vz9q166NBQsWAAAWLVqEmTNnYtu2bXB1dZWvFbSysoKVlZW83pSUFPz6669YsmRJgW2qwp+LiwsWL16MxMREedmLjjwSEekKAyARVRp+fn5ITEzEzJkzkZCQAA8PDwQHB8s3hsTFxakdnfvpp5+QlZWFQYMGqa1n1qxZmD17tvx6+/btEEJg2LBhBbYZGhqKa9eu4dq1a6hTp47aMj5li4j0FZ8DWIbK4zmAPAJIREREAJ8DSERERETF4ClgIiKqtHiWhKhwPAJIREREZGAYAImIiIgMDAMgERERkYFhACQiIiIyMAyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGGNdN4CISJvGLNN1C4C1k3TdAiKi4vEIIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiIDwwBIREREZGAYAImIiIgMDAMgERERkYFhACQiIiIyMAyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMDobQA8deoUevXqhapVq8LS0hLe3t7YuXNnid4rhEBQUBA+/PBDNG/eHLa2trCwsIC7uzvmz5+PZ8+elWg9H374ISRJgiRJSEhI0KQ7RERERHrDWNcNKEx4eDh8fX1hZmaGoUOHwtraGrt374afnx/i4+Px6aefFvv+zMxM9OrVC6ampujcuTN8fX3x7NkzhISE4Msvv8Tvv/+OiIgIWFhYFLmO0NBQrFq1CpaWlkhPT9d2F4mIiIh0Ru8CYE5ODsaMGQOFQoHIyEh4eHgAAGbOnAlPT08EBARg0KBBcHFxKXIdRkZG+Prrr/HRRx/Bzs5OLs/OzsbAgQPx559/YsWKFfj8888LfX9ycjLee+89DBo0CImJiThy5IhW+0hERESkS3p3CjgsLAzXr1/H8OHD5fAHALa2tggICEBWVhYCAwOLXYeJiQm+/PJLtfCnKp82bRoAFBvqPvnkE2RkZGDFihUv3xEiIiIiPaV3RwAjIiIAAD169CiwzNfXF0Dx4e1FTExMAADGxoV3/c8//0RgYCC2bdsGe3v7l94OERERkb7SuwAYGxsLAGjQoEGBZY6OjrCyspLrvIwNGzYAKDxgPnr0CGPGjEH//v0xbNiwUq87MzMTmZmZ8uuUlBQAeaees7OzAQAKhQJGRkbIzc2FUqmU66rKc3JyIISQy42MjKBQKIos1we5ubla7ZNqrFRUYT0nJ6dE5SYmJlAqlcjNzZXLJEmCsbFxkeVFtZ19qoh9MoGu5R8b/px03ScJupadnc2fE/tULn0qDb0LgMnJyQDyTvkWxsbGRq5TWkFBQVi9ejUaN26M0aNHF1j+0UcfISsrCz/99NNLrX/BggWYM2dOgfKDBw/KN5zUrVsXLVq0wIULFxAXFyfXadSoEdzc3BATE4PExES53MPDAy4uLoiMjERqaqpc3rZtW705QnnhwgWt9ungwYNqvzQ+Pj4wNzfHgQMH1Lbbq1cvZGRkIDw8XC4zNjZG7969kZSUhKioKLnc2toaXbp0QXx8PM6fPy+X16xZE+3atUNsbCyuXLkil2v758Q+lWef+kHX8o8Bf0667ZM+7BAcOHCAPyf2qVz65OTkhJKSRP6Iqwd69OiB0NBQxMbGon79+gWW165dG2lpaaUOgadOnULXrl1hbGyMo0ePomnTpmrLd+zYgaFDh2Lz5s1499135fLOnTvjyJEjuH//PhwdHYvdRmFHAJ2dnZGUlAQbGxsA2t8bGbOsVMNQJlZN5BFA9kl/+vTRCt3/wV85nkcA9aVPY7/X/RHAleN5BJB9Kp8+paenw9bWFsnJyXLuKIreHQFUHfkrKuClpKQUuLnjRU6fPo0ePXpAoVAgJCSkQPh7/Pgxxo8fj969e6uFv9IyNTWFqalpgXITExP52kMVIyMjGBkZFahb1LWJRZXrA1U/tNWn58fqZcoVCkWhh8OLKi+q7exTxe6TrpSmr/w5lX2fdC1/u/hzYp/05XtPPy4iy0d17V9h1/klJCQgLS2t0OsDi3L69Gl0794dSqUSISEhaNOmTYE6cXFxePToEfbv3y8/+Fn1n+qGk1q1akGSJLXDs0REREQVkd4dVurUqRMWLFiAgwcPYujQoWrLQkJC5DoloQp/ubm5CAkJgZeXV6H1qlevXug1gQCwf/9+JCQkYPjw4TA3N0f16tVL0RsiIiIi/aN3AbBr166oV68etm3bho8//lh+FmBycjLmz5+PKlWqwN/fX65///59JCcno1atWmo3jpw5cwbdu3dHTk4OgoOD0bZt2yK36ezsjHXr1hW6rHPnzkhISMCSJUteeA0gERERUUWgdwHQ2NgY69atg6+vLzp27Kg2Fdzt27exePFiuLq6yvWnTZuGwMBAbNy4ESNHjgSQd01f9+7d8fTpU/Ts2ROhoaEIDQ1V207VqlUxadKk8usYERERkZ7QuwAI5N1WfezYMcyaNQs7duxAdnY2mjVrhkWLFsHPz++F709JScGTJ08AAMHBwQgODi5Qx8XFhQGQiIiIDJJeBkAA8PT0RFBQ0Avrbdq0CZs2bVIrc3V1hbaebqOamYSIiIiostC7u4CJiIiIqGwxABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBqZMHgR969YthIaGwszMDAMGDICVlVVZbIaIiIiIXoJGRwDnz5+PV155RZ52DcibOeO1117DBx98gJEjR6Jly5Z4/Pixxg0lIiIiIu3QKAD+/vvvcHV1hZ2dnVw2depUKJVKzJkzBx9++CGuXbuGZcuWadpOIiIiItISjQLgrVu30KRJE/n1vXv3cOrUKYwfPx7Tp0/H8uXL0bVrV+zZs0fjhhIRERGRdmgUAFNSUlC1alX5dWRkJCRJQp8+feSyli1bIi4uTpPNEBEREZEWaRQAHRwccPv2bfl1aGgoTE1N4eXlJZc9e/YMkiRpshkiIiIi0iKN7gJu06YN9u7di3379sHMzAw7duyAj48PTE1N5To3b96Ek5OTxg0lIiIiIu3Q6AhgQEAAcnJy0K9fP/j6+uLZs2cICAiQl2dmZiIyMlLtiCARERER6ZZGRwBbtmyJkydP4ueffwYADBkyBJ6envLyc+fOwcfHB8OHD9eslURERESkNRo/CNrd3R3u7u6FLvP29uYdwERERER6RmszgaSlpeHq1atIT09Hhw4dtLVaIiIiItIyjecCvnXrFvr16wc7Ozu0adMGPj4+8rLjx4+jSZMmiIiI0HQzRERERKQlGgXAuLg4eHt748CBA+jXrx/atm0LIYS83MvLC0lJSfjll180bigRERERaYdGAXDWrFl48uQJjhw5gl27dqF79+5qy42NjdGhQwccP35co0YSERERkfZoFABDQkIwYMAAtGvXrsg6Li4uuHv3riabISIiIiIt0igAPn78GK6ursXWEUIgMzNTk80QERERkRZpPBVcbGxssXX++usv1K1bV5PNEBEREZEWaRQAu3fvjn379uHChQuFLj969CjCwsLQq1cvTTZDRERERFqkUQCcPn06zM3N0bFjR8ybNw/Xrl0DAAQFBWHGjBno2bMnatSogc8//1wrjSUiIiIizWn0IGhXV1eEhIRg6NChmDFjBiRJghACb775JoQQqFu3Lnbt2oVatWppq71EREREpCGNZwLx8vJCbGws/vzzT0RHR+Px48ewsbGBl5cX+vXrhypVqmijnURERESkJVqZCs7Y2BgDBgzAgAEDtLE6IiIiIipDGk8FR0REREQVS6mOAG7evBkAMGDAAFhbW8uvS8Lf3790LSMiIiKiMlGqADhy5EhIkgRvb29YW1vLr4sjhIAkSQyARERERHqiVAFww4YNkCRJvqt348aNZdIoIiIiIio7pT4CmN+IESO02RYiIiIiKgca3QQSGRmJuLi4YuvEx8cjMjJSk80QERERkRZpFAB9fHywadOmYuts3rwZPj4+mmyGiIiIiLRIowAohHhhHaVS+cIbRYiIiIio/JT5cwBjY2Nha2tb1pshIiIiohIq9Uwg7733ntrr33//Hbdu3SpQLzc3V77+74033njpBhIRERGRdpU6AOa/5k+SJJw/fx7nz58vtK4kSWjTpg2+++67l20fEREREWlZqQPgzZs3AeRd/1evXj1MmjQJn3zySYF6RkZGsLOzg6WlpeatJCIiIiKtKXUAdHFxkf+9ceNGeHh4qJURERERkX4rdQDMjw+CJiIiIqp4ShUAVQ909vT0hJmZWake8NyxY8fStYyIiIiIykSpAmDnzp0hSRL++ecfNGzYUH5dErm5uS/VQCIiIiLSrlIFwJkzZ0KSJNSoUUPtNRERERFVHKUKgLNnzy72NRERERHpvzKfCYSIiIiI9AsDIBEREZGBKdUp4C5durzURiRJwuHDh1/qvURERESkXaUKgBERES+1Ed4oQkRERKQ/ShUAlUplWbWDiIiIiMoJrwEkIiIiMjAMgEREREQGhlPBERERERkYTgVHREREZGA4FRwRERGRgeFUcEREREQGhjeBEBERERmYUh0BLEpmZiYOHDiAc+fOITk5Gba2tmjRogV69eoFU1NTbWyCiIiIiLRE4wD4xx9/YOzYsUhMTIQQQi6XJAn29vZYs2YN+vTpo+lmiIiIiEhLNAqAhw8fxsCBA2FkZIT33nsPHTp0gIODAx48eIDIyEhs2bIFb731FkJCQl56HmEiIiIi0i6NAuCsWbNgbm6OEydO4LXXXlNb5u/vj48//hjt27fHrFmzGACJiIiI9IRGN4GcO3cOfn5+BcKfSvPmzTFkyBCcPXtWk80QERERkRZpFAAtLCxQs2bNYuvY29vDwsJCk80QERERkRZpFAC7deuGQ4cOFVvn0KFD6N69uyabISIiIiIt0igALl68GA8fPoS/vz/i4+PVlsXHx+Pdd99FUlISFi9erFEjiYiIiEh7SnUTSGE3ctjZ2WHr1q3Yvn076tatK98FHBcXh9zcXDRv3hzvvvsuDh8+rLVGExEREdHLK1UAjIiIKHJZTk4Obty4gRs3bqiV/+9//+N8wURERER6pFQBUKlUllU7iIiIiKiccC5gIiIiIgPDAEhERERkYDSeCxgA7ty5g/DwcNy7dw+ZmZkFlkuShBkzZmhjU0RERESkIY0D4Oeff47vv/8eubm5cpkQQr7xQ/Xv0gbAU6dOYdasWThx4gSys7PRrFkzTJkyBUOGDCnR+69fv46ff/4ZZ8+exZkzZ3Dv3j24uLjg1q1bxb5PqVRi06ZN2LBhAy5evIisrCzUqVMH7du3xw8//ABra+tS9YOIiIhI32h0Cnjt2rVYsmQJfHx8sGvXLgghMGLECPzyyy/44IMPYGxsjMGDByMsLKxU6w0PD0f79u1x7NgxDBkyBB988AESEhLg5+eHJUuWlGgdR48exZw5c3DgwAFUq1YNCsWLu5qZmYl+/fph9OjRSE1NxciRIzFx4kS0atUKBw4cQHJycqn6QURERKSPNDoCuGbNGri6uiIoKEgOWK6urvDz84Ofnx+GDBmC7t27Y/DgwSVeZ05ODsaMGQOFQoHIyEh4eHgAAGbOnAlPT08EBARg0KBBcHFxKXY9HTt2RFRUFNzd3WFubg4zM7MXbvuLL77Avn37sHDhQkydOlVtGe+AJiIiospCoyOAly9fRs+ePdWOruXk5Mj/7tSpE3r37l2qmUDCwsJw/fp1DB8+XA5/AGBra4uAgABkZWUhMDDwheupV68evL29YW5uXqLt3r17F8uXL0eHDh0KhD8AUCgUJTqKSERERKTvNL4GsGrVqvK/LS0t8ejRI7XljRo1euF8wfmpHjbdo0ePAst8fX0BAEeOHCl9Q19g165dyMnJweDBg5Gamoo//vgDcXFxcHBwgK+vL2rXrq31bRIRERHpgkYBsHbt2rhz5478+tVXX0V0dLRanYsXL8LS0rLE64yNjQUANGjQoMAyR0dHWFlZyXW06cyZMwCAp0+folGjRrh//768rEqVKli4cCEmT55c7DoyMzPV7oJOSUkBAGRnZyM7OxtA3pFEIyMj5Obmqp1WVpXn5ORACCGXGxkZQaFQFFmuD3Jzc7XaJ9VYqRgb531M8x9dLq7cxMQESqVS7cYkSZJgbGxcZHlRbWefKmKfTKBr+ceGPydd90n3M1FlZ2fz58Q+lUufSkOjANi+fXscPXpUft2vXz98/fXXGDduHPr27Ytjx44hKCgIAwcOLPE6VTda2NraFrrcxsamTG7GePjwIQBgzpw56N69Ow4dOgRnZ2dERkZi7NixmDJlCtzc3PDGG28UuY4FCxZgzpw5BcoPHjwICwsLAEDdunXRokULXLhwAXFxcXKdRo0awc3NDTExMUhMTJTLPTw84OLigsjISKSmpsrlbdu2hb29vcb91oYLFy5otU8HDx5U+6Xx8fGBubk5Dhw4oLbdXr16ISMjA+Hh4XKZsbExevfujaSkJERFRcnl1tbW6NKlC+Lj43H+/Hm5vGbNmmjXrh1iY2Nx5coVuVzbPyf2qTz71A+6ln8M+HPSbZ/0YYfgwIED/DmxT+XSJycnJ5SUJPJH3FKKiIjAokWLsGrVKri4uCAtLQ2dOnXCuXPnIEkShBBwdXVFeHj4C2/aUOnRowdCQ0MRGxuL+vXrF1heu3ZtpKWllToEmpmZwdHRscjHwKi2W6tWLVy7dk0ObAAQFBSEXr16oWvXrsWezi7sCKCzszOSkpJgY2MDQPt7I2OWlWoYysSqiTwCyD7pT58+WqH7P/grx/MIoL70aez3uj8CuHI8jwCyT+XTp/T0dNja2iI5OVnOHUXR6Ahg586d0blzZ/m1lZUVTp48ib179+L69etwcXFBnz59SnUKWHXkr6iAl5KSAjs7O02aXex2u3Xrphb+gLxrD01NTXH69Oli12FqagpTU9MC5SYmJjAxUf+jZGRkBCMjowJ1VR+akpbrA1U/tNWn58fqZcqLummnqPKi2s4+Vew+6Upp+sqfU9n3Sdfyt4s/J/ZJX773tJ4qTExMMGjQoJd+v+rav9jYWLRq1UptWUJCAtLS0uDp6alRGwvTqFEjAOo3tagoFApYW1vL1/QRERERVWRau4vg0aNHCAsLw549exAWFlbgbuCS6tSpE4C86+aeFxISolZHm7p06QIA+PvvvwssS0xMRFJSElxdXbW+XSIiIqLypnEAvHXrFvr16wcHBwd0794dgwYNQvfu3eHg4ID+/fu/cOq153Xt2hX16tXDtm3b1C6GTE5Oxvz581GlShX4+/vL5ffv38fly5c1vjGkU6dOaNy4MQ4fPozQ0FC5XAiBgIAAACjxNHRERERE+kyjU8DXr19H+/bt8fDhQzRo0ADt27eHg4MDHjx4gBMnTuCPP/7AyZMnceLECdSrV69kDTI2xrp16+Dr64uOHTti6NChsLa2xu7du3H79m0sXrxY7UjctGnTEBgYiI0bN2LkyJFyeVJSEj777DP5dXZ2NpKSktTqLF68GDVq1ACQdy5948aN6NKlC3r16oW33noLderUwbFjxxATE4OWLVviiy++0GS4iIiIiPSCRgFw6tSpSExMxKpVqzBmzBhI0n93WwkhsGbNGnz00UeYOnUqfv311xKv18fHB8eOHcOsWbOwY8cOZGdno1mzZli0aBH8/PxKtI60tLQCM4akp6erlc2ePVsOgADg5eWFmJgYzJo1C4cPH0ZKSgrq1q2LadOmISAgoFQ3sxARERHpK40eA2NnZ4fOnTtjz549Rdbp168fIiMj8eTJk5fdTIWVkpJS4tuxX5Y+PAZm7SRdt4DoP/ydoPz4eSBDUprcodE1gLm5uWjatGmxdV577TW159oQERERkW5pFABbtmyJS5cuFVvn0qVLaN26tSabISIiIiIt0igAzps3D0FBQVi3bl2hy9esWYOQkBB8/fXXmmyGiIiIiLSoVDeBfPXVVwXKfHx8MG7cOCxZskTtLuDjx4/j6tWr8PX1xeHDh9GuXTutNZqIiIiIXl6pAuDs2bOLXHblyhW1yYpVgoODERISghkzZpS6cURERESkfaUKgOHh4WXVDiIiIiIqJ6UKgGUxBRsRERERlS+tzQVMRERERBWDRjOBqBw/fhybNm3C+fPnkZKSAhsbG7Ro0QL+/v54/fXXtbEJIiIiItISjQPg5MmT8cMPP0A1oYgkSRBC4MyZM1i/fj0++eQTLF26VOOGEhEREZF2aHQKODAwEN9//z0aNGiArVu34t69e8jJycH9+/exbds2NGzYEN9//z02b96srfYSERERkYY0CoA//fQT6tSpg+joaAwbNgyOjo6QJAkODg4YOnQoTp48idq1a2PlypXaai8RERERaUijAHjp0iUMHDgQtra2hS63tbXFwIEDXzhdHBERERGVnzK/C1iSpLLeBBERERGVgkYBsGnTpti9ezfS0tIKXZ6amordu3ejadOmmmyGiIiIiLRIowA4btw43LlzB23btsXu3buRlJQEAEhKSsKuXbvQrl073LlzBx9++KFWGktEREREmtPoMTCjRo3CuXPnsHz5cgwZMgQAoFAooFQqAQBCCEycOBEjRozQvKVEREREpBUaPwfwhx9+wODBgwt9EPSIESPQoUMHbbSTiIiIiLREowAYGRkJGxsbdOjQgUGPiIiIqILQ6BpAHx8frFmzRlttISIiIqJyoFEAtLe3h5mZmbbaQkRERETlQKMA2L17d0RERMjzABMRERGR/tMoAC5cuBCPHj3C2LFj8fjxY221iYiIiIjKkEY3gbzzzjuoWrUqNmzYgC1btuCVV16Bg4NDgdk/JEnC4cOHNWooEREREWmHRgEwIiJC/ndmZiYuX76My5cvF6jH6eCIiIiI9IdGAVD1wGciIiIiqjhe6hrAqKgodOnSBdbW1rC1tUX37t0RExOj7bYRERERURko9RHAv/76C127dsWzZ8/kssOHD+PEiROIiYlB06ZNtdpAIiIiItKuUh8BXLhwIZ49e4Yvv/wSCQkJSEhIwIwZM5CRkYFFixaVRRuJiIiISItKfQTw6NGjeP311zF37ly5bM6cOYiIiMCRI0e02jgiIiIi0r5SHwF88OABvL29C5R7eXnhwYMHWmkUEREREZWdUgfA7OxsWFlZFSi3tLREdna2VhpFRERERGVHo5lAiIiIiKjieannAG7ZsgUnT55UK7t27RoAoFevXgXqS5KE/fv3v8ymiIiIiEjLXioAXrt2TQ58zwsODi5QxplAiIiIiPRHqQPgzZs3y6IdRERERFROSh0AXVxcyqIdRERERFROeBMIERERkYFhACQiIiIyMAyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiIDwwBIREREZGAYAImIiIgMDAMgERERkYFhACQiIiIyMAyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMDobQA8deoUevXqhapVq8LS0hLe3t7YuXNnqdaRmZmJr776Cg0aNICZmRmcnJwwduxYPHz4sND6GRkZWLp0KVq2bAk7OztUrVoV7u7umDdvHpKTk7XRLSIiIiKdM9Z1AwoTHh4OX19fmJmZYejQobC2tsbu3bvh5+eH+Ph4fPrppy9ch1KpRL9+/RASEgJvb28MHDgQsbGxWLduHQ4fPoyTJ0+iZs2acv3s7Gz4+PggOjoaHh4eGDlypNyW6dOn45dffkFMTAwsLCzKqttERERE5ULvAmBOTg7GjBkDhUKByMhIeHh4AABmzpwJT09PBAQEYNCgQXBxcSl2PYGBgQgJCcGwYcOwdetWSJIEAFi1ahU+/PBDTJ8+HatXr5br79mzB9HR0RgwYAB+++03tXX1798fe/fuxa5du+Dv76/dDhMRERGVM707BRwWFobr169j+PDhcvgDAFtbWwQEBCArKwuBgYEvXM/atWsBAAsWLJDDHwCMGzcO9erVw9atW5GRkSGX37hxAwDwxhtvFFhX7969AQCJiYkv1SciIiIifaJ3ATAiIgIA0KNHjwLLfH19AQBHjhwpdh3Pnj1DdHQ0GjVqVOBIoSRJ6N69O9LT03H69Gm5/LXXXgMABAUFFVjf/v37IUkSfHx8StUXIiIiIn2kd6eAY2NjAQANGjQosMzR0RFWVlZynaJcv34dSqWy0HXkX3dsbCw6dOgAIO8oX//+/bFnzx60aNECnTt3BpB3DeDNmzexZs0atGzZstjtZmZmIjMzU36dkpICIO/6wuzsbACAQqGAkZERcnNzoVQq5bqq8pycHAgh5HIjIyMoFIoiy/VBbm6uVvukGisVY+O8j2lOTk6Jyk1MTKBUKpGbmyuXSZIEY2PjIsuLajv7VBH7ZAJdyz82/Dnpuk8SdC07O5s/J/apXPpUGnoXAFV329ra2ha63MbG5oV35JZkHfnrAXkDvXv3bgQEBOCbb77B+fPn5WUjRoxA9+7dX9j2BQsWYM6cOQXKDx48KN88UrduXbRo0QIXLlxAXFycXKdRo0Zwc3NDTEyM2qlmDw8PuLi4IDIyEqmpqXJ527ZtYW9v/8I2lYcLFy5otU8HDx5U+6Xx8fGBubk5Dhw4oLbdXr16ISMjA+Hh4XKZsbExevfujaSkJERFRcnl1tbW6NKlC+Lj49V+tjVr1kS7du0QGxuLK1euyOXa/jmxT+XZp37QtfxjwJ+TbvukDzsEBw4c4M+JfSqXPjk5OaGkJJE/4uqBHj16IDQ0FLGxsahfv36B5bVr10ZaWlqxIfDEiRNo37493n77bWzZsqXA8rVr12Ls2LFYunQpJk+eDAD4999/MWzYMERHR+P7779Ht27dAACHDh3CJ598AiEEoqOj4erqWuR2CzsC6OzsjKSkJDl0antvZMyyIptTblZN5BFA9kl/+vTRCt3/wV85nkcA9aVPY7/X/RHAleN5BJB9Kp8+paenw9bWFsnJyXLuKIreHQFUHbUrKuClpKTAzs5O43XkrwcA8+fPxx9//IG9e/eib9++crmfnx/MzMzQv39/zJs3T765pDCmpqYwNTUtUG5iYgITE/U/SkZGRjAyMipQV/WhKWm5PlD1Q1t9en6sXqZcoVAUeji8qPKi2s4+Vew+6Upp+sqfU9n3Sdfyt4s/J/ZJX7739OMisnzyX5/3vISEBKSlpRV5bZ9KvXr1oFAoirxWsLDrDFU3fxR2o4eq7Ny5cyXoAREREZF+07sA2KlTJwB51809LyQkRK1OUczNzeHp6YkrV67g9u3basuEEAgNDYWlpSVat24tl2dlZQEo/FEvqrLCju4RERERVTR6FwC7du2KevXqYdu2bWoXQyYnJ2P+/PmoUqWK2sOY79+/j8uXLxc43Tt27FgAwLRp09TO469evRo3btzA22+/DXNzc7m8ffv2AIA5c+aonVPPzc3FrFmzABR+dJCIiIiootG7C8uMjY2xbt06+Pr6omPHjmpTwd2+fRuLFy9WuxFj2rRpCAwMxMaNG+Xp24C8O3d37NiBX375BTdv3kSnTp1w7do1/Pbbb3jllVfw9ddfq203ICAAe/fuxebNm3HmzBl06dIFAHD48GH8/fffaNCgQYmmoCMiIiLSd3p3BBDIO9J27NgxtG/fHjt27MBPP/0EBwcHbN++vcQhTKFQYO/evZg9ezYSExPx3Xff4fjx4xg9ejSioqLU5gEG8m6rPnPmDCZMmIDMzEysXr0aa9asQW5uLj7//HNER0e/8OYTIiIioopA7x4DU5mkpKSU+Hbsl6UPj4FZO0nXLSD6D38nKD9+HsiQlCZ36OURQCIiIiIqOwyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA8MASERERGRgGACJiIiIDAwDIBEREZGBYQAkIiIiMjAMgEREREQGhgGQiIiIyMAwABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiIDwwBIREREZGAYAImIiIgMDAMgEVEltGLFCri6usLMzAxeXl6IiYkptv6vv/4KNzc3mJmZoVmzZjhw4IDa8tmzZ8PNzQ2Wlpaws7NDt27dEB0drVbn6tWr6NevH2rUqAEbGxu8/vrrCA8P13rfiEhzDIBERJXMjh07MGXKFMyaNQtnz56Fu7s7fH198fDhw0LrnzhxAsOGDcPo0aNx7tw59O/fH/3798fFixflOg0bNsTy5cvx119/4dixY3B1dUWPHj2QmJgo13nzzTeRk5ODsLAwnDlzBu7u7njzzTeRkJBQ5n0motKRhBBC142orFJSUmBra4vk5GTY2NiUyTbGLCuT1ZbK2km6bgHRf/g7AXh5eaFNmzZYvnw5AECpVMLZ2RkTJ07EF198UaC+n58f0tPTsW/fPrnM29sbHh4eWLVqVaHbUH2/HTp0CF27dkVSUhJq1qyJyMhIdOjQAQCQmpoKGxsbhIaGolu3bmXQ0xfj54EMSWlyB48AElUSujjl5+rqCkmS1P5buHCh1vtGJZeVlYUzZ86oBS6FQoFu3bohKiqq0PdERUUVCGi+vr5F1s/KysKaNWtga2sLd3d3AED16tXRqFEjbN68Genp6cjJycHq1athb2+PVq1aaal3RKQtDIBElYCuTvkBwFdffYX79+/L/02cOLFM+0rFS0pKQm5uLhwcHNTKHRwcijwVm5CQUKL6+/btg5WVFczMzPDdd98hNDQUNWrUAABIkoRDhw7h3LlzsLa2hpmZGZYuXYrg4GDY2dlpsYdEpA0MgESVwNKlSzFmzBiMGjUKTZo0wapVq2BhYYENGzYUWv/7779Hz5498fnnn6Nx48aYO3cuWrZsKZ8yBIDhw4ejW7duqFevHpo2bYqlS5ciJSUFFy5cUFuXtbU1HB0d5f8sLS3LtK+kOz4+Pjh//jxOnDiBnj17YsiQIfJOhhAC48ePh729PY4ePYqYmBj0798fffr0wf3793XcciJ6HgMgUQWnq1N+KgsXLkT16tXRokULfPvtt8jJydGwR6SJGjVqwMjICA8ePFArf/DgARwdHQt9j6OjY4nqW1paon79+vD29sb69ethbGyM9evXAwDCwsKwb98+bN++He3bt0fLli2xcuVKmJubIzAwUIs9JCJtYAAkquB0dcoPAD7++GNs374d4eHhGDduHObPn4//+7//01LP6GVUqVIFrVq1wuHDh+UypVKJw4cPo23btoW+p23btmr1ASA0NLTI+vnXm5mZCQD4999/AeTtfOSnUCigVCpL3Q8iKlvGum4AEekv1Sm/pKQkrF27FkOGDEF0dDTs7e0BAFOmTJHrNm/eHFWqVMG4ceOwYMECmJqa6qrZBm/KlCkYMWIEWrduDU9PTyxbtgzp6ekYNWoUAMDf3x+1a9fGggULAACffPIJOnXqhCVLlqB3797Yvn07Tp8+jTVr1gAA0tPTMW/ePPTt2xe1atVCUlISVqxYgbt372Lw4MEA8kKknZ0dRowYgZkzZ8Lc3Bxr167FzZs30bt3b90MBBEViUcAiSo4XZ3yK4yXlxdycnJw69atl+sMaYWfnx8WL16MmTNnwsPDA+fPn0dwcLB81DcuLk7turx27dph27ZtWLNmDdzd3bFr1y78/vvveO211wAARkZGuHz5MgYOHIiGDRuiT58+ePToEY4ePYqmTZsCyPscBgcHIy0tDV26dEHr1q1x7Ngx7N27t8BlA0SkezwCSFTB5T/l179/fwD/nfKbMGFCoe9RnfKbNGmSXFbaU36FOX/+PBQKhXyEkHRnwoQJRf78IyIiCpQNHjxYPpr3PDMzM/z2228v3Gbr1q0REhJSqnYSkW4wABJVAro45RcVFYXo6Gj4+PjA2toaUVFRmDx5Mt555x0+9oOISM/xFDBVCtp8CHJ2djamTp2KZs2awdLSEk5OTvD398e9e/fkOhEREQUegKz679SpU2XWz6Lo4pSfqakptm/fjk6dOqFp06aYN28eJk+eLIdIIiLSXwyAVOFp+yHI//77L86ePYsZM2bg7Nmz+O2333DlyhX07dtXXke7du3UHn58//59vP/++3jllVfQunXrcun38yZMmIDbt28jMzMT0dHR8PLykpdFRERg06ZNavUHDx6MK1euIDMzExcvXkSvXr3kZapTfnfv3kVmZibu3buHvXv3ok2bNnKdli1b4uTJk3j69CkyMjLw999/Y9q0abz5g0jPlPcOssr+/fvh5eUFc3Nz2NnZyZeokH5gAKQKT9sPQba1tUVoaCiGDBmCRo0awdvbG8uXL8eZM2cQFxcHIO+6u/wPP65evTr27t2LUaNGQZKkcus7EVFxdLGDDAC7d+/Gu+++i1GjRuF///sfjh8/juHDh5d5f6nkeA0gVWiqhyBPmzZNLivJQ5DzP74EyHsI8u+//17kdpKTkyFJEqpWrVro8j/++AOPHj2Sr7kj0rUxy3TdAmDtJF23gPLvIAPAqlWrsH//fmzYsAFffPFFgfr5d5ABYO7cuQgNDcXy5cuxatUqeQc5v+XLl8PT0xNxcXGoW7cucnJy8Mknn+Dbb7/F6NGj5XpNmjQpw55SafEIIFVoZfkQZJVnz55h6tSpGDZsGGxsbAqts379evj6+qJOnTov0QsiIu0rj1mCgII7yGfPnsXdu3ehUCjQokUL1KpVC2+88YbaXOO6oKtT4QCQmZkJDw8PSJKE8+fPa7NbL40BkKgY2dnZGDJkCIQQ+Omnnwqtc+fOHYSEhKjt6RIR6ZqudpBv3LgBAJg9ezamT5+Offv2wc7ODp07d8bjx4817dZL0dWpcJX/+7//g5OTU5n172XwFDBVaGX5EGRV+Lt9+zbCwsKKPPq3ceNGVK9evchf/PLE035EVF6K2kFWTf335ZdfYuDAgQDyvifr1KmDX3/9FePGjSv3turiVLhKUFAQDh48iN27dyMoKKgMe1k6PAJIFVpZzXuq+mKLjY3FoUOHUL169ULXJYTAxo0b4e/vDxMTEy30iIhIO8prBzk0NFRtB7lWrVoA1K/5MzU1Rb169eQb6cqTrk6FA3ljN2bMGPz888+wsLDQrCNaxgBIFd6UKVOwdu1aBAYG4p9//sGHH35Y4CHI+W8S+eSTTxAcHIwlS5bg8uXLmD17Nk6fPi3PmpCdnY1Bgwbh9OnT2Lp1K3Jzc5GQkICEhARkZWWpbTssLAw3b97E+++/X34dJiIqAV3tILdq1Qqmpqa4cuWK2ntu3boFFxcXbXStVHR1KlwIgZEjR+KDDz7Q2ePBisNTwFTh+fn5ITExETNnzkRCQgI8PDwKPARZofhvX0f1EOTp06cjICAADRo0UHsI8t27d/HHH38AADw8PNS2FR4ejs6dO8uv169fj3bt2sHNza1sO0lE9BK0PUuQagf57Nmz2Ldvn7yDDADVqlVDlSpVYGNjgw8++ACzZs2Cs7MzXFxc8O233wJAkdMNVmRFnQr/8ccfkZqaqnYAQp8wAFKloM15T11dXSGEKNF2t23bVuI2EhGVN13tIH/77bcwNjbGu+++i4yMDHh5eSEsLEwn00Tq6lrxsLAwREVFFXg4fuvWrfH2228jMDBQk25pjAGQiIioEtPFDrKJiQkWL16MxYsXl6qtZSH/qXDVbCSqU+FFjYvqVPikSZPksuJOhYeHhxc4Ff7DDz/g66+/ll/fu3cPvr6+2LFjh9pMTbrCAEhERESVmi5Ohee/ExgArKysAACvvvqqXjwzlgGQiIiIKjVdXiuurxgAiYiIqNLT1bXimrynLDEAUqXAByATERGVHAMgERFRJcedZHoeHwRNREREZGB4BJCIiIgqPR4FVccjgEREREQGhgGQiIiIyMAwABIREREZGAZAIiIiIgPDAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiIDwwBIREREZGAYAImIiIgMDAMgERERkYFhACQiIiIyMAyARERERAaGAZCIiIjIwDAAEhERERkYBkAiIiIiA6O3AfDUqVPo1asXqlatCktLS3h7e2Pnzp2lWkdmZia++uorNGjQAGZmZnBycsLYsWPx8OHDIt+zdetWeHp6wtLSEnZ2dnjzzTdx9uxZTbtDREREpDf0MgCGh4ejffv2OHbsGIYMGYIPPvgACQkJ8PPzw5IlS0q0DqVSiX79+mHWrFmoUaMGJk2ahLZt22LdunVo27YtEhMTC7xn3rx5eOedd/Dw4UN88MEHGDx4MCIjI9GuXTscP35c290kIiIi0gljXTfgeTk5ORgzZgwUCgUiIyPh4eEBAJg5cyY8PT0REBCAQYMGwcXFpdj1BAYGIiQkBMOGDcPWrVshSRIAYNWqVfjwww8xffp0rF69Wq4fGxuL2bNno2HDhoiJiYGtrS0A4KOPPoK3tzfGjBmDixcvQqHQy8xMREREVGJ6l2bCwsJw/fp1DB8+XA5/AGBra4uAgABkZWUhMDDwhetZu3YtAGDBggVy+AOAcePGoV69eti6dSsyMjLk8o0bNyInJwdffvmlHP4AwMPDA8OGDcM///yDY8eOaaGHRERERLqldwEwIiICANCjR48Cy3x9fQEAR44cKXYdz549Q3R0NBo1alTgSKEkSejevTvS09Nx+vRprW6XiIiIqCLQu1PAsbGxAIAGDRoUWObo6AgrKyu5TlGuX78OpVJZ6Dryrzs2NhYdOnSQ/21lZQVHR8di6xcnMzMTmZmZ8uvk5GQAwOPHj5GdnQ0AUCgUMDIyQm5uLpRKpVxXVZ6TkwMhhFxuZGQEhUJRZHnWs2KbVC6ePMnVap9UY6VibJz3Mc3JySmyPOuZidb7VVopKdBqn/IzMTGBUqlEbm6uXCZJEoyNjdXK9WEcHj0qWV9L2qf85UV9xvKX69sYaKNP+ctL+vukT+Og7e+90vw+ZT2ToGuPHmWXyfdefi/6fcp6pvvjPcnJef3W9vde/vLifp+ynhlpvU+llZKCMvneU5Wnp6cDgNpnrCh6FwBVoSn/adj8bGxs5DqarCN/PdW/7e3tS1y/MAsWLMCcOXMKlL/yyivFvq+i2zxN1y3QDxyHPBwHjoEKxyEPxyEPx6H8xiA1NbXIDKSidwGwIps2bRqmTJkiv1YqlXj8+DGqV6+udh2iPklJSYGzszPi4+PloGtoOAZ5OA55OA55OA4cAxWOQ56KMA5CCKSmpsLJyemFdfUuAKoSa1FH21JSUmBnZ6fxOvLXU/27NPULY2pqClNTU7WyqlWrFvsefWFjY6O3H+jywjHIw3HIw3HIw3HgGKhwHPLo+zi8KKuo6P6igOcUd71dQkIC0tLSiry2T6VevXpQKBRFXrNX2HWGDRo0QFpaGhISEkpUn4iIiKii0rsA2KlTJwDAwYMHCywLCQlRq1MUc3NzeHp64sqVK7h9+7baMiEEQkNDYWlpidatW2t1u0REREQVgd4FwK5du6JevXrYtm0bzp8/L5cnJydj/vz5qFKlCvz9/eXy+/fv4/LlywVO344dOxZA3nV5+e+GWb16NW7cuIG3334b5ubmcvmoUaNgbGyMefPmqa3r/Pnz+OWXX9C4cWO8/vrr2u6uzpmammLWrFkFTl0bEo5BHo5DHo5DHo4Dx0CF45Cnso2DJEpyr3A5Cw8Ph6+vL8zMzDB06FBYW1tj9+7duH37NhYvXoxPP/1Urjty5EgEBgZi48aNGDlypFyuVCrRq1cvhISEwNvbG506dcK1a9fw22+/wdXVFdHR0ahZs6badufNm4fp06fDxcUFAwcORGpqKrZv346srCwcPnwY7du3L68hICIiIiozencEEAB8fHxw7NgxtG/fHjt27MBPP/0EBwcHbN++XS38FUehUGDv3r2YPXs2EhMT8d133+H48eMYPXo0oqKiCoQ/APjyyy+xZcsW1KxZEz/99BN27tyJDh064MSJEwx/REREVGno5RFAIiIiIio7enkEkIiIiIjKDgMgERERkYFhACQiIiIyMAyARERERAaGAdCAFXX/D+8LIiIiqtwYAA2YJEm4e/cuACArKwv//vuvXE6GhTsDRFQcfhdUPnwMjAESQmDfvn1Yv349/vrrL6SlpaF58+Zo1qwZWrVqBQ8PD9SvXx+mpqYQQjAQGojY2FjY29sjNTUV5ubmqF69uq6bRHqI3wmkws9CxcYAaIBmzpyJxYsXw8LCAs7OzsjOzkZWVhbi4+MhhIC7uzsGDRoEf39/ODg46Lq5ZSo3NxcKhcJgv8QyMzPx66+/YuXKlTh37hwUCgUaNGiA+vXro1WrVmjXrh1atmwJa2trXTe1zAkhkJubCyMjI4P9POT38OFDJCYmonr16khNTUXNmjVRtWpVXTeLyllubi5iY2Px5MkTAHm/J6+++mql/9tgCBgADcytW7fQtGlTdO7cGUuWLIGbmxuSkpIQHx+P69evIzIyEiEhIYiNjYW7uzvmz5+PN954A0qlEgpF5bliID4+Hs7OzvJrpVIJIQSMjIx02Kry9+mnn+L777+Hi4sLGjRoABMTEzx9+hR//fUXUlJS4OzsjDfffBPvvfceWrVqpevmlpnr16/j1VdflV8rlUoolUoYGxvrsFW6cf/+fXz55ZcIDQ3F3bt3YW1tjVdeeQWNGzeGl5cXXn/9dTRr1qzSzIf6PNVRLUP+DKhcuXIF06ZNw4EDB5CVlQVTU1PY2dnB1dUVbdu2Rc+ePdGuXTtYWlrquqn0EhgADczcuXOxbNky7Ny5E127dkVOTo7aF1xKSgouXbqEnTt34vvvv4eDgwOCgoLg4eGhu0Zr2a1bt1CvXj306NEDw4YNw5tvvql2ujM3NxeSJEGhUMh/DLKyslClShUdtlr7bt68iSZNmqBPnz5YsWIFatasidTUVDx9+hT3799HZGQk9uzZg1OnTqF27dqYM2cO/P39K91pn+vXr6NBgwZwc3PDe++9h3feeQeOjo7y8tzcXACAkZGR3Pf09HSkpaWhevXqlSogJCQkYMCAAYiOjkbPnj1hZWUFhUKB27dv48KFC8jIyECTJk0wZMgQjBkzBrVq1dJ1k7UuJSUFT58+Rd26deWy/J8BQ3Hv3j307NkTly5dwrvvvosaNWrA2NgYly5dwtGjR5GSkoKqVatiwIABGDduHDw9PXXd5DLx5MkTXLhwAd7e3pVvp0eQQfH39xe1atUSCQkJQgghlEql2v/z2759u7C1tRXe3t7l2sayNn/+fCFJkvxfjRo1xIgRI8T+/ftFdna2Wt3MzEwhhBCrVq0SXbt2FVeuXNFFk8vEvHnzRLVq1cThw4eFEELk5OSoLc/OzhY3btwQy5YtEzVr1hSSJIng4GBdNLVMLVq0SO3zIEmS6Ny5s9iyZYvIyspSq5v/8+Dp6SnOnj2riyaXmZkzZwpbW1uxbNkyuezJkyciPj5eREZGiunTp4smTZoIhUIh2rZtK44dOyaEKPz7o6KaMmWKkCRJdOjQQWzYsEGkp6erLc/Ozha5ublqZffv3xcPHjyoVOMwffp0YWdnJ9atWyeXZWZmiqysLBEXFydWr14t2rdvLxQKhWjSpInYt2+fEKJyfRaEEOKzzz4TkiSJli1birlz54qLFy8WWVfV96tXr4rz588X+P7QNwyABmbx4sVCkiTx66+/ymXPf5nl/wUeNWqUqFGjhrh8+XK5tbGsvfnmm8La2lqsW7dOjBgxQlhYWMh/+OvXry8+++wzERMTo/aet956S0iSJNLS0nTUau376KOPRNWqVUV8fLwQovgv7oMHD4patWqJRo0aiWfPnpVXE8vFwIEDhbm5udi2bZuYOXOmaNKkifx5MDExEUOHDpVDskpl/DwIIUSTJk3Em2++KR4+fCiEKPiZePbsmfjf//4nhyQ3Nzfx4MEDXTS1zDRr1qzADsGAAQPE/v371eqpxiYlJUW8/fbbwtfXt8AOZEXm7u4uevbsKf98C/t+SExMFD/++KOoVq2asLa2Fn///Xd5N7PMeXh4CIVCIapVqyZ/Hnx8fMTq1avFnTt3CtRPS0sTw4YNE97e3gyApF8iIyOFlZWVcHNzE6dOnVJbplQq5TCo+v/8+fOFpaVlgUBUUT18+FB4enqK2rVry2UZGRli69atomvXrmpf+m3atBE//PCD2Llzp6hVq5bo06ePDluufevXrxeSJIkVK1bIX+45OTlFBsFp06YJKyurSnXUKzExUbRr1044OjrKZZmZmSIoKEiMHj1a1KpVS/481KxZU3zxxRdiy5YtlfLzkJCQIBo3biy6d+/+wrrZ2dnihx9+EJIkialTp5ZD68rH9evXRc2aNUWnTp1EZGSk+PDDD0XdunXlz4CdnZ346KOP1H4Hzp07J+zs7ESnTp1013AtS0pKEq1bty7R2Z/s7Gyxfft2IUmSGDduXDm0rvzcvHlTODk5CW9vb3H+/Hkxd+5c0bFjR2FmZiYkSRLW1tZiyJAhYs+ePeLRo0dCCCFiYmJEtWrVhI+Pj45b/2IMgAZE9Yd97dq1wsjISEiSJMaOHSsOHTokUlJSCtT/999/xbBhw0T16tXLu6llJi4uTnTo0EH07t1bCPHfKT2Ve/fuicWLF6sdBVD9sj9/BKCi++uvv0Tt2rVFtWrVxJ9//qm2TKlUyqeEVTsDS5cuFWZmZuLEiRPl3taykpCQIHr27Cm6d+8usrOzC+yxJyYmis2bN4u+ffsKS0tLtR2EyvR5UO38DRo0SNjY2Ijo6Gi5/PlLA/Jr1qyZ6NKli0hNTS2vppapgwcPCkmSxKeffiqXPX36VOzYsUMMHjxY2Nrayj//V199VSxcuFBMnTpVSJIknwKt6FR/J8aMGSMkSRJ//vmnvGNY3BHO9u3bizZt2shBqDIICwsTCoVCfPzxx3JZamqqCAkJEZMnTxbNmzeXPw+1a9cWkyZNEuPGjaswnwcGQAOUlpYmfvrpJ2Fvby8kSRL29vaiX79+Yv78+eLQoUPi8ePHIjo6WowbN05UqVJF7cuwosvKyhJhYWHixIkTcrBR/ZF7/lT4lStXxPjx44UkSaJatWq6aG6ZUX3JBwUFiTp16ghJkoSvr6/YuXOnePz4cYH6aWlpYsiQIZVqZ0AlNjZWXLx4scDn4fkjoXFxceKrr74SFhYWws7OThdNLXNr1qyRr397/lqn3NxctXFJTk4WvXr1Eq+99poumlomTpw4IZydncWaNWuEEKJA4Ll9+7b48ccfRefOndV2Birj5+HAgQNCkiTRsGFDERISorYsJydH7bPw9OlT0b9/f9GwYUNdNLXMnD9/XjRo0ED88MMPQoiC10nfv39f/PLLL2LEiBHilVdeqXCfBwZAA/L8H7S0tDSxbNky0bZtW2FsbCx/eBUKhahSpYqQJEmMGjWq0OscKrrnw56Kai9X9YseExMjLCwsxNixY8uzeeUmOztb7Nq1S21P1t3dXYwfP17s3r1b/PPPP+K3334Tfn5+wsjISHzxxRe6bnK5UoVB1echKiqqUn8ehBBi4cKFQqFQCEmSxIgRI0RISIjIyMiQl6u+Rw4dOiRq164txowZo6umal1WVpa4dOmSfJOcEEUfBb169ap45513hCRJYvz48eXZzHKzdetW4eDgIF/3tmPHDrXrXlWfhf379wsnJ6dK9VlQSUlJKbBTXNjfj7t374oJEyYISZLERx99VF7N0wgfA0NISkrC1atXcfLkSRw9ehS5ublo2LAhGjdujNGjR+u6eVqletCvEAJKpfKFj3WYOHEiVqxYgVOnTlXq5+ABwO+//45169YhJCREfuyFJEkQQsDExATjx4/H1KlTDfoBsBMmTMDKlSsr5edB/P9H3Dx9+hQbNmzAokWLkJiYCCMjI7Rq1Qrt27eHj48PbG1tcerUKSxfvhypqakICwtDs2bNdN38cvH898ZXX32F2bNnV8rPA5D3oPjdu3dj6dKlOHv2LADA3t4enTp1Qvfu3WFqaoqLFy9i/fr1MDU1xcGDB9G0aVMdt7r8PP95mDVrFubOnVthPg8MgAbi4cOH+Ouvv3D16lWkpaXB09MTbm5uqFGjRoEQlJmZqfa8I1HJnvtWUikpKRg3bhzCw8ORkJCg6+aUicKCcEJCAsLDw3H8+HGYmJjAyckJbm5u6NOnjw5bqnvp6ekYP348Dhw4gIcPH+q6OVr3/O/5s2fPEBgYiM2bNyMqKqpA/SZNmmDatGl4++23y7OZZUr1wHvVjmJhVON09epV9OnTBzk5Obh+/Xo5t7R8CSHw559/Ys2aNTh48CBycnLUlrdt2xbTp0/HG2+8oaMW6t6NGzfQv39/pKam4ubNm7puTokwABqAoKAgfP311wW+xKtVq4auXbvCz88Pffr0gYmJibysss38ARQdgvM/zPf5L/7MzEw8fPhQbdaQiq40P9vnx6My7Qy87Gc8JSUFNjY2ZdAi/RUXF4dDhw7h4sWLcHR0hL29PV5//XXUr19f103TmStXrqB///7o06cPvvnmG103p0yIvMvE1H5PkpOTERERgRs3bsDJyQlWVlZo06YN7O3tddhS3bt58ybGjRuHTp064csvv9R1c0qEAbCSi4+PR+fOnZGeno6RI0fCx8cHN27cwLlz5/C///0PFy5cQGZmJpo0aYKAgAAMGjQIVapUqVR/6IHiQ3C3bt3kEFyZZnUoiaJCUP45kp+fLaYyKkkYzMnJgSRJlXI2iODgYFy8eBHnz5+Hg4MDWrdujfr168PZ2RnVq1dX2zmsrPKPgb29Pdq0aYP69evDxcUF1atXV5sJJr/K9vtR1NHP/DMkGYLijgKXxft0ohyvNyQd+PLLL4WdnZ3YvXt3gWXx8fFix44d4u2335ZvAFi0aJEOWlm24uLiRL169YSDg4OYOnWqCA4OFitXrhRjxowRnp6e8mNeXnvtNbF161b50TBF3ShSUSUkJIgpU6aI4OBg8eTJE7VlSqWy0j3Bvygch/88efJE/N///Z+QJEntRjBJkkT16tVF3759xcaNGws82qMyjVFJx+D5z0pxj8epiAqbEKCw78D85S96NExFVNJxeN7zjxSrCBgAKzkvLy/RuXNnkZiYKIQQane45hcWFiZatGghTE1Nxfr168u7mWWKITjPzJkzhSRJ4pVXXhG9e/cW3377rYiJiSkws4fqcR9CCBEeHi6CgoJ00dwyw3H4zzfffCMsLCzEgAEDRHh4uLhy5YrYvn27mDNnjnjzzTflKQBbtmwp9uzZo+vmlgmOQZ6VK1eKIUOGiH379hV4rmNubm6l2yEuiiGNAwNgJZaamiq6desm3Nzc5Pks8394n9+zOXv2rLCzsxN9+/aVl1cGDMF5PDw8RJUqVYS3t7f8mB9XV1fx9ttvi3Xr1ol//vlHrX56erro27evUCgUao8Bqeg4Dv9xcXERvXv3FklJSQWW3b17V+zbt0+MHTtWPjK2du1aHbSybHEM8ri6usoPvvfy8hIzZswQUVFRBf4OqI74paeni++++06EhYXporllxpDGgQGwklM9pb6wQJP/A60Kgv369RMNGzYUt27dKrc2liWG4DxxcXHC1dVVtGrVSmRlZYmoqCgxY8YM4e7uLiRJEkZGRqJ58+ZiwoQJYufOnSI5OVnExMQIR0fHSjXlGcfhP//884+wsrISAQEBcllhRzgyMzPF/v37Rb169US1atUq1UwwHIM8Fy9eFJIkidatW4vu3bvLZ0OsrKyEr6+v+P777wvsGB09elRIkiTat2+vo1Zrn6GNAwNgJXfnzh15WrOJEyeKM2fOFDiKodqTSU5OFoMHDxZ169bVRVPLjKGHYCGEiI6OFtWqVRMjRowQQgh55pMHDx6IoKAg8cEHHwgXFxchSZKwsLAQHTt2lOdGfn6auIqM4/Cfv//+W9SpU0f4+fkJIfK+B57fOcr/+/H7779XukskOAZ5fvnlFyFJkli6dKkQIm8WpEWLFgkPDw85BNWqVUsMGzZMbN68WTx+/FgsWbKkwkx5VlKGNg4MgAZgz5498jQ1rVu3FnPnzhXh4eHi1q1bamFwy5YtombNmpVuQm+G4Lzpzt566y2xdevWQpdnZWWJW7duiZ9//lkMGTJEVKtWrUJNaVRSHAd1Xl5ewtraWhw4cKDAMlXwUQWiR48eiVdeeUUMGjSoXNtY1jgGQqxevVpIklToGMTExIjJkycLZ2dnOQQ1bNhQODo6Cltb2/JvbBkytHFgAKyknj91+ejRI/HZZ5+JunXryvP/dunSRbzzzjti7Nix4t133xWmpqbCzc1NXL58WUetLjuGHoKFyJuvs7DrnPJT/aFbtWpVhZrSqDQ4Dv99P0RHR4vatWsLSZLEpEmTRHR0dIGdI9XNMSdOnBBOTk7i448/Lvf2lgWOQR6lUimioqLE5MmTxbVr19TK88vIyBD79u0TI0aMELa2tkKSJDFhwoTybm6ZMcRxYACsxFQf3Pj4ePkP2l9//SUWLFggfH195TAoSZKoVq2a6NKlS4EJ4CsyhuA8hV3HqDr1WZTPP/9cSJIkzpw5U5ZNK1cch4JycnLEpk2bRK1atYQkSaJp06Zi8uTJ4tdffxWXLl2Sx+bOnTti2LBhwtjYuNKNBccgT2pqapGPMnn+d2f8+PFCkiRx7ty5cmhZ+TKkceCDoCuhnJwcHD9+HBs2bMDVq1chSRIsLCzQpk0bDBkyBC1atIAQAvHx8cjIyMCNGzfg5uYGZ2dnGBsbV6qHQKv6cufOHTg5OUGhUODixYvYt28fIiIi8M8//yA+Ph4AYGdnBw8PD/zwww+Vbj5L1TgkJCTA3t5e7WGu+R/6DAB37txB7969ce/ePSQmJuqqyWWC41C4xMRELF++HDt37sTVq1dhYWGB2rVrw8rKCtWqVcPly5eRmJiIUaNGYeXKlbpubpngGBRP9btz/fp1+Pn5ITk5GbGxsbpuVrmrTOPAAFgJLV68GHPnzkVqairq168PIyMjXLlyRV7epEkTfPTRRxg0aFClnb6HITjP8+OgUChgbm4Od3d3DBw4EO3atSvwnqSkJPz8889wcnKCn5+fDlqtfRyHwol8c0FnZGQgNjYWp06dwvHjxxEdHY3Lly+jZs2acHZ2xvvvv4933nkHlpaWum62VnEMSmffvn3o27cvPv/8cyxatEjXzdGZSjEOOjjqSGXoxo0bwtLSUnTo0EHcuHFD3LlzR2RnZ4v4+HixcuVK4ePjI5/27dKlizh16pSum1wmvv32W2FjYyMkSRINGjQQbm5uak/4b9q0qVixYoV48OCBrptapl40Do0bNxZLly4V9+/fV3tfZmZmpXrgKceh5HJzc0V6errIzs4WSUlJleqykJIyxDEo6SOvEhISxKZNmwrMDlNZGNI4MABWMjNmzBD29vbi0KFDctnzH+gLFy4If39/YWZmJho1aiROnz5d3s0sUwzBeUozDl27dq2U1zUJwXHI799//xWXL18W//77b4Flubm5at8Vz39vVJYgzDHIU9w4vEhlmgbPkMeBAbCSeeutt0S9evXE7du3hRD/Pd5EqVQW+LAuW7ZMSJIkRo4cWe7tLEsMwXk0GYfK8gBsITgO+S1YsEC0bt1azJ8/X4SFhYm7d+8W+F54/tl3Dx8+rFTzvXIM8pRkHJ7HcchTWcaBAbCSmTt3rpAkSVy6dKnIOvm/2AYOHCjq1q0rrl+/Xh7NKxcMwXk4Dnk4Dv9RPe7E2NhYVK9eXfTp00f8+OOPIiYmptBH46SlpYnPPvtMjBo1qtIc/eIY5NFkHCr6ka/8DHkcGAArmWPHjglJkoSHh4c4fPhwobez5//DFxAQICwsLMT//ve/8m5qmWEIzsNxyMNxyHPlyhVhZWUl2rVrJ5YvXy769esn7O3thSRJwsXFRYwYMUL8/PPP4uLFi+LJkydCCCFOnjwpbG1tRb9+/XTadm3hGOThOOQx9HFgAKxkcnJyxKeffipf2L58+XKRkJBQaN3Hjx8Lf39/UbNmzXJuZdliCM7DccjDccjz559/CmNjYzF79mwhhBC3bt0SISEhYvbs2aJjx47CyspKGBsbi+bNm4tJkyaJ4OBg+TmIFXGaq8JwDPJwHPIY+jgwAFZSq1atEq+++qqQJEnUrl1bTJgwQezfv19cuHBBXLp0Sdy9e1d88cUXwszMTEyZMkXXzdUqhuA8HIc8HIc8v/76q5AkSezYsUOtPCsrS8TGxopdu3aJTz75RLi7u4sqVaoIS0tLYWFhUammweMY5OE45DH0cWAArKSUSqW4evWq+Pzzz9XmLnRwcBB16tQRRkZGQpIkMXz4cBEfH6/r5pYJQw7B+XEc8hj6OCiVSvH333+LGzduyK+fl5aWJs6ePSt++eUX0aNHD3n+7MqCY5CH45DH0MeBAdAApKWlibCwMDFp0iQxZMgQ0blzZ9G3b1+xZcuWAnNeViYMwXk4Dnk4DkUr7A/fxIkThSRJ4uzZszpoUfnjGOThOOQxhHHgTCAGJjs7GyYmJrpuRrlLT09HTEwM/vjjD9y7dw8PHz6EjY0NhgwZgoEDB8LMzEzXTSwXHIc8HIfCKZVKKBQK3Lp1C/369cOTJ08QFxen62aVK45BHo5Dnso8Dsa6bgCVL0MMfwBgaWkJHx8f+Pj4GGwIBjgOKhyHwqnmRr579y6ys7Px0Ucf6bhF5Y9jkIfjkKcyjwOPABIRkRohBO7cuYNq1aoZ7Ly3HIM8HIc8lXEcGACJiIiIDIxC1w0gIiIiovLFAEhERERkYBgAiYiIiAwMAyARERGRgWEAJCIiIjIwDIBEREREBoYBkIiIiMjAMAASERERGRgGQCIiIiID8/8A1pHyGHEj4LkAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 700x500 with 1 Axes>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "backend = Aer.get_backend('qasm_simulator')\n",
    "grover = Grover(quantum_instance=backend)\n",
    "problem = AmplificationProblem(oracle)\n",
    "result = grover.amplify(problem)\n",
    "plot_histogram(result.circuit_results)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "The result shows that the assignments $000, 101, 110$ for $x_1 x_2 x_3$ are potential solutions to the problem.  \n",
    "Whether these are correct solutions to the problem can be verified efficiently, as 3-SAT is in NP.\n",
    "Note that the variables in the histogram are in reverse order: $x_3, x_2, x_1$ instead of $x_1, x_2, x_3$.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Classical brute force algorithm\n",
    "\n",
    "The solutions to the problem can also be derived with a classical (non-quantum) algorithm by simply trying every possible combination of input values $x_1, x_2, x_3$of $f$.\n",
    "\n",
    "We find again, that the solutions for the given 3-SAT problem are the assignments $000, 101, 110$ for $x_1 x_2 x_3$.  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "scrolled": false,
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<table>\n",
       "<thead>\n",
       "<tr><th style=\"text-align: right;\">  $x_1$</th><th style=\"text-align: right;\">  $x_2$</th><th style=\"text-align: right;\">  $x_3$</th><th>$f$  </th></tr>\n",
       "</thead>\n",
       "<tbody>\n",
       "<tr><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      0</td><td>True </td></tr>\n",
       "<tr><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      1</td><td>False</td></tr>\n",
       "<tr><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      0</td><td>False</td></tr>\n",
       "<tr><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      1</td><td>False</td></tr>\n",
       "<tr><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      0</td><td>False</td></tr>\n",
       "<tr><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      0</td><td style=\"text-align: right;\">      1</td><td>True </td></tr>\n",
       "<tr><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      0</td><td>True </td></tr>\n",
       "<tr><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      1</td><td style=\"text-align: right;\">      1</td><td>False</td></tr>\n",
       "</tbody>\n",
       "</table>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "from IPython.display import HTML, display\n",
    "import tabulate\n",
    "\n",
    "nbr = 3 # number of Boolean variables in Boolean function\n",
    "\n",
    "table = []\n",
    "for i in range(2**nbr):\n",
    "    x1, x2, x3 = [int(x) for x in '{0:03b}'.format(i)] # Boolean variables\n",
    "    \n",
    "    # define clauses \n",
    "    c1 = [not x1, not x2, not x3] # -1 -2 -3\n",
    "    c2 = [    x1, not x2,     x3] #  1 -2  3\n",
    "    c3 = [    x1,     x2, not x3] #  1  2 -3\n",
    "    c4 = [    x1, not x2, not x3] #  1 -2 -3\n",
    "    c5 = [not x1,     x2,     x3] # -1  2  3\n",
    "    \n",
    "    f = all([any(c1), any(c2), any(c3), any(c4), any(c5)]) # Boolean function\n",
    "    table.append([x1, x2, x3, f])\n",
    "    \n",
    "display(HTML(tabulate.tabulate(table, tablefmt = 'html', \n",
    "            headers = ['$x_1$', '$x_2$', '$x_3$', '$f$'])))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "Remark: this is obviously not the most efficient classical algorithm that exists. Heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols, which is sufficient for many practical SAT problems."
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "celltoolbar": "Slideshow",
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.13"
  },
  "latex_envs": {
   "bibliofile": "biblio.bib",
   "cite_by": "apalike",
   "current_citInitial": 1,
   "eqLabelWithNumbers": true,
   "eqNumInitial": 0
  },
  "livereveal": {
   "autolaunch": true
  },
  "nav_menu": {},
  "toc": {
   "navigate_menu": true,
   "number_sections": true,
   "sideBar": true,
   "threshold": 6,
   "toc_cell": false,
   "toc_section_display": "block",
   "toc_window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}