SolveSATWithGrover/SolveSATWithGrover.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Solving SAT problem with Grover's algorithm\n",
    "\n",
    "The **\"Solving SAT problem with Grover's algorithm\"** quantum kata is a series of exercises designed\n",
    "to get you comfortable with using Grover's algorithm to solve realistic problems\n",
    "using boolean satisfiability problems (SAT) as an example.\n",
    "\n",
    "Each task is wrapped in one operation preceded by the description of the task.\n",
    "Your goal is to fill in the blank (marked with the `// ...` comments)\n",
    "with some Q# code that solves the task. To verify your answer, run the cell using Ctrl+Enter (⌘+Enter on macOS).\n",
    "\n",
    "Within each section, tasks are given in approximate order of increasing difficulty; \n",
    "harder ones are marked with asterisks."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Part I. Oracles for SAT problems\n",
    "\n",
    "The most interesting part of learning Grover's algorithm is solving realistic problems.\n",
    "This means using oracles which express an actual problem and not simply hard-code a known solution.\n",
    "In this section we'll learn how to express boolean satisfiability problems as quantum oracles."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.1. The AND oracle: $f(x) = x_0 \\wedge x_1$\n",
    "\n",
    "**Inputs:** \n",
    "\n",
    "  1. 2 qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2), \n",
    "i.e., flip the target state if all qubits of the query register are in the $|1\\rangle$ state, \n",
    "and leave it unchanged otherwise.\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "**Stretch Goal:** \n",
    "\n",
    "Can you implement the oracle so that it would work \n",
    "for `queryRegister` containing an arbitrary number of qubits?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T11_Oracle_And \n",
    "\n",
    "operation Oracle_And (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.1.-The-AND-oracle:-$f(x)-=-x_0-\\wedge-x_1$).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.2. The OR oracle: $f(x) = x_0 \\vee x_1$\n",
    "\n",
    "**Inputs:** \n",
    "\n",
    "  1. 2 qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "**Goal:** \n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2), \n",
    "i.e., flip the target state if at least one qubit of the query register is in the $|1\\rangle$ state, \n",
    "and leave it unchanged otherwise.\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "**Stretch Goal:** \n",
    "\n",
    "Can you implement the oracle so that it would work \n",
    "for `queryRegister` containing an arbitrary number of qubits?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T12_Oracle_Or \n",
    "\n",
    "operation Oracle_Or (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.2.-The-OR-oracle:-$f(x)-=-x_0-\\vee-x_1$).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.3. The XOR oracle: $f(x) = x_0 \\oplus x_1$\n",
    "\n",
    "**Inputs:** \n",
    "\n",
    "  1. 2 qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "**Goal:** \n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2), \n",
    "i.e., flip the target state if the qubits of the query register are in different states, \n",
    "and leave it unchanged otherwise.\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "**Stretch Goal:** \n",
    "\n",
    "Can you implement the oracle so that it would work \n",
    "for `queryRegister` containing an arbitrary number of qubits?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T13_Oracle_Xor \n",
    "\n",
    "operation Oracle_Xor (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.3.-The-XOR-oracle:-$f(x)-=-x_0-\\oplus-x_1$).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.4. Alternating bits oracle: $f(x) = (x_0 \\oplus x_1) \\wedge (x_1 \\oplus x_2) \\wedge \\dots \\wedge (x_{N-2} \\oplus x_{N-1})$\n",
    "\n",
    "**Inputs:** \n",
    "\n",
    "  1. N qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2).\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "> This oracle marks two states similar to the state explored in task 1.2 of the GroversAlgorithm kata: \n",
    "$|10101...\\rangle$ and $|01010...\\rangle$.  \n",
    "It is possible (and quite straightforward) to implement this oracle based on this observation; \n",
    "however, for the purposes of learning to write oracles to solve SAT problems we recommend using the representation above.\n",
    "\n",
    "<details>\n",
    "  <summary><b>Need a hint? Click here</b></summary>\n",
    "  Remember that you can use operations defined in previous tasks.\n",
    "</details>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T14_Oracle_AlternatingBits \n",
    "\n",
    "operation Oracle_AlternatingBits (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.4.-Alternating-bits-oracle:-$f(x)-=-(x_0-\\oplus-x_1)-\\wedge-(x_1-\\oplus-x_2)-\\wedge-\\dots-\\wedge-(x_{N-2}-\\oplus-x_{N-1})$).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.5. Evaluate one clause of a SAT formula\n",
    "\n",
    "> For SAT problems, $f(x)$ is represented as a conjunction (an AND operation) of several clauses on $N$ variables,\n",
    "and each clause is a disjunction (an OR operation) of **one or several** variables or negated variables:\n",
    ">\n",
    "> $$clause(x) = \\bigvee_k y_{k},\\text{ where }y_{k} =\\text{ either }x_j\\text{ or }\\neg x_j\\text{ for some }j \\in \\{0, \\dots, N-1\\}$$\n",
    ">\n",
    "> For example, one of the possible clauses on two variables is:\n",
    ">\n",
    "> $$clause(x) = x_0 \\vee \\neg x_1$$\n",
    "\n",
    "**Inputs:**\n",
    "\n",
    "  1. N qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "  3. A 1-dimensional array of tuples `clause` which describes one clause of a SAT problem instance $clause(x)$.\n",
    "\n",
    "`clause` is an array of one or more tuples, each of them describing one component of the clause.\n",
    "\n",
    "Each tuple is an `(Int, Bool)` pair:\n",
    "\n",
    "* the first element is the index $j$ of the variable $x_j$, \n",
    "* the second element is `true` if the variable is included as itself ($x_j$) and `false` if it is included as a negation ($\\neg x_j$).\n",
    "\n",
    "**Example:**\n",
    "\n",
    "* The clause $x_0 \\vee \\neg x_1$ can be represented as `[(0, true), (1, false)]`.\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2).\n",
    "\n",
    "Leave the query register in the same state it started in."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T15_Oracle_SATClause \n",
    "\n",
    "operation Oracle_SATClause (queryRegister : Qubit[], target : Qubit, clause : (Int, Bool)[]) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.5.-Evaluate-one-clause-of-a-SAT-formula).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 1.6. k-SAT problem oracle\n",
    "\n",
    "> For k-SAT problems, $f(x)$ is represented as a conjunction (an AND operation) of $M$ clauses on $N$ variables,\n",
    "and each clause is a disjunction (an OR operation) of **one or several** variables or negated variables:\n",
    ">\n",
    "> $$f(x) = \\bigwedge_i \\big(\\bigvee_k y_{ik} \\big),\\text{ where }y_{ik} =\\text{ either }x_j\\text{ or }\\neg x_j\\text{ for some }j \\in \\{0, \\dots, N-1\\}$$\n",
    "\n",
    "**Inputs:**\n",
    "\n",
    "  1. N qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "  3. A 2-dimensional array of tuples `problem` which describes the k-SAT problem instance $f(x)$.\n",
    "\n",
    "$i$-th element of `problem` describes the $i$-th clause of $f(x)$; \n",
    "it is an array of one or more tuples, each of them describing one component of the clause.\n",
    "\n",
    "Each tuple is an `(Int, Bool)` pair:\n",
    "\n",
    "* the first element is the index $j$ of the variable $x_j$, \n",
    "* the second element is `true` if the variable is included as itself ($x_j$) and `false` if it is included as a negation ($\\neg x_j$).\n",
    "\n",
    "**Example:**\n",
    "\n",
    "A more general case of the OR oracle for 3 variables $f(x) = (x_0 \\vee x_1 \\vee x_2)$ can be represented as `[[(0, true), (1, true), (2, true)]]`.\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2).\n",
    "\n",
    "Leave the query register in the same state it started in."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T16_Oracle_SAT \n",
    "\n",
    "operation Oracle_SAT (queryRegister : Qubit[], target : Qubit, problem : (Int, Bool)[][]) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solving SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-1.6.-k-SAT-problem-oracle).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Part II. Oracles for exactly-1 3-SAT problem\n",
    "\n",
    "Exactly-1 3-SAT problem (also known as \"one-in-three 3-SAT\") is a variant of a general 3-SAT problem.\n",
    "It has a structure similar to a 3-SAT problem, but each clause must have *exactly one* true literal, \n",
    "while in a normal 3-SAT problem each clause must have *at least one* true literal."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 2.1. \"Exactly one $|1\\rangle$\" oracle\n",
    "\n",
    "**Inputs:** \n",
    "\n",
    "  1. 3 qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "**Goal:** \n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2), \n",
    "where $f(x) = 1$ if exactly one bit of $x$ is in the $|1\\rangle$ state, and $0$ otherwise.\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "**Stretch Goal:** \n",
    "\n",
    "Can you implement the oracle so that it would work \n",
    "for `queryRegister` containing an arbitrary number of qubits?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T21_Oracle_Exactly1One \n",
    "\n",
    "operation Oracle_Exactly1One (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solve SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-2.1.-\"Exactly-one-$|1\\rangle$\"-oracle).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 2.2. \"Exactly-1 3-SAT\" oracle\n",
    "\n",
    "**Inputs:**\n",
    "\n",
    "  1. N qubits in an arbitrary state $|x\\rangle$ (input/query register).\n",
    "\n",
    "  2. A qubit in an arbitrary state $|y\\rangle$ (target qubit).\n",
    "\n",
    "  3. A 2-dimensional array of tuples `problem` which describes the 3-SAT problem instance $f(x)$.\n",
    "\n",
    "`problem` describes the problem instance in the same format as in task 1.6;\n",
    "each clause of the formula is guaranteed to have exactly 3 terms.\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Transform state $|x,y\\rangle$ into state $|x, y \\oplus f(x)\\rangle$ ($\\oplus$ is addition modulo 2).\n",
    "\n",
    "Leave the query register in the same state it started in.\n",
    "\n",
    "**Example:**\n",
    "\n",
    "An instance of the problem $f(x) = (x_0 \\vee x_1 \\vee x_2)$ can be represented as `[[(0, true), (1, true), (2, true)]]`,\n",
    "and its solutions will be `(true, false, false)`, `(false, true, false)` and `(false, false, true)`, \n",
    "but none of the variable assignments in which more than one variable is true, which are solutions for the general SAT problem.\n",
    "\n",
    "<br/>\n",
    "<details>\n",
    "  <summary><b>Need a hint? Click here</b></summary>\n",
    "  Can you reuse parts of the code in section 1?\n",
    "</details>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T22_Oracle_Exactly1SAT \n",
    "\n",
    "operation Oracle_Exactly1_3SAT (queryRegister : Qubit[], target : Qubit, problem : (Int, Bool)[][]) : Unit is Adj {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solve SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-2.2.-\"Exactly-1-3-SAT\"-oracle).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Part III. Using Grover's algorithm for problems with multiple solutions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 3.1. Using Grover's algorithm\n",
    "\n",
    "**Goal:**\n",
    "\n",
    "Implement Grover's algorithm and use it to find solutions to SAT instances from parts I and II. \n",
    "\n",
    "> If you want to learn the Grover's algorithm itself, try doing [GroversAlgorithm kata](./../GroversAlgorithm/GroversAlgorithm.ipynb) first.\n",
    "\n",
    "> This is an open-ended task, and is not covered by a unit test. To run the code, execute the cell with the definition of the `Run_GroversSearch_Algorithm` operation first; if it compiled successfully without any errors, you can run the operation by executing the next cell (`%simulate Run_GroversSearch_Algorithm`).\n",
    "\n",
    "> Note that this task relies on your implementations of the previous tasks. If you are getting the \"No variable with that name exists.\" error, you might have to execute previous code cells before retrying this task.\n",
    "\n",
    "<details>\n",
    "  <summary><b>Need a hint? Click here</b></summary>\n",
    "Experiment with SAT instances with different number of solutions and the number of algorithm iterations \n",
    "to see how the probability of the algorithm finding the correct answer changes depending on these two factors.\n",
    "\n",
    "For example, \n",
    "* the AND oracle from task 1.1 has exactly one solution,\n",
    "* the alternating bits oracle from task 1.4 has exactly two solutions,\n",
    "* the OR oracle from task 1.2 for 2 qubits has exactly 3 solutions, and so on.\n",
    "</details>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "operation Run_GroversSearch_Algorithm () : Unit {\n",
    "    // ...\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%simulate Run_GroversSearch_Algorithm"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solve SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-3.1.-Using-Grover's-algorithm).*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Task 3.2. Universal implementation of Grover's algorithm\n",
    "\n",
    "**Inputs:**\n",
    "\n",
    "  1. The number of qubits N.\n",
    "\n",
    "  2. A marking oracle which implements a boolean expression, similar to the oracles from part I.\n",
    "\n",
    "**Output:**\n",
    "\n",
    "An array of N boolean values which satisfy the expression implemented by the oracle \n",
    "(i.e., any basis state marked by the oracle).\n",
    "\n",
    "> Note that the similar task in the [GroversAlgorithm kata](./../GroversAlgorithm/GroversAlgorithm.ipynb) required you to implement Grover's algorithm \n",
    "in a way that would be robust to accidental failures, but you knew the optimal number of iterations \n",
    "(the number that minimized the probability of such failure).\n",
    "> \n",
    "> In this task you also need to make your implementation robust to not knowing the optimal number of iterations.\n",
    "> You can see an example of doing that in [Exploring Grover's Algorithm tutorial](./../tutorials/ExploringGroversAlgorithm/ExploringGroversAlgorithm.ipynb)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": [
     "timeout"
    ]
   },
   "outputs": [],
   "source": [
    "%kata T32_UniversalGroversAlgorithm \n",
    "\n",
    "operation UniversalGroversAlgorithm (N : Int, oracle : ((Qubit[], Qubit) => Unit is Adj)) : Bool[] {\n",
    "    // ...\n",
    "    return [false, size = N];\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*Can't come up with a solution? See the explained solution in the [Solve SAT problem with Grover's algorithm Workbook](./Workbook_SolveSATWithGrover.ipynb#Task-3.2.-Universal-implementation-of-Grover's-algorithm).*"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Q#",
   "language": "qsharp",
   "name": "iqsharp"
  },
  "language_info": {
   "file_extension": ".qs",
   "mimetype": "text/x-qsharp",
   "name": "qsharp",
   "version": "0.14"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}