algorithms/grover/3_sat_grover/3_sat_grover.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "db29ba85",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "tags": []
   },
   "source": [
    "\n",
    "# Demo: Solving 3-SAT Using Grover's Algorithm\n",
    "\n",
    "Grover's algorithm [[1](#Gro97),[2](#GroWiki)] is a quantum search algorithm that enables searching a dataset of $N$ items using $O(\\sqrt{N})$ queries, in contrast to classical algorithms that require $\\Omega(N)$ queries in the worst case. Using the algorithm allows us to speed up various computations that are considered classically intractable.\n",
    "For example, the 3-SAT problem [[3](#3SAT)] is a famous $\\text{NP-Complete}$ problem, a solution of which allows solving any problem in the complexity class $\\text{NP}$.\n",
    "\n",
    "In this demo, we show how the Classiq platform enables us to solve an instance of 3-SAT using Grover's algorithm at a higher functional level, avoiding the implementation details you encounter when using other platforms.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2b14dbae",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## The 3-SAT Formula\n",
    "\n",
    "We now specify the 3-CNF [[4](#CNF)] formula that requires a solution:\n",
    "$$ (x_1 \\lor x_2 \\lor x_3) \\land (\\neg x_1 \\lor x_2 \\lor x_3) \\land (\\neg x_1 \\lor \\neg x_2 \\lor \\neg x_3) \\land (\\neg x_1 \\lor \\neg x_2 \\lor x_3) \\land (x_1 \\lor x_2 \\lor \\neg x_3) \\land (\\neg x_1 \\lor x_2 \\lor \\neg x_3) $$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "dda1a10d-406f-45f2-9431-13df855375de",
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [],
   "source": [
    "def _not(y):\n",
    "    return y ^ 1\n",
    "\n",
    "\n",
    "def sat_formula(x1, x2, x3):\n",
    "    return (\n",
    "        ((x1) | (x2) | (x3))\n",
    "        & ((_not(x1)) | (x2) | (x3))\n",
    "        & ((_not(x1)) | (_not(x2)) | (_not(x3)))\n",
    "        & ((_not(x1)) | (_not(x2)) | (x3))\n",
    "        & ((x1) | (x2) | (_not(x3)))\n",
    "        & ((_not(x1)) | (x2) | (_not(x3)))\n",
    "    )\n",
    "\n",
    "\n",
    "NUM_VARIABLES = 3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "33b41fe0-c901-4f04-9f72-1f2741d25d26",
   "metadata": {},
   "outputs": [],
   "source": [
    "import itertools\n",
    "\n",
    "\n",
    "def print_truth_table(num_variables, boolean_func):\n",
    "    variables = [f\"x{i}\" for i in range(num_variables)]\n",
    "    combinations = list(itertools.product([0, 1], repeat=len(variables)))\n",
    "\n",
    "    header = \"  \".join([f\"{var:<5}\" for var in variables]) + \" | Result\"\n",
    "    print(header)\n",
    "    print(\"-\" * len(header))\n",
    "\n",
    "    for combination in combinations:\n",
    "        result = boolean_func(*combination)\n",
    "        values_str = \"  \".join([f\"{str(val):<5}\" for val in combination])\n",
    "        print(f\"{values_str} | {str(result):<5}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3832b859-65b3-4e94-8e76-cf302eea08ea",
   "metadata": {},
   "source": [
    "We can see that the formula has two possible solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "aa5b8a6e-38ea-468f-bf99-371875f003dc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x0     x1     x2    | Result\n",
      "----------------------------\n",
      "0      0      0     | 0    \n",
      "0      0      1     | 0    \n",
      "0      1      0     | 1    \n",
      "0      1      1     | 1    \n",
      "1      0      0     | 0    \n",
      "1      0      1     | 0    \n",
      "1      1      0     | 0    \n",
      "1      1      1     | 0    \n"
     ]
    }
   ],
   "source": [
    "print_truth_table(NUM_VARIABLES, sat_formula)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "54616eaa",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "We note that since there are multiple satisfying assignments for the formula, the goal of the Grover quantum algorithm is to find one of them.\n",
    "This is contrast to the usual description of the search problem (found in [2](#GroWiki)), in which there is a single solution (out of $N$ possibilities).\n",
    "\n",
    "## Loading the Grover Search Model\n",
    "\n",
    "We load the Grover search model for finding the solution. To specify the model, we define the oracle it uses. Each oracle call is analogous to a classical query. In this case, we define an oracle based on the 3-CNF formula defined earlier, using the standard `phase_oracle` that transforms 'digital' oracle; i.e., $|x\\rangle|0\\rangle \\rightarrow |x\\rangle|f(x)\\rangle$ to a phase oracle $|x\\rangle \\rightarrow (-1)^{f(x)}|x\\rangle$.\n",
    "\n",
    "\n",
    "In addition, we define the number of Grover operator repetitions in the model (which is based on the frequency of solutions in the search space). This time, only one repetition is needed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "4848a14b-956c-4e2b-ad2e-c52e12d0b915",
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [],
   "source": [
    "from classiq import *\n",
    "\n",
    "\n",
    "@qfunc\n",
    "def sat_oracle(x: QArray[QBit], res: QBit):\n",
    "    res ^= sat_formula(*[x[i] for i in range(NUM_VARIABLES)])\n",
    "\n",
    "\n",
    "@qfunc\n",
    "def main(x: Output[QArray[QBit, NUM_VARIABLES]]):\n",
    "    allocate(x.len, x)\n",
    "    grover_search(\n",
    "        reps=1,\n",
    "        oracle=lambda vars: phase_oracle(sat_oracle, vars),\n",
    "        packed_vars=x,\n",
    "    )\n",
    "\n",
    "\n",
    "qmod = create_model(\n",
    "    main, constraints=Constraints(max_width=20), out_file=\"3_sat_grover\"\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fb73f614",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Synthesizing the Circuit\n",
    "\n",
    "We synthesize the circuit using the Classiq synthesis engine. The synthesis takes several seconds:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "994f958c-595e-4a56-9e41-a5aaf8a75b03",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "qprog = synthesize(qmod)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c161436b-4ee9-4e35-94cd-2831a893aaf6",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "tags": []
   },
   "source": [
    "## Showing the Resulting Circuit\n",
    "\n",
    "Once the Classiq synthesis engine finishes the job, we can show the resulting circuit in the interactive GUI:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "fd3eb709-e7ef-4d46-8f7a-e42c34ee9381",
   "metadata": {
    "tags": []
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      ""
     ]
    }
   ],
   "source": [
    "show(qprog)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9900e10e",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Executing the Circuit\n",
    "\n",
    "Lastly, we run the resulting circuit with the Classiq execute interface using the `execute` function."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "005ebd9d-3afa-47a4-a941-910060509ac2",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "result = execute(qprog).result_value()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "478e4440",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "Upon printing the result, we see that our execution of Grover's algorithm successfully found the satisfying assignments for the input formula:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "c0f1248c-9f10-4b88-b64f-317bf811ae1f",
   "metadata": {
    "tags": []
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{'x': [0, 1, 0]}: 510, {'x': [0, 1, 1]}: 490]"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result.parsed_counts"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "4b82ed33-37a2-4ab4-ba9a-8b92e240f9d2",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert sat_formula(*result.parsed_counts[0].state[\"x\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d73514b2-03bb-4b05-9ee7-98a1e314e0da",
   "metadata": {},
   "source": [
    "# Large 3-SAT Example"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ece3be60-21d5-49a1-9c65-8081e4ecce2d",
   "metadata": {},
   "source": [
    "We now demonstrate on a larger example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "fc8df585-ac75-44c1-a60d-9cba0225eee7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x0     x1     x2     x3    | Result\n",
      "-----------------------------------\n",
      "0      0      0      0     | 0    \n",
      "0      0      0      1     | 1    \n",
      "0      0      1      0     | 0    \n",
      "0      0      1      1     | 1    \n",
      "0      1      0      0     | 0    \n",
      "0      1      0      1     | 0    \n",
      "0      1      1      0     | 0    \n",
      "0      1      1      1     | 0    \n",
      "1      0      0      0     | 0    \n",
      "1      0      0      1     | 0    \n",
      "1      0      1      0     | 0    \n",
      "1      0      1      1     | 0    \n",
      "1      1      0      0     | 0    \n",
      "1      1      0      1     | 0    \n",
      "1      1      1      0     | 0    \n",
      "1      1      1      1     | 0    \n"
     ]
    }
   ],
   "source": [
    "def sat_formula_large(x1, x2, x3, x4):\n",
    "    return (\n",
    "        (x2 | x3 | x4)\n",
    "        & (_not(x1) | x2 | x3)\n",
    "        & (_not(x1) | x2 | _not(x3))\n",
    "        & (_not(x1) | _not(x2) | x3)\n",
    "        & (x1 | _not(x2) | _not(x3))\n",
    "        & (x1 | _not(x2) | x3)\n",
    "        & (_not(x1) | _not(x2) | _not(x4))\n",
    "        & (_not(x1) | _not(x2) | x4)\n",
    "        & (_not(x2) | _not(x3) | _not(x4))\n",
    "        & (x2 | _not(x3) | x4)\n",
    "        & (x1 | _not(x3) | x4)\n",
    "        & (x1 | _not(x2) | _not(x4))\n",
    "        & (_not(x1) | _not(x2) | _not(x3))\n",
    "    )\n",
    "\n",
    "\n",
    "NUM_VARIABLES_LARGE = 4\n",
    "print_truth_table(NUM_VARIABLES_LARGE, sat_formula_large)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "7c50cd26-8a64-4ee9-97da-69951c791ee6",
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      ""
     ]
    }
   ],
   "source": [
    "@qfunc\n",
    "def sat_oracle_large(x: QArray[QBit], res: QBit):\n",
    "    res ^= sat_formula_large(*[x[i] for i in range(NUM_VARIABLES_LARGE)])\n",
    "\n",
    "\n",
    "@qfunc\n",
    "def main(x: Output[QArray[QBit, NUM_VARIABLES_LARGE]]):\n",
    "    allocate(x.len, x)\n",
    "    grover_search(\n",
    "        reps=2,\n",
    "        oracle=lambda vars: phase_oracle(sat_oracle_large, vars),\n",
    "        packed_vars=x,\n",
    "    )\n",
    "\n",
    "\n",
    "qmod_large = create_model(\n",
    "    main, constraints=Constraints(max_width=24), out_file=\"3_sat_grover_large\"\n",
    ")\n",
    "qprog_large = synthesize(qmod_large)\n",
    "show(qprog_large)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "632bd4d8-3cab-4d0f-9b85-bc475dc923fc",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{'x': [0, 0, 0, 1]}: 492,\n",
       " {'x': [0, 0, 1, 1]}: 458,\n",
       " {'x': [1, 1, 0, 0]}: 6,\n",
       " {'x': [0, 1, 1, 0]}: 5,\n",
       " {'x': [0, 1, 1, 1]}: 5,\n",
       " {'x': [0, 0, 0, 0]}: 5,\n",
       " {'x': [1, 0, 0, 1]}: 4,\n",
       " {'x': [1, 1, 0, 1]}: 4,\n",
       " {'x': [0, 1, 0, 0]}: 4,\n",
       " {'x': [0, 1, 0, 1]}: 3,\n",
       " {'x': [1, 1, 1, 1]}: 3,\n",
       " {'x': [1, 0, 0, 0]}: 3,\n",
       " {'x': [1, 0, 1, 0]}: 3,\n",
       " {'x': [1, 1, 1, 0]}: 3,\n",
       " {'x': [1, 0, 1, 1]}: 2]"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result_large = execute(qprog_large).result_value()\n",
    "result_large.parsed_counts"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "acd91d9f-abe0-472e-ac76-016b9b22807f",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert sat_formula_large(*result_large.parsed_counts[0].state[\"x\"])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "49c24c5e",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "\n",
    "# References\n",
    "\n",
    "<a name='Gro97'>[1]</a>: [Grover, Lov K. \"Quantum mechanics helps in searching for a needle in a haystack.\" Physical Review Letters 79.2 (1997): 325.](https://journals.aps.org/prl/abstract/10.1103/PhysRevLett.79.325)\n",
    "\n",
    "<a name='GroWiki'>[2]</a>: [Grover's algorithm (Wikipedia)](https://en.wikipedia.org/wiki/Grover%27s_algorithm)\n",
    "\n",
    "<a name='3SAT'>[3]</a>: [3-SAT Problem (Wikipedia)](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability)\n",
    "\n",
    "<a name='CNF'>[4]</a>: [Conjunctive Normal Form (Wikipedia)](https://en.wikipedia.org/wiki/Conjunctive_normal_form)\n"
   ]
  }
 ],
 "metadata": {
  "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.11.7"
  },
  "vscode": {
   "interpreter": {
    "hash": "a07aacdcc8a415e7643a2bc993226848ff70704ebef014f87460de9126b773d0"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}