3sat-v2.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "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 [\n",
    "Using Grover search for boolean satisfiability](https://github.com/JavaFXpert/qiskit4devs-workshop-notebooks/blob/master/grover_search_party.ipynb) by [James Weaver](http://twitter.com/JavaFXpert).\n",
    "\n",
    "Implemented by [Jan-R. Lahmann](http://twitter.com/JanLahmann) using Qiskit, binder and RISE."
   ]
  }, 
 
  
  
  
  {
   "cell_type": "markdown",
   "metadata": {
    "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": {
    "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": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Solving 3-SAT using Qiskit Aqua and Grover's search algorithm\n",
    "### Throwing a party while avoiding the drama\n",
    "\n",
    "Imagine you are inviting some friends to a party, some who are couples, and some who are not on speaking terms. \n",
    "\n",
    "Specifically, **Alice** and **Bob** are in a relationship, as are **Carol** and **David**. However, **Alice** and **David** had a bad breakup a while ago and haven't been civil with each other since. \n",
    "\n",
    "Armed with a quantum computer and Qiskit Aqua, how can you leverage Grover's quantum search algorithm to identify friendly combinations of people to invite?\n",
    "\n",
    "The constraints for our party planning problem may be formulated with the following boolean expression:\n",
    "\n",
    "        ((A and B) or (C and D)) and not (A and D)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "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": 1,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Import the necessary functions from Qiskit and Qiskit Aqua\n",
    "from qiskit import BasicAer, qiskit\n",
    "from qiskit.aqua.algorithms import Grover\n",
    "from qiskit.aqua.components.oracles import LogicalExpressionOracle\n",
    "from qiskit.tools.visualization import plot_histogram"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "Let's go ahead and use our expression in a Grover quantum search to find out compatible combinations of people to invite.\n",
    "\n",
    "Note: We'll represent and with \"&\", or with \"|\", not with \"~\" in our expression."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Define the formal logical expression corresponding to our \"party problem\"\n",
    "log_expr = '((A & B) | (C & D)) & ~(A & D)' "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "Let's run the algorithm on a quantum simulator and plot the result.\n",
    "\n",
    "Each basis state represents our four friends, with the least significant bit representing Alice. If a bit is 1, then the advice is to invite the person that the bit represents. If the bit is 0, then Grover advises not to send an invitation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAc0AAAFLCAYAAAC0rNfYAAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADh0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uMy4xLjEsIGh0dHA6Ly9tYXRwbG90bGliLm9yZy8QZhcZAAAgAElEQVR4nO3deXxU5dn/8c9FECQIaCTFRKGAUIwbBpBNELe4i5Qibk+pduFRK+oPLX2qPuJupVKXFpfSuoDFGitoRXlKMVVEEStSRMG4AEEIWAmIFMSEeP3+OCfpEBI4A8nMJPN9v155OXOfeybX4TZzzX3OvZi7IyIiIrvXLNkBiIiINBZKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRNU92AMl04IEHeqdOnZIdhoiIpJB//vOf6909u7ZjaZ00O3XqRFFRUbLDEBGRFJKVlVVS1zFdnhUREYlISVNERCQiJU0REZGIlDRFREQiUtIUERGJSElTREQkIiVNERGRiJQ0RUREIlLSFBERiUhJU0REJCIlTRERkYiUNEVERCJS0hQREYlISVNERCQiJU0REZGIlDRFREQiUtIUERGJSElTREQkIiVNERGRiJQ0RUREIlLSFBERiUhJU0REJCIlzSSZM2cOffv2pXfv3tx33307HZ80aRL9+/dn0KBBDBs2jE8//bT62OrVqxk+fDj9+vWjf//+rFq1CgB35/bbb+fYY4+lX79+PPLIIwk7HxGRdNA82QGko8rKSsaNG8f06dPJzc3l5JNP5vTTT+ewww6rrnP00UdTVFREZmYmjz76KOPHj+fRRx8F4PLLL2fs2LGceOKJ/Pvf/6ZZs+C7z7Rp01izZg0LFiygWbNmfP7550k5PxGRpko9zSRYuHAhXbp0oXPnzrRo0YLhw4cza9asHeoMHjyYzMxMAPr06UNpaSkAH3zwAdu3b+fEE08EYL/99quu99hjj/Gzn/2sOolmZ2cn6pRERNKCkmYSrF27loMPPrj6eW5uLmvXrq2z/pNPPskpp5wCwCeffEK7du0YNWoUQ4YM4aabbqKyshKAFStWMGPGDE466STOO+88Pvnkk4Y9ERGRNKOkmeIKCwtZtGgRY8aMAWD79u3Mnz+fW2+9lZdffpmVK1cybdo0AMrLy2nZsiVFRUWMGjWq+jUiIlI/lDSTICcnhzVr1lQ/Ly0tJScnZ6d6r7zyChMnTmTatGm0bNkSCHqlRx11FJ07d6Z58+acddZZvPvuu9XHzjnnHADOPvts3n///QScjUjDaohBc5MnT6Z3795kZWVRVlaWsHORxk9JMwl69erF8uXLKSkpoby8nOnTp3P66afvUOfdd99l7NixTJs2bYd7k7169WLTpk2sX78egLlz59KjRw8AzjzzTF577TUAXn/9dbp165agMxJpGFWD5goLC5k/fz7PPvssH3zwwQ51qgbNzZs3j6FDhzJ+/PjqY5dffjljxoxhwYIFzJkzh/bt2wPQr18/ZsyYQceOHRN6PtL4afRsEjRv3pwJEyYwYsQIKisrufjii8nLy+POO+8kPz+fM844g/Hjx7NlyxYuvfRSAA455BCmTZtGRkYGt956K8OGDcPdOeaYYxg1ahQA11xzDaNHj+ahhx6idevW3H///ck8TZG9FjtoDqgeNBc70nzw4MHVj/v06UNhYSFQ+6C5KkcffXQCopemSEkzSQoKCigoKNih7Prrr69+PGPGjDpfe+KJJzJv3rydytu1a8fTTz9df0GKJFltg+YWLlxYZ/26Bs2VlJQwZMgQxo8fT0ZGRoPHLU2XLs+KSJMQz6A5kT2lnqaIpKx4B83NnDmz1kFzAGeddRZvv/12QuKWpks9TRFJWQ01aE5kTylpioT2ZmpD+/btOf744zn++OO56KKLqstHjx5N3759GThwIFdeeSUVFRUJOZemInbQXP/+/Rk2bFj1oLmqVbRiB83F/vvHDpo77rjjAKoHzT3yyCMcccQRlJaWMnjwYK666qrknKA0OubuyY4hafLz872oqCjZYUgKqKys5Nhjj91hPeDJkyfvMErztddeo3fv3tXrAc+bN696PeCOHTvukESr/O1vf6semPKTn/yEgQMH8sMf/jAxJyUieyQrK2uhu/ep7Zh6miLs3XrAu1JQUICZYWb06tUr0mtEJHUpaYqwd+sBA2zbto2TTjqJgoICXnzxxZ3qV1RUUFhYyMknn1y/gYtIQmn0rEicqqY2zJw5s7ps8eLF5ObmsnLlSs4991wOP/xwunTpUn38uuuuY8CAAQwYMCAZIYtIPVFPU4S9Ww8Ygp4pQOfOnRk0aFD1esAAd999N2VlZdxxxx0NeAYikghKmiLs3dSGL774gq+//hqAsrIyFixYUD21YcqUKRQVFTF58uTqfU5FpPHS5VkR9m494OLiYsaOHUuzZs345ptvuPrqq6tH3V577bV07NiR0047DQh2nxk3blzSzlNE9o6mnGjKiYiIxNjVlBP1NOvBuCcOSHYI9WbCDzYmOwQRkZSlmywiIiIRKWmKiIhEpKQpIiISke5pikjC6P6/NHbqaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIRJqnKU2S5gOKSENQT1NERCQiJU0REZGIlDRFREQiUtIUERGJSElTREQkooQnTTO7wsxWmNk2M1toZoN3UXe4mc02s8/NbLOZLTCzobuof6GZuZnNbJjoRUQknSU0aZrZ+cD9wJ1APvAGMMvMOtXxkiFAEXBWWP8lYEZtidbMugK/Al5rgNBFRCQ0Z84c+vbtS+/evbnvvvt2Oj5p0iT69+/PoEGDGDZsGJ9++ikAS5Ys4dRTT2XAgAEMGjSI6dOnV79m9OjR9O3bl4EDB3LllVdSUVGRsPOJR6J7mmOBx919srsvc/cxwFrg8toqu/vV7v5Ld3/L3T9291uAhcCw2Hpmtg/wFHADsLxhT0FEJH1VVlYybtw4CgsLmT9/Ps8++ywffPDBDnWOPvpoioqKmDdvHkOHDmX8+PEAtGrVioceeoj58+fzzDPPcMMNN7Bp0yYAzjvvPBYsWMDrr7/Otm3bmDp1asLPLYqEJU0zawH0BmbXODQbGBjHW7UBas72vgNY6e5P7HmEIiKyOwsXLqRLly507tyZFi1aMHz4cGbNmrVDncGDB5OZmQlAnz59KC0tBaBbt24ceuihAOTk5NC+fXvWr18PQEFBAWaGmdGrV6/q16SaRK4I1B7IAD6rUf4ZcEqUNzCznwKHAFNjyk4FRgLHRHyP0cBoCBrtnXfeASA3N5fMzEw+/vhjANq1a0fXrl1ZtGgRABkZGfTs2ZPi4mK2bNkCQF5eHhs2bACazuozVf8eXbt2pby8nNWrVwPQoUMHsrKyWLZsGQCtW7emR48eLF68mMrKSgDy8/NZvnx59TfHbt26sXXr1ur/+XNycmjbti3FxcUAtGnThu7du7No0SLcHTMjPz+fjz76iM2bNwPQo0cPvvzyS9auXQtEb6emZMmSJdWXqnr27MmqVavYuDH43tjY2qkpqfpbadWqFXl5eU2qnXb1uVdSUsIBBxxQff777bcf7733XvXzAw44gE6dOrF48WIguFR7yimnsGzZMr766isADj/8cIqKiti8eTMbN26krKwMM2PlypVs376dJ598kl/+8pfV79myZUuOOOII3n//fb7++msAjjzySNauXUtZWRkAnTt3xt0pKSkBIDs7m+zsbJYuXRp3O+2KufsuK9QXM8sF1gBD3H1uTPlNwMXu3mM3r/8eQbI8391fCMuygcXAhe7+alj2ONDe3c/eXUz5+fleVFS0h2f0H1qyLfWoTVKT2qXxe/7553n55Zd54IEHAHj66adZuHAhEyZM2KluYWEhkydPZubMmbRs2bK6fN26dQwdOpRJkyZx7LHH7vCaq6++mszMTO66666GPZFdyMrKWujufWo7lsie5nqgEuhQo7wDsG5XLzSzEcAUYFRVwgwdAeQAL5tZVVmz8DXbgSPcvXjvQxcREQh6uGvWrKl+XlpaSk5Ozk71XnnlFSZOnLhTwvzyyy+54IILuOGGG3ZKmHfffTdlZWXce++9DXcCeylh9zTdvZxgEE9BjUMFBKNoa2VmIwl6mJe4+59rHP4HcBTBpdmqn78QjKA9BlhRL8GLiAgAvXr1Yvny5ZSUlFBeXs706dM5/fTTd6jz7rvvMnbsWKZNm0Z2dnZ1eXl5OaNGjeL888/n3HPP3eE1U6ZMoaioiMmTJ9OsWeouIZDoXU5+DUw1s7eA14HLgFzgYQAzmwLg7qPC5xcQJMzrgLlmdlD4PuXuvsHdtwDvxf4CM/sCaO7uO5SLiMjea968ORMmTGDEiBFUVlZy8cUXk5eXx5133kl+fj5nnHEG48ePZ8uWLVx66aUAHHLIIUybNo3nnnuON954gw0bNvDUU08BwT3Po446imuvvZaOHTty2mmnAXD22Wczbty4pJ1nXRKaNN39aTM7ELiR4LLqe8CZ7l4SVqk5X/MyghjvC3+qvAqc0LDRiohIbQoKCigo2PGi4fXXX1/9eMaMGbW+buTIkYwcObLWY59//nn9BdiAEr6fprs/CDxYx7ETdvU84vtfsidxiYiI7E7qXjgWERFJMUqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhECV8RSEREUoe2a4uPepoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhEcSVNMxtpZqfGPL/JzFab2V/NLKf+wxMREUkd8fY0b656YGa9gOuBB4B9gIn1F5aIiEjqiXdrsG8DxeHj7wLPufsEM5sN/LVeIxMREUkx8fY0twFtwscnA3PCx5tiykVERJqkeHuarwETzWwe0AcYEZZ/B/i0PgMTERFJNfH2NK8EygmS5WXuXhqWn4Euz4qISBMXV0/T3VcD59RSfk29RSQiIpKi4p6naWb7mtkIM/u5me0flh1qZln1H56IiEjqiKunaWbdCAb/7AfsDzwDfAFcHj7/cX0HKCIikiri7WneB8wGOgBfxZT/BTixvoISERFJRfGOnh0I9Hf3SjOLLV8F5NZbVCIiIiloT9ae3aeWsk4EczVFRESarHiT5mxgbMxzN7O2wC3Ai/UWlYiISAqK9/LsWODvZlYM7As8DXQDPgNG1nNsIiIiKSXeeZqlZnYMcCHQi6Cn+jvgj+7+1S5fLCIi0sjF29MkTI6Phj8iIiJpY7dJ08yGAy+4e0X4uE7uPr3eIhMREUkxUXqafwYOAv4VPq6LAxn1EZSIiEgq2m3SdPdmtT0WERFJN3ElQTM73sx2SrRmlmFmx9dfWCIiIqkn3p7j34HaFmbfPzwmIiLSZMWbNI3g3mVNBwJb9j4cERGR1BVpyomZ/SV86MCTZvZ1zOEM4EjgjXqOTUREJKVEnadZFv7XgI3suMNJOTAPmFyPcYmIiKScSEnT3S8FMLOVwD3urkuxIiKSduJdRu+WhgpEREQk1UVZEehdYIi7bzSzJdQ+EAgAdz+6PoMTERFJJVF6ms8CVQN/drUikIiISJMWZUWgW2p7LCIikm60LJ6IiEhEUe5p7vI+Zizd0xQRkaYs6i4nIiIiaS+ue5oiIiLpTPc0RUREItI8TRERkYgSPk/TzK4AfgbkAO8D17j7a3XUzQEmAr2A7sBUd7+klnptgduBEQQ7rnwKXO/uhXsbr4iISJWEztM0s/OB+4ErCBZ5vwKYZWaHu/uqWl7SElgP/BIYXcd77gP8DdgAjARWA4fwn0QvIiJSL+Jae7aKmR0K5IVPl7n7JxFfOhZ43N2rdkQZY2anA5cDv6hZ2d1XAleFv3NEHe95KZANDHb38rBsZcR4REREIotrIJCZHWhmzwEfAc+FPx+a2fNmduBuXtsC6A3MrnFoNjAwnjhqGAa8DvzGzNaZ2VIzuznsgYqIiNSbeHuavwe6AYOBBWFZP+Ahgv00h+/ite0JNqz+rEb5Z8ApccYRqytwEjANOAvoDEwC9gOuq1nZzEYTXurNycnhnXfeASA3N5fMzEw+/vhjANq1a0fXrl1ZtGgRABkZGfTs2ZPi4mK2bAl2RsvLy2PDhg3AAXsRfmqp+vfo2rUr5eXlrF69GoAOHTqQlZXFsmXLAGjdujU9evRg8eLFVFZWApCfn8/y5cvZtGkTAN26dWPr1q2UlpYCwb9327ZtKS4uBqBNmzZ0796dRYsW4e6YGfn5+Xz00Uds3rwZgB49evDll1+ydu1aIHo7NSVLliyhoqICgJ49e7Jq1So2btwINL52akqq/lZatWpFXl5eo22npvT5VVZWRklJCQDZ2dlkZ2ezdOlSIL522hVzj7TYT1DZbCtwsrvPr1E+AJjj7q138dpcYA3BSNy5MeU3ARe7e4/d/O6ZwPqaA4HM7ENgX6CLu1eGZaOBe4H9fBcnmJ+f70VFRbv6tZGMe6Lp/E834Qcbkx1CvVCbpCa1S+pRm+wsKytrobv3qe1YvD3Nz4HaNqDeCpTt5rXrgUqgQ43yDsC6OOOItRaoqEqYoWVAJkHv9vO9eG8REZFq8S5ucCtwn5kdXFUQPp4YHqtTOEhnIVBQ41AB8EacccR6HehmZrHn8h2CRL5+L95XRERkB3uyYHsXYKWZrQmfHwxsA75FcM9zV34NTDWztwiS3WVALvBw+LumALj7qJjff0z4sC3wTfi83N2XhuUPAVcC95vZbwnuad4CPLirS7MiIiLxSuiC7e7+dDjK9kaCxQ3eA85095KwSqdaXraoxvNzgBKC5Ii7f2pmpxIk5H8SXOp9lGCxAxERkXqT8AXb3f1B4ME6jp1QS5lFeM832btpKyIiIrulBdtFREQiindxgxZmdouZfWhm28ysMvanoYIUERFJBfH2NG8DfkAwWvYbgoXXJxFMN7mifkMTERFJLfEmzZHAZe7+CMGcy+fd/SpgPDtPJREREWlS4k2aHYCqqR7/BvYPH/8fcGp9BSUiIpKK4k2aqwjmVQJ8DJwWPh4AfFVfQYmIiKSieJPmDODk8PH9wC1mtgJ4nN0vbCAiItKoxbX2rLv/Iubxn81sNcH8yA/dfWZ9ByciIpJK9mgT6irhogJv1lMsIiIiKS3uxQ3MrJeZTTGzt8OfqWbWqyGCExERSSXxLm5wMfAPgnVjXwp/OgBvmdl/1X94IiIiqSPey7N3AP/r7nfGFprZLwgWSH+yvgITERFJNfFens0GCmspf4ZgazAREZEmK96k+XfghFrKTwBe3dtgREREUlmUTaiHxzydBdxlZn34z6jZ/sBw4OZ6j05ERCSF7Okm1KPDn1i/oY59MkVERJqCKJtQa89NERERtAm1iIhIZHuyuMFZZjbXzNab2edm9qqZndkQwYmIiKSSeBc3+DHBou2fAD8H/gdYAcwwsx/Wf3giIiKpI97FDX4OjHX338aU/cHMFhIk0EfrLTIREZEUE+/l2U4EG07XNAv49t6HIyIikrr2ZBPqglrKTwVK9j4cERGR1BXv5dl7gN+Eu5q8EZYdB3wfGFOfgYmIiKSaeDehfsTM/gVcS7AKEMAyYKS7P1/fwYmIiKSSyEnTzJoTXIad6+4zGi4kERGR1BT5nqa7bwemA20aLhwREZHUFe9AoMVAt4YIREREJNXFmzRvBiaa2TAz62hmWbE/DRCfiIhIyoh39OyL4X+nAx5TbuHzjPoISkREJBXFmzRPbJAoREREGoFISdPMMoFfAcOAfYA5wFXuvr4BYxMREUkpUe9p3gJcQnB59imCVYEeaqCYREREUlLUy7PDgR+5+58AzOyPwOtmluHulQ0WnYiISAqJ2tPsCLxW9cTd3wK2A7kNEZSIiEgqipo0M4DyGmXbiX8gkYiISKMVNekZ8KSZfR1Tti8w2cy2VhW4+9D6DE5ERCSVRE2aT9RS9mR9BiIiIpLqIiVNd7+0oQMRERFJdfEuoyciIpK2lDRFREQiUtIUERGJSElTREQkIiVNERGRiJQ0RUREIlLSFBERiUhJU0REJCIlTRERkYiUNEVERCJS0hQREYlISVNERCQiJU0REZGIlDRFREQiUtIUERGJSElTREQkIiVNERGRiJQ0RUREIkp40jSzK8xshZltM7OFZjZ4N/WHhPW2mdlyM7usxvEMM7st5j1XmNntZta8Yc9ERETSTUKTppmdD9wP3AnkA28As8ysUx31uwAvhfXygbuA35jZ92Kq/Rz4KXAVcBhwdfj8Fw10GiIikqYS3RsbCzzu7pPD52PM7HTgcmpPcpcBpe4+Jny+zMz6AdcBz4ZlA4EX3P2F8PlKM/sL0K9BzkBERNJWwnqaZtYC6A3MrnFoNkHiq82AWur/FehjZvuEz+cBJ5rZYeHvORw4iaCHKiIiUm8SeXm2PZABfFaj/DPgoDpec1Ad9ZuH7wdwNzAVWGpmFcD7wBPu/mB9BC0iIlKlKQyWOR8YBVxEkDCPAe43sxXu/oealc1sNDAaICcnh3feeQeA3NxcMjMz+fjjjwFo164dXbt2ZdGiRQBkZGTQs2dPiouL2bJlCwB5eXls2LABOKCBTzFxqv49unbtSnl5OatXrwagQ4cOZGVlsWzZMgBat25Njx49WLx4MZWVlQDk5+ezfPlyNm3aBEC3bt3YunUrpaWlQPDv3bZtW4qLiwFo06YN3bt3Z9GiRbg7ZkZ+fj4fffQRmzdvBqBHjx58+eWXrF27FojeTk3JkiVLqKioAKBnz56sWrWKjRs3Ao2vnZqSqr+VVq1akZeX12jbqSl9fpWVlVFSUgJAdnY22dnZLF26FIivnXbF3L0BTyHmFwWXZ7cCF7r7MzHlk4Aj3X1ILa+ZCyxx95/GlJ0HTAMy3b3CzD4F7nH3+2Pq3Ahc4u7ddhVTfn6+FxUV7e2pMe6JpvM/3YQfbEx2CPVCbZKa1C6pR22ys6ysrIXu3qe2Ywm7POvu5cBCoKDGoQKC0bG1mV9H/bfdvSJ8nglU1qhTieagiohIPUv05dlfA1PN7C3gdYLRsbnAwwBmNgXA3UeF9R8GrjSz+4BHgOOAS4ALY97zBeB/zGwFweXZfIJRulMa+mRERCS9JDRpuvvTZnYgcCOQA7wHnOnuJWGVTjXqrzCzM4F7CaallAJXufuzMdXGALcBDwLfAtYCk4FbG/JcREQk/SR8IFA4qrXWka3ufkItZa8CvXbxfpuBa8IfERGRBqP7fiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESlpioiIRKSkKSIiEpGSpoiISERKmiIiIhEpaYqIiESkpCkiIhKRkqaIiEhESpoiIiIRKWmKiIhEpKQpIiISkZKmiIhIREqaIiIiESU8aZrZFWa2wsy2mdlCMxu8m/pDwnrbzGy5mV22t+8pIiKyJxKaNM3sfOB+4E4gH3gDmGVmneqo3wV4KayXD9wF/MbMvren7ykiIrKnEt3THAs87u6T3X2Zu48B1gKX11H/MqDU3ceE9ScDTwDX7cV7ioiI7JGEJU0zawH0BmbXODQbGFjHywbUUv+vQB8z22cP31NERGSPJLKn2R7IAD6rUf4ZcFAdrzmojvrNw/fbk/cUERHZI82THUCimdloYHT49N9ZWVnFyYwnDu2B9Q39S37//xr6NzQ5Dd4uapO46W8lNTWmv5Vv13UgkUlzPVAJdKhR3gFYV8dr1tVRf3v4fhbve7r774DfRY46RZjZ2+7eJ9lxyI7ULqlHbZKamkq7JOzyrLuXAwuBghqHCghGvNZmfh3133b3ij18TxERkT2S6MuzvwammtlbwOsEo2NzgYcBzGwKgLuPCus/DFxpZvcBjwDHAZcAF0Z9TxERkfqS0KTp7k+b2YHAjUAO8B5wpruXhFU61ai/wszOBO4lmEJSClzl7s/G8Z5NRaO7pJwm1C6pR22SmppEu5i7JzsGERGRRkFrz4qIiESkpCkiIhKRkqaIiEhESpoiIiIRKWk2EmaWkewYZEdmlmFmluw4RCRxNHq2kTGzZgDu/k0tx8zVoAkXtom5e2WyY5GAmbUBWgP/AjKBrbX9zUjimFkO0Ab4imDN8HXuvi25UcVPSbMRMLM7gHeA2e6+OaY8A/hGiTLxzOwx4E2g0N03xpQ3J2gTfUAniZldBFwK9AqL5gOzgDnuXhzW0RfMBDKzK4AfAkcCFQQrub0JFAGvuvvXjaVNlDRTnJkNAuYCi4F/AwuAF9z91Zg6rYC7gXvcfVVSAk0jMW3yMbAvQZs86e7Px9RpBUwiaJOlSQk0DZnZ8cAUgvZ5CvgWcAFwEkGv85fuPil5EaYfMzsB+CPwJPA40BkYDgwhuBrwODDe3bcnJcA4KWmmODObABwLPE3wLe1IYH+C7c9eAV4guPz0JtAuticqDcPMbidokweB7sAJBO1SDvwNmEqwkcAC1CYJZWaFwBfuPrpGeSYwDhgD3OfutyUjvnRkZtOAze7+3zXK9wF+BNxK0BH4UTLii1fabQ3WCLUHlrv7w+G9s14Em3MfCwwFvgt0Af5PH84J0xpYC7zo7tvN7FmCpDkAGAT8CTgYmKU2SbgWBF9YADCzlgSXy7cCN4d/QxeY2VR3X5mkGNNNOZBlZvu6+zYz2xfY7u4VwMNmVgH8zMyOcPf3kxvq7qmnmeLM7CDgMHd/pUZ5O4IEeiLBurtnu/tLiY8w/ZjZfkSljAkAAAkLSURBVMCR7v5mjfJWBF9gBhKss6k2STAzuxh4ADjH3d+IKc9w90ozyyK4n3aRu89PVpzpxMxOI7g8e4W7F8aUNw+/dLYGlgHfj73tlKqUNBuZ8JuyV90wN7NzgKfcfb/kRpa+ag5gMLOhBAOE9k1iWGknnP7TGpgMnAG8BDwLvOzuX4R/O+cDv3P3NsmLNH2EbdISuJPg0vjbwBPAM+5eZmbtCa6Y3efubZMXaXRKmo1Y+CHwIJDl7iOTHY9Uf0jcAnSoeQ9HEiPsuVwKnEswEGg7sIlgmkMH4E/ufnPSAkxTZnY2cBGQD2QTjMvYTpBUf+/u9yQxvMiUNFNcOK3E65rCEB5v4+5fJDay9LW7aSXhl5nWup+ZHGbWMpzCcBBwPHAE0JHgw/m3wMJwA3tJgNgrMeFczcMJtoHsQjD6/FHgo8Yyz1lJM0WZWW93X1ijTPMyk8jMBrn7vBplOyRQM2umOZqJZ2Z5wFiCXsxyYAXBpvRz9YUy+RrLHMwotIxeCjKz7sA/zOw9M/u1meUDuHulu7sF9jGzvmbWIsnhpgUzOwyYa2abzexPZnYcgLtvd/dvwjZpAZxlZh2SG216MbNDgeeAHgRTfvYhmAN4G/AHMzslieGlJTPrYGbfDwdeEdPTbFa19GS4DGXLZMa5J5Q0U9OFwCcEHwD9gZlm9qaZjTOzjuH/gN8imJv5rSTGmU6GEywwcSfBdJJXzWydmd1jZoeGbbI/8DzBtAdJnOuAD4Gz3P0X7v5dgvuZ9xLcO/uLmTWKOYBNyI0EA34+NrNnzOzM8LJ57JWyg4ExjS1x6vJsCjKzPwLrgbuAA4E+wGCgL5AFLAIM6OLuRyQrznRiZpMAB24Ki44ETieYJ9sDeI+gzTqoTRLLzF4C/uHu48NbGMTeHzOzicBxwEnhfE1pYGY2n2DxlQ+Biwk+v8oIRjM/5u7vmNltwIXu3i1pge4BLW6QYsJ7ZC8C33b3dcA64H0ze4Hgw7k3weCGEcBPkhZoGgk/iF8EOrv7hrB4rpm9CTwMHE3Qs/lR+COJ9VfgWjN7yt0/AKi6bREO+PkDwZWCfsDfkxZlmjCzXGA1sMLdHzOzqUA3gr+RC4ErzGwp0BW4PnmR7hn1NFOcme0TrpwRWzYc+DOwn745J15tg33CCdyzUJsknJl1AaYTXB6/zd0frXH8SIIND/ZX2zS8cMrPScC/3H1BjWOZBFdpriP4ItPG3b9KfJR7Tj3NFFPzA7kqYYY90MrwfsBAglGB+gBIgHDgglW1Sx2jYwcAf1ObJJ67r7Bgofa7gIlm9gAwG5hD8AE9iGBuptomAdx9C8Ga2MCOI2fDNnjLzLYC8xtbwgT1NFOOmR1CcCnDgG+A4vAybdVxI7jMscbd/5GcKKUmC3Zy+LwxrJ3ZlIR/D83CJfL2BY4iuH1xEsEykysIdteYHvt3JA2n5qpltRxvRTBg7iF3n5HQ4OqBkmYKMbPLCfac6wlsIdh6ajXBKNnnPNwLUBLHzFo1xm/D6Sx2PrOZtXP3TcmOSf7Dgt1N+jTWtX815SRFmNmBBNMZngdyCC73PUGwY8Mo4AEzOzysm5GsONOJmR0AFJvZQ2Z2XNX8svBY7OM8M9s/KUGmqXCe8ndqm64QO3JWCTNxdtUmsdy9orEmTFDSTCUXAR+6++3uXubuH7j7b919BPDfBHtmzjSz9o1luakm4L8I1irtTbjptJndamY9YiZrdwSmEUwFksT5KcHUq4fN7BwzOyj2y2TYy2xrZmeEPRtpeLtsE4CwTc5qzIuyKGmmjnKgTTjSDzNrGTNsfh7BXKdtwKnJCzHtHA08BpxNsDxbIcGQ+aXhYhOjCRJrd3dfnrww09L5wFsE9/+fA+YDvzKzQRZsmwfBF9HxNUefS4OJ2ib/25jX/lXSTB1/Jhj4c42ZtXH3r929PLypjruvAr4ADklmkOkivMS0FPjU3f/l7u+6+y8IFpo4LTx2M3AHcHfSAk1DZpYNVACT3X0w8G2CuZhnE1wRKDKznwPXAAvqfCOpN+nUJhoIlAJi7o+dC9xPcKmvkGDbr0UEifJ44CHgKNeO8wkRJs4D3H2d1bLbTDhitgjo5O6rkxRm2rFgp4wLgKXu/tcax/KBH4fHDwA6uvuaxEeZXtKpTZQ0U0g4mKQTwTzM7xIs/QXBqkAGTHXtA5gQVXPLzKwrsMXdP6vl2E3AJe7eNXmRpqdw2oK7+7bYQVkx95rvAM509/xkxZhu0qVNtLhBkpnZt4DvA9cSrF36FcFl2HnAPQQ7NnQD/s/dP0xWnOmkqk3MbCzwL2C7ma0FniGY77cl/FBYB1yVxFDTlrt/VfXBXHM+YLjqzPcI7kdLgqRLm6inmWRm9jjBJrkvABsILs0eBXyH4AP7xppLUUnDqqNN8oHDCObN/srdZyctwDRmZm2BzXVNnA/r7EswKOWpxjzgpLFItzZR0kyi8FvZZoJLFnNjyjoRLC79Y4JFjUe6+ztJCzSN7KJNDiHYpu0nBIMcLlSbJJ6ZPUIwQvMtoMTdv6ylzv6ujacTJt3aRKNnk+twgmW+qr95eaDE3QuBcwgu1Z6XpPjSUV1t8qm7P0MwGnAzapOEM7MLCb60TCRYBORXZvZdMzs0vJ9WdV/tiaqpW9Kw0rFN1NNMovB/ppkECxeMAj6puRi4mY0BfuTuxyQhxLSjNkldZjaZYIWsCQQ7ZPwAOBQoBl4CXibYPu9+d2+0k+cbk3RsE/U0kyhc0/QGoBUwBRhlZh3NbD+ovnk+hGCDY0kAtUlqsmCXnxXAF+6+3N3vcfejgGOBVwk+rAuB3wBTkxdp+kjXNlFPMwWEly3+FxhKsFD7fOBz4BRgLfBjd1+SvAjTj9ok9ViwFnAHd/8gXC2rInbwiZmdDzwF9HL3fyYrznSSjm2ipJlCwqkOZwHDCJbMew94xsPd6CXx1CapLVwxyzzYGuwnBJcBM5MdVzpr6m2ipJmirMZm1JJ8apPUFs6rzXD3XyU7Fgk0xTZR0hSRJiHczaRSX2xSR1NsEyVNERGRiDR6VkREJCIlTRERkYiUNEVERCJS0hQREYlISVNERCQiJU0REZGI/j/Mlr25NkR3+wAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<Figure size 504x360 with 1 Axes>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Run the algorithm on a simulator, and print a histogram of the result\n",
    "# The logical expression can automatically be transformed into a form suitable for Grover's algorithm\n",
    "backend = BasicAer.get_backend('qasm_simulator')\n",
    "algorithm = Grover(LogicalExpressionOracle(log_expr))\n",
    "result = algorithm.run(backend)\n",
    "plot_histogram(result['measurement'])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "The result shows that the assignments 0011, 0111, 1100, 1110 for David-Carol-Bob-Alice are potential solutions to the problem.  \n",
    "Whether or not 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: David-Carol-Bob-Alice instead of Alice-Bob-Carol-David.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Now it's your turn to play!\n",
    "\n",
    "Create and implement your own scenario that can be modeled as a boolean satisfiability problem using Grover search. Have fun with it, and carry on with your quantum computing journey!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Define the formal logical expression corresponding to our \"party problem\"\n",
    "log_expr = '((A & C) | (B & D)) & ~(A & D)'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Run the algorithm \n",
    "algorithm = Grover(LogicalExpressionOracle(log_expr))\n",
    "result = algorithm.run(backend)\n",
    "plot_histogram(result['measurement']) # print a histogram of the result"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'qiskit': '0.10.5',\n",
       " 'qiskit-terra': '0.8.2',\n",
       " 'qiskit-ignis': '0.1.1',\n",
       " 'qiskit-aer': '0.2.1',\n",
       " 'qiskit-ibmq-provider': '0.2.2',\n",
       " 'qiskit-aqua': '0.5.2'}"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Print Qiskit version \n",
    "qiskit.__qiskit_version__"
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "celltoolbar": "Slideshow",
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "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
}