SolveSATWithGrover/Workbook_SolveSATWithGrover.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Solving SAT problem with Grover's algorithm Kata Workbook\n",
    "\n",
    "**What is this workbook?**\n",
    "A workbook is a collection of problems, accompanied by solutions to them. \n",
    "The explanations focus on the logical steps required to solve a problem; they illustrate the concepts that need to be applied to come up with a solution to the problem, explaining the mathematical steps required. \n",
    "\n",
    "Note that a workbook should not be the primary source of knowledge on the subject matter; it assumes that you've already read a tutorial or a textbook and that you are now seeking to improve your problem-solving skills. You should attempt solving the tasks of the respective kata first, and turn to the workbook only if stuck. While a textbook emphasizes knowledge acquisition, a workbook emphasizes skill acquisition.\n",
    "\n",
    "This workbook describes the solutions to the problems offered in the [Solving SAT problem with Grover's algorithm kata](./SolveSATWithGrover.ipynb). Since the tasks are offered as programming problems, the explanations also cover some elements of Q# that might be non-obvious for a first-time user.\n",
    "\n",
    "**What you should know for this workbook**\n",
    "\n",
    "You should be familiar with the following concepts before tackling the Solve SAT with Grover kata (and this workbook):\n",
    "\n",
    "1. [Basic linear algebra](./../tutorials/LinearAlgebra/LinearAlgebra.ipynb).\n",
    "2. [Single-qubit](./../tutorials/SingleQubitGates/SingleQubitGates.ipynb) and [multi-qubit quantum gates](./../tutorials/MultiQubitGates/MultiQubitGates.ipynb) and using them to manipulate the state of the system.\n",
    "3. [Exploring Grover's algorithm tutorial](./../tutorials/ExploringGroversAlgorithm/ExploringGroversAlgorithmTutorial.ipynb) and [Grover's algorithm implementation kata](./../GroversAlgorithm/GroversAlgorithm.ipynb).\n",
    "4. Basic knowledge of logic gates and SAT problems."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Part I. Oracles for SAT problems"
   ]
  },
  {
   "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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "The goal is to flip the qubit $|y\\rangle$ if and only if all qubits in the register $|x\\rangle$ are in the state $|1\\rangle$.  \n",
    "Hence the required unitary $U_{and}$ is such that:\n",
    "$$U_{and}|x\\rangle|y\\rangle = \\begin{cases} \n",
    "          |x\\rangle|y\\rangle & \\text{if }x \\neq 1...1 \\\\\n",
    "          |x\\rangle X|y\\rangle & \\text{if }x = 1...1 \n",
    "       \\end{cases}$$\n",
    "       \n",
    "We can rewrite this as \n",
    "\n",
    "$$U_{and} = \\big(I - |1...1\\rangle\\langle 1...1|\\big) \\otimes I + |1...1\\rangle\\langle 1...1|\\otimes X$$ \n",
    "\n",
    "Here we're using a convenient shorthand for ket-bra notation of gate effect on multiple basis states at once:\n",
    "\n",
    "$$I - |1...1\\rangle\\langle 1...1| = \\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}|i\\rangle\\langle i|$$\n",
    "\n",
    "For the number of qubits in the input register $n=2$, $U_{and}$ is the **Toffoli** gate:\n",
    "$$U_{and} = \\begin{bmatrix}\n",
    "1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n",
    "0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n",
    "0 & 0 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n",
    "0 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\\\\n",
    "0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 \\\\\n",
    "0 & 0 & 0 & 0 & 0 & 1 & 0 & 0 \\\\\n",
    "0 & 0 & 0 & 0 & 0 & 0 & 0 & 1 \\\\\n",
    "0 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\\\\n",
    "\\end{bmatrix}$$\n",
    "\n",
    "In the general case of arbitrary number of qubits in the input, \n",
    "this can be represented as a `Controlled X` gate, with the input register $|x\\rangle$ as control and the target qubit $|y\\rangle$ as target. \n",
    "\n",
    "> In Q# you can use [Controlled functor](https://docs.microsoft.com/azure/quantum/user-guide/language/expressions/functorapplication#controlled-functor) to apply a controlled version of the gate, if the gate specifies it.\n",
    ">\n",
    "> If $|x\\rangle$ consists of just 2 qubits, we could also use the built-in **Toffoli** gate - the [`CCNOT` gate](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.intrinsic.ccnot)."
   ]
  },
  {
   "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",
    "    Controlled X(queryRegister, target); \n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.1 of the Solving SAT with Grover's algorithm kata.](./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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "The goal is to flip the qubit $|y\\rangle$ if at least one qubit in the register $|x\\rangle$ is in the state $|1\\rangle$.  \n",
    "This can also be restated as to flip the qubit $|y\\rangle$ *unless* the register $|x\\rangle$ is in the state $|0...0\\rangle$.\n",
    "\n",
    "Hence the required unitary $U_{or}$ is such that:\n",
    "$$U_{or}|x\\rangle|y\\rangle = \\begin{cases} \n",
    "          |x\\rangle |y\\rangle & \\text{if }x = 0...0  \\\\\n",
    "          |x\\rangle X|y\\rangle & \\text{if }x \\neq 0...0\n",
    "       \\end{cases}$$\n",
    "\n",
    "We can rewrite this as\n",
    "$$U_{or} = |0...0\\rangle\\langle 0...0|\\otimes I + \\big(I - |0...0\\rangle\\langle 0...0|\\big) \\otimes X$$  \n",
    "\n",
    "We can now reduce this problem to the AND oracle using the fact that OR gate can be created using an AND gate and NOT gates.  \n",
    "\n",
    "$$x_0\\vee x_1\\vee ... \\vee x_{n-1} = \\lnot(\\lnot x_0\\wedge \\lnot x_1\\wedge ... \\wedge \\lnot x_{n-1})$$\n",
    "\n",
    "Thus $U_{or}$ can be rewritten as $U_{or}=(X^{\\otimes n}\\otimes X) \\cdot U_{and} \\cdot (X^{\\otimes n}\\otimes I)$. \n",
    "\n",
    "> <details>\n",
    "    <summary><b>Click here to see how to get this matrix expression using ket-bra notation</b></summary>\n",
    ">    \n",
    "$$\n",
    "U_{or}= (X^{\\otimes n}\\otimes X) \\cdot U_{and} \\cdot (X^{\\otimes n}\\otimes I) = \\\\\n",
    " = (X^{\\otimes n}\\otimes X) \\cdot (\\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}|i\\rangle\\langle i| \\otimes I + |1...1\\rangle\\langle 1...1|\\otimes X) \\cdot (X^{\\otimes n}\\otimes I) = \\\\\n",
    " = (X^{\\otimes n}\\otimes X) \\cdot (\\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}|i\\rangle\\langle i|X^{\\otimes n} \\otimes I + |1...1\\rangle\\langle 1...1|X^{\\otimes n}\\otimes X) = \\\\\n",
    " = (X^{\\otimes n}\\otimes X) \\cdot (\\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}|i\\rangle\\langle i|X^{\\otimes n} \\otimes I + |1...1\\rangle\\langle 0...0|\\otimes X) = \\\\\n",
    " = \\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}X^{\\otimes n}|i\\rangle\\langle i|X^{\\otimes n} \\otimes X + X^{\\otimes n}|1...1\\rangle\\langle 0...0|\\otimes I = \\\\\n",
    " = \\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |1...1\\rangle}X^{\\otimes n}|i\\rangle\\langle i|X^{\\otimes n} \\otimes X + |0...0\\rangle\\langle 0...0|\\otimes I = \\\\\n",
    " = \\sum_{i \\in \\{0,1\\}^n,\\\\ |i\\rangle\\neq |0...0\\rangle}|i\\rangle\\langle i| \\otimes X + |0...0\\rangle\\langle 0...0|\\otimes I$$\n",
    "</details>\n",
    "\n",
    "This corresponds to the following steps:\n",
    "\n",
    "1. Flip all the qubits of $|x\\rangle$ using X gates to convert the inputs from $|x_0, x_1, ..., x_{n-1}\\rangle$ to $|\\lnot x_0, \\lnot x_1, ..., \\lnot x_{n-1}\\rangle$.\n",
    "2. Apply $U_{and}$ oracle to convert $|y\\rangle$ to $|y \\oplus (\\lnot x_0\\wedge \\lnot x_1\\wedge ... \\wedge \\lnot x_{n-1}) \\rangle$.\n",
    "3. Undo the flipping to return the inputs to $|x_0, x_1, ..., x_{n-1}\\rangle$.\n",
    "4. Flip the state of the target qubit $|y\\rangle$ again to perform the final negation $|y \\oplus \\lnot(\\lnot x_0\\wedge \\lnot x_1\\wedge ... \\wedge \\lnot x_{n-1}) \\rangle = |y \\oplus x_0\\vee x_1\\vee ... \\vee x_{n-1} \\rangle$.\n",
    "\n",
    "> We can use the ` within ... apply ...` construct in Q# implement the pattern of modifying the qubits of $|x\\rangle$, applying the oracle to get the result and write it into $|y\\rangle$ and undoing (uncomputing) the modification to $|x\\rangle$."
   ]
  },
  {
   "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",
    "    within {\n",
    "        // Flip input qubits to negate them\n",
    "        ApplyToEachA(X, queryRegister);\n",
    "    } apply {\n",
    "        // Use the AND oracle to get the AND of negated inputs\n",
    "        Oracle_And(queryRegister, target);\n",
    "    }\n",
    "    // Flip the target to get the final answer\n",
    "    X(target);\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.2 of the Solving SAT with Grover's algorithm kata.](./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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "Let's consider the case of $n$-qubit register $|x\\rangle$; then $f(x) = x_0 \\oplus x_1 \\oplus ... \\oplus x_{n-1}$. \n",
    "The goal is to flip the qubit $|y\\rangle$ if and only if $f(x) = 1$.  \n",
    "\n",
    "Hence the effect of the required unitary $U_{xor}$ on the basis state $|x\\rangle|y\\rangle$ will be:\n",
    "\n",
    "$$U_{xor}|x\\rangle|y\\rangle = |x\\rangle|y\\oplus f(x)\\rangle = \\\\\n",
    "= |x\\rangle|y\\oplus x_0 \\oplus x_1 \\oplus ... \\oplus x_{n-1}\\rangle = \\\\\n",
    "= |x\\rangle|(...((y\\oplus x_0) \\oplus x_1) ... )\\oplus x_{n-1}\\rangle$$\n",
    "\n",
    "Let's consider a unitary $U_{\\oplus i}$, which has the following effect on the basis state:\n",
    "\n",
    "$$U_{\\oplus i}|x\\rangle|y\\rangle = |x\\rangle|y \\oplus x_i\\rangle$$\n",
    "\n",
    "This unitary is simply a CNOT gate with i-th qubit $|x_i\\rangle$ as control and $|y\\rangle$ as target.\n",
    "\n",
    "Then we can rewrite the effect of our unitary $U_{xor}$ as follows:\n",
    "\n",
    "$$U_{xor}|x\\rangle|y\\rangle = U_{\\oplus n-1} (U_{\\oplus n-2} (... U_{\\oplus 0} |x\\rangle|y\\rangle ...)) = \\prod_{i=0}^{n-1}U_{\\oplus i}|x\\rangle|y\\rangle$$\n",
    "\n",
    "We see that we can write\n",
    "\n",
    "$$U_{xor}=\\prod_{i=0}^{n-1}U_{\\oplus i}$$\n",
    "\n",
    "We can implement this as a sequence of CNOT gates, with each of the qubits of the input register as controls and the output qubit as target."
   ]
  },
  {
   "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",
    "    ApplyToEachA(CNOT(_, target), queryRegister); \n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.3 of the Solving SAT with Grover's algorithm kata.](./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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "Let $x_i'=x_i\\oplus x_{i+1}$, then we can rewrite $f(x)$ as $f(x) = x_0' \\wedge x_1' \\wedge ... \\wedge x_{N-2}'$.\n",
    "\n",
    "We can compute $x_i'$ using $U_{xor}$ (implemented by operation `Oracle_Xor`) from the previous task, since $U_{xor}|x_l\\rangle|x_r\\rangle|0\\rangle = |x_l\\rangle|x_r\\rangle|x_l \\oplus x_r\\rangle$.\n",
    "We will store XORs of pairs of adjacent qubits in an auxiliary register of qubits that we'll allocate for this purpose. (This procedure can be undone in the same way before deallocating that register.)\n",
    "\n",
    "Now we can find $f(x)$ using the values $x_i'$, i.e., transform $|y\\rangle$ into $|y \\oplus f(x)\\rangle$ using the `Oracle_And` on the auxiliary register and the `target` qubit.\n",
    "\n",
    "Hence the final solution consists of:\n",
    "1. Finding XORs of all pairs of adjacent qubits and storing them in an auxiliary register.\n",
    "2. Applying $U_{and}$ (`Oracle_And`) on `auxiliaryRegister` and `target`.\n",
    "3. Undo the computation done in 1. to reset the `auxiliaryRegister` before releasing the qubits.\n",
    "\n",
    "We can use the `within ... apply ...` construct in Q# to express this sequence of steps, similar to task 2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T14_Oracle_AlternatingBits \n",
    "\n",
    "open Microsoft.Quantum.Arrays;\n",
    "\n",
    "operation Oracle_AlternatingBits (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    let N = Length(queryRegister);\n",
    "    use auxiliaryRegister = Qubit[N-1];\n",
    "    // Find the XOR of all pairs of consecutive qubits and store the result in auxiliaryRegister\n",
    "    within {\n",
    "        for i in 0 .. N-2 {\n",
    "            Oracle_Xor(queryRegister[i .. i+1], auxiliaryRegister[i]);\n",
    "        }\n",
    "    }\n",
    "    // Use the And oracle on auxiliaryRegister to get the answer\n",
    "    apply {\n",
    "        Oracle_And(auxiliaryRegister, target); \n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can also avoid using the auxiliary register by computing XORs in place, i.e., storing the results of XOR operations in the `queryRegister` itself. \n",
    "To do this, we apply $\\textrm{CNOT}$ to two adjacent qubits, with the target qubit being the one in which we store the result. \n",
    "\n",
    "Since all qubits except those at index $0$ and $N-1$ are inputs to two XOR operations, the order of these operations must be carefully chosen.\n",
    "If we are going from index $0$ to $N-1$ when computing $x_i'$, the target must always be the lower index (the one that will not be involved in later computations), i.e., `CNOT(queryRegister[i+1], queryRegister[i])`. This way `queryRegister[i+1]` is preserved for the next XOR operation.\n",
    "\n",
    "Now the `queryRegister[0..N-2]` contains the XOR results, and we can perform the `Oracle_And` operation with this array as control directly. We uncompute the effects of the XORs computations using `within ... apply ...` construct, as usual."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T14_Oracle_AlternatingBits \n",
    "\n",
    "open Microsoft.Quantum.Arrays;\n",
    "\n",
    "operation Oracle_AlternatingBits (queryRegister : Qubit[], target : Qubit) : Unit is Adj {\n",
    "    let N = Length(queryRegister);\n",
    "    // Find the XOR of all pairs of consecutive qubits and store the result in queryRegister itself\n",
    "    within {\n",
    "        for i in 0 .. N-2 {\n",
    "            CNOT(queryRegister[i+1], queryRegister[i]);\n",
    "        }\n",
    "    }\n",
    "    // Use the And oracle on the first N-1 qubits of queryRegister to get the answer\n",
    "    apply {\n",
    "        Oracle_And(Most(queryRegister),target); \n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.4 of the Solving SAT with Grover's algorithm kata.](./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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "This task involves evaluating a clause which is a disjunction (OR) of negated and non-negated variables encoded in the `queryRegister` . This task can be solved in 2 steps using a similar technique to the one we saw in task 1.4:\n",
    "\n",
    "1. We first flip the qubits which are negated in `clause` (and later undo this operation).  \n",
    "   To do this, we conditionally apply an $X$ gate to qubit $|x_j\\rangle$ if and only if the clause has a term of the form `(j, false)`.\n",
    "2. We use the $U_{or}$ unitary (implemented by `Oracle_Or`) to calculate $|y\\oplus f(x)\\rangle$.  \n",
    "   Here we need to construct an array `clause_qubits` - all qubits which are included as a negated or non-negated variable in the clause. \n",
    "We then apply the `Oracle_Or` operation on `clause_qubits` and `target`.\n",
    "\n",
    "> We want our implementation of `Oracle_SATClause` be adjointable, and to rely on Q# compiler to generate the adjoint variant of this operation. To enable this, we move the classical computations that involve manipulating mutable variables to a separate function."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "// Find all qubits which are variables in clause\n",
    "function GetClauseQubits (queryRegister : Qubit[], clause: (Int,Bool)[]) : Qubit[] {\n",
    "    mutable clauseQubits = [];\n",
    "    for (index, _) in clause {\n",
    "        set clauseQubits += [queryRegister[index]];\n",
    "    }\n",
    "    return clauseQubits;\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T15_Oracle_SATClause \n",
    "\n",
    "open Microsoft.Quantum.Arrays;\n",
    "    \n",
    "operation Oracle_SATClause (queryRegister : Qubit[], target : Qubit, clause : (Int, Bool)[]) : Unit is Adj {\n",
    "    within {\n",
    "        // Flip all qubits which are in negated form in the SAT clause.\n",
    "        for (index, positive) in clause {\n",
    "            if not positive {\n",
    "                X(queryRegister[index]);\n",
    "            }\n",
    "        }\n",
    "    }\n",
    "    apply {\n",
    "        // Find all qubits which are variables in the clause.\n",
    "        let clauseQubits = GetClauseQubits(queryRegister, clause); \n",
    "        // Compute disjunction of variables in clause.\n",
    "        Oracle_Or(clauseQubits, target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can also use several Q# library functions and constructs to write our code in the functional style.\n",
    "\n",
    "* The functions \n",
    "[`Fst`](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.canon.fst) and\n",
    "[`Snd`](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.canon.snd) \n",
    "extract the first and second element of a 2-element tuple, respectively. \n",
    "`Fst(term)` would give us the index $j$ for variable $x_j$ and `Snd(term)` would be `false` if the variable was negated or `true` if it was not. \n",
    "* We can use the function\n",
    "[`Mapped`](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.arrays.mapped) \n",
    "to extract the list of variable indices used in the clause. Given an array and a function that is defined for the elements of the array, `Mapped` returns a new array that consists of the images of the original array under the function. `Mapped(Fst<Int, Bool>, clause)` will return an array of all first elements of the tuples in `clause`.\n",
    "* Finally, we use the function \n",
    "[`Subarray`](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.arrays.subarray) to find the `clauseQubits`: this function takes an array and a list of indices and produces a new array formed from the elements of the original array at the given locations."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%kata T15_Oracle_SATClause \n",
    "\n",
    "open Microsoft.Quantum.Arrays;\n",
    "    \n",
    "operation Oracle_SATClause (queryRegister : Qubit[], target : Qubit, clause : (Int, Bool)[]) : Unit is Adj {\n",
    "    // Flip all qubits which are in negated form in the SAT clause.\n",
    "    within {\n",
    "        for term in clause {\n",
    "            // If Snd(term) is false, apply X gate, otherwise apply I (do nothing).\n",
    "            (Snd(term)? I | X)(queryRegister[Fst(term)]);\n",
    "        }\n",
    "    }\n",
    "    apply {\n",
    "        // Get indices of all variables in clause.\n",
    "        let indexList = Mapped(Fst<Int, Bool>, clause);\n",
    "        // Get all qubits which are part of clause.\n",
    "        let clauseQubits = Subarray(indexList,queryRegister);\n",
    "        // Compute disjunction of variables in clause.\n",
    "        Oracle_Or(clauseQubits,target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.5 of the Solving SAT with Grover's algorithm kata.](./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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "This task consists of a conjunction (AND) of results of multiple clause evaluations. Each clause individually can be evaluated using the code we've written in task 1.5. The computation results of these clauses must be stored (temporarily) in freshly allocated qubits. Then the conjunction of these results can be computed using `Oracle_And` from task 1.1.\n",
    "\n",
    "Let the number of clauses in the formula be $m$, then the steps for implementing k-SAT oracle will be:\n",
    "1. Allocate an array of $m$ qubits in the state $|0\\rangle$ `auxiliaryRegister`.\n",
    "2. Evaluate each clause using `Oracle_SATClause` from task 1.5 with the corresponding element of `auxiliaryRegister` as the target qubit.\n",
    "3. Evaluate the SAT formula using `Oracle_And` implemented in task 1.1 with `auxiliaryRegister` as the input register and `target` as the target qubit.\n",
    "4. Undo step 2 to restore the auxiliary qubits back into the $|0^{\\otimes m}\\rangle$ state before releasing them.\n",
    "\n",
    "We can again use the `within ... apply ...` Q# language construct to perform steps 2, 3 and 4."
   ]
  },
  {
   "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",
    "    use auxiliaryRegister = Qubit[Length(problem)];\n",
    "    // Compute the clauses.\n",
    "    within {\n",
    "        for i in 0 .. Length(problem) - 1 {\n",
    "            Oracle_SATClause(queryRegister, auxiliaryRegister[i], problem[i]);\n",
    "        }\n",
    "    }\n",
    "    // Evaluate the overall formula using an AND oracle.\n",
    "    apply {\n",
    "        Oracle_And(auxiliaryRegister, target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 1.6 of the Solving SAT with Grover's algorithm kata.](./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": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "Consider the set of all bit strings of length $n$ which have only one bit of $x$ equal to $1$.   \n",
    "This set of bit strings is $S=\\{00...01, 00...10, ..., 00..1..00, ..., 01...00, 10...00\\}$, \n",
    "or, if we convert the bit strings to integers, \n",
    "$$S=\\{1,2,4,..2^i,..,2^{n-1}\\} = \\{2^k: 0 \\le k \\le n-1\\}$$\n",
    "\n",
    "We need to implement an oracle that flips $|y\\rangle$ if the input basis state $|x\\rangle$ corresponds to one of the bit strings in $S$. We can represent this as the following unitary in Dirac notation:\n",
    "\n",
    "$$U = \\sum_{i\\in S}|i\\rangle\\langle i|\\otimes X + \\sum_{j \\not\\in S}|j\\rangle\\langle j|\\otimes I$$\n",
    "\n",
    "This unitary can be implemented using $n$ controlled NOT gates, with `queryRegister` as control and the `target` qubit flipped if and only if the control register is in a particular state of the form $2^k$.\n",
    "\n",
    "We can use the Q# library function [`ControlledOnInt`](https://docs.microsoft.com/qsharp/api/qsharp/microsoft.quantum.canon.controlledonint) to implement these controlled NOT gates. "
   ]
  },
  {
   "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",
    "    for i in 0 .. Length(queryRegister) - 1 {\n",
    "        (ControlledOnInt(2^i, X))(queryRegister, target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 2.1 of the Solving SAT with Grover's algorithm kata.](./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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "This task is similar to [task 1.6](#Task-1.6.-k-SAT-problem-oracle): it consists of a conjunction (AND) of results of multiple clause evaluations, but this time each clause has to be evaluated using the *Exactly One 1* policy we've implemented in task 2.1, rather than an `Oracle_Or` we used in task 1.5. We can reuse the function `GetClauseQubits` from task 1.5:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "open Microsoft.Quantum.Arrays;\n",
    "    \n",
    "operation Oracle_Exactly1OneSATClause (queryRegister : Qubit[], target : Qubit, clause : (Int, Bool)[]) : Unit is Adj {\n",
    "    within {\n",
    "        for (index, positive) in clause {\n",
    "            if not positive {\n",
    "                X(queryRegister[index]);\n",
    "            }\n",
    "        }\n",
    "    }\n",
    "    apply {\n",
    "        // Find all qubits which are variables in the clause.\n",
    "        let clauseQubits = GetClauseQubits(queryRegister, clause); \n",
    "        // Check if \"Exactly one 1\" criteria is satisfied.\n",
    "        Oracle_Exactly1One(clauseQubits,target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The rest of the code is similar to task 1.6. See the [solution for task 1.6](#Task-1.6.-k-SAT-problem-oracle) for the discussion of implementation details."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "%kata T22_Oracle_Exactly1SAT \n",
    "\n",
    "operation Oracle_Exactly1_3SAT (queryRegister : Qubit[], target : Qubit, problem : (Int, Bool)[][]) : Unit is Adj {\n",
    "    use auxiliaryRegister = Qubit[Length(problem)];\n",
    "    // Compute the clauses.\n",
    "    within {\n",
    "        for i in 0 .. Length(problem) - 1 {\n",
    "            Oracle_Exactly1OneSATClause(queryRegister, auxiliaryRegister[i], problem[i]);\n",
    "        }\n",
    "    }\n",
    "    // Evaluate the overall formula using an AND oracle.\n",
    "    apply {\n",
    "        Oracle_And(auxiliaryRegister, target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 2.2 of the Solving SAT with Grover's algorithm kata.](./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. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "This task can be solved  following steps (see the [GroversAlgorithm kata](../GroversAlgorithm/GroversAlgorithm.ipynb) for details):\n",
    "\n",
    "1. Grover's algorithm requires a phase oracle, rather than the marking oracles we implemented in parts I and II, so we need to write Q# code that converts a marking oracle to a phase oracle."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "operation Oracle_Converter (markingOracle : ((Qubit[], Qubit) => Unit is Adj), register : Qubit[]) : Unit is Adj {\n",
    "    use target = Qubit();\n",
    "    // Put the target into the |-⟩ state and later revert the state\n",
    "    within { \n",
    "        X(target);\n",
    "        H(target); \n",
    "    }\n",
    "    // Apply the marking oracle; since the target is in the |-⟩ state,\n",
    "    // flipping the target if the register satisfies the oracle condition will apply a -1 factor to the state\n",
    "    apply { \n",
    "        markingOracle(register, target);\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "2. The main part of Grover's algorithm is a loop which runs the Grover's algorithm iteration with the given `markingOracle` on the given `register` the given number of times.\n",
    "This loop results in a state on the given `register` which satisfies the condition marked by the marking oracle with high probability."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "open Microsoft.Quantum.Arrays;\n",
    "\n",
    "operation GroversLoop (register: Qubit[], oracle: ((Qubit[], Qubit) => Unit is Adj), numIterations: Int) : Unit {\n",
    "    let phaseOracle = Oracle_Converter(oracle, _);\n",
    "    ApplyToEach(H, register);\n",
    "\n",
    "    for _ in 1 .. numIterations {\n",
    "        phaseOracle(register);\n",
    "        within{\n",
    "            ApplyToEachA(H, register);\n",
    "            ApplyToEachA(X, register);\n",
    "        } \n",
    "        apply{\n",
    "            Controlled Z(Most(register), Tail(register));\n",
    "        }\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "3. Finally, the operation `Run_GroversSearch_Algorithm` will define the problem you want to solve, run the `GroversLoop` and measure the qubit register to find the solution. \n",
    "\n",
    "The parameters defining size of register `N` and `oracle` are up to you!\n",
    "\n",
    "Try experimenting with the number of iterations in the code. \n",
    "Remember that for an oracle which has $M << N, N=2^n$ marked states, the optimal number of iterations is $\\frac{\\pi}{4}\\sqrt{\\frac{N}{M}}$.\n",
    "\n",
    "The solution given here runs Grover's search algorithm once, and if it fails to find the solution, you need to retry manually. You can add the logic to automate the retries; see [Exploring Grover's Algorithm tutorial](./../tutorials/ExploringGroversAlgorithm/ExploringGroversAlgorithm.ipynb) for details."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "open Microsoft.Quantum.Measurement;\n",
    "open Microsoft.Quantum.Convert;\n",
    "\n",
    "operation Run_GroversSearch_Algorithm () : Unit {\n",
    "    // Create a data structure describing the SAT instance we want to solve\n",
    "    let problem = [[(0, true)], [(0, false), (1, false)]];\n",
    "    let N = 2;\n",
    "\n",
    "    // Define the oracle we want to use; try this with different oracles!\n",
    "    let oracle = Oracle_SAT(_, _, problem);\n",
    "    \n",
    "    // Try different numbers of iterations.\n",
    "    let numIterations = 1;\n",
    "    use (register, output) = (Qubit[N], Qubit());\n",
    "    Message($\"Trying search with {numIterations} iterations\");\n",
    "    GroversLoop(register, oracle, numIterations);\n",
    "\n",
    "    // Measure the result.\n",
    "    let res = MultiM(register);\n",
    "\n",
    "    // Apply the oracle to the register after measurement to check whether the result is correct. \n",
    "    oracle(register, output);\n",
    "\n",
    "    if MResetZ(output) == One {\n",
    "        let answer = ResultArrayAsBoolArray(res);\n",
    "        Message($\"Found Answer: {answer}\");\n",
    "    } else {\n",
    "        Message(\"Failed to find an answer. Try again!\");\n",
    "    }\n",
    "    ResetAll(register);        \n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "%simulate Run_GroversSearch_Algorithm"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 3.1 of the Solving SAT with Grover's algorithm kata.](./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)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Solution\n",
    "\n",
    "This is very similar to task 3.1, but we don't know the problem described by the `oracle`, so we have no way of predicting the optimal number of iterations. Instead we try the series $\\{1, 2, 4, 8, ...\\}$ as the number of iterations. Even if none of these numbers are optimal, we will still eventually get the correct answer with high probability. (There are also other ways to pick the sequence of the numbers of iterations to try; feel free to experiment with them!)\n",
    "\n",
    "We use the repeat-until-success (RUS) loop to try the search with different numbers of iterations until we find an answer. The `repeat` block (the body of the loop) consists of performing the `GroversLoop`, measuring the result and checking if it is correct. The `until` block defines the condition of exiting the loop - if we found a correct answer or reached a time-out condition. The `fixup` block happens before retrying the algorithm, in this case it doubles the number of iterations in order to try again."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "tags": [
     "timeout"
    ]
   },
   "outputs": [],
   "source": [
    "%kata T32_UniversalGroversAlgorithm \n",
    "\n",
    "open Microsoft.Quantum.Measurement;\n",
    "open Microsoft.Quantum.Convert;\n",
    "\n",
    "operation UniversalGroversAlgorithm (N : Int, oracle : ((Qubit[], Qubit) => Unit is Adj)) : Bool[] {\n",
    "    // Since we are unaware of the optimal number of iterations, we try different numbers of iterations.\n",
    "    mutable answer = [false, size = N];\n",
    "    use (register, output) = (Qubit[N], Qubit());\n",
    "    mutable correct = false;\n",
    "    mutable iter = 1;\n",
    "    repeat {\n",
    "        Message($\"Trying search with {iter} iterations\");\n",
    "        GroversLoop(register, oracle, iter);\n",
    "        let res = MultiM(register);\n",
    "\n",
    "        oracle(register, output);\n",
    "        if MResetZ(output) == One {\n",
    "            set correct = true;\n",
    "            set answer = ResultArrayAsBoolArray(res);\n",
    "        }\n",
    "        ResetAll(register);\n",
    "    } until (correct or iter > 10)  // The fail-safe to avoid going into an infinite loop\n",
    "    fixup {\n",
    "        set iter *= 2;\n",
    "    }\n",
    "    if not correct {\n",
    "        fail \"Failed to find an answer\";\n",
    "    }\n",
    "    Message($\"{answer}\");\n",
    "    return answer;\n",
    "}\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Return to task 3.2 of the Solving SAT with Grover's algorithm kata.](./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
}