{
"cells": [
{
"cell_type": "markdown",
"metadata": {
"tags": [
"remove_cell"
]
},
"source": [
"# Solving Satisfiability Problems using Grover's Algorithm"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this section, we demonstrate how to solve satisfiability problems using the implementation of Grover's algorithm in Qiskit Aqua. "
]
},
{
"cell_type": "markdown",
"metadata": {
"tags": [
"contents"
]
},
"source": [
"## Contents\n",
"\n",
"1. [Introduction](#introduction)\n",
"2. [3-Satisfiability Problem](#3satproblem)\n",
"3. [Qiskit Implementation](#implementation)\n",
"4. [Problems](#problems)\n",
"5. [References](#references)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## 1. Introduction \n",
"\n",
"Grover's algorithm for unstructured search was introduced in an [earlier section](https://qiskit.org/textbook/ch-algorithms/grover.html), with an example and implementation using Qiskit Terra. We saw that Grover search is a quantum algorithm that can be used to search for solutions to unstructured problems quadratically faster than its classical counterparts. Here, we are going to illustrate the use of Grover's algorithm to solve a particular combinatorial Boolean satisfiability problem.\n",
"\n",
"In computer science, the Boolean satisfiability problem is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. This can be seen as a search problem, where the solution is the assignment where the Boolean formula is satisfied.\n",
"\n",
"For _unstructured_ search problems, Grover’s algorithm is optimal with its run time of $O(\\sqrt{N}) = O(2^{n/2}) = O(1.414^n)$[2]. In this chapter, we will look at solving a specific Boolean satisfiability problem (3-Satisfiability) using Grover’s algorithm, with the aforementioned run time of $O(1.414^n)$. Interestingly, at the time of writing, the best-known classical algorithm for 3-Satisfiability has an upper-bound of $O(1.307^n)$[3]. You may have heard that Grover’s algorithm can be used to speed up solutions to NP-complete problems, but these NP-complete problems do actually contain structure[4] and we can sometimes do better than the $O(1.414^n)$ of Grover’s algorithm.\n",
"\n",
"While it doesn’t make sense to use Grover’s algorithm on 3-sat problems, the techniques here can be applied to the more general case (k-SAT, discussed in the next section) for which Grover’s algorithm can outperform the best classical algorithm. Additionally, the techniques in Grover’s algorithm can theoretically be combined with the techniques used in the classical algorithms to gain an even better run time than either individually. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## 2. 3-Satisfiability Problem \n",
"\n",
"The 3-Satisfiability (3SAT) Problem is best explained with the following concrete problem. Let us consider a Boolean function $f$ with three Boolean variables $v_1,v_2,v_3$ as below:\n",
"\n",
"\n",
"\n",
"$$f(v_1,v_2,v_3) = (\\neg v_1 \\vee \\neg v_2 \\vee \\neg v_3) \\wedge (v_1 \\vee \\neg v_2 \\vee v_3) \\wedge (v_1 \\vee v_2 \\vee \\neg v_3) \\wedge (v_1 \\vee \\neg v_2 \\vee \\neg v_3) \\wedge (\\neg v_1 \\vee v_2 \\vee v_3)$$\n",
"\n",
"\n",
"\n",
"In the above function, the terms on the right-hand side equation which are inside $()$ are called clauses; this function has 5 clauses. In a k-SAT problem, each clause has exactly k literals; our problem is a 3-SAT problem, so each clause has exactly three literals. For instance, the first clause has $\\neg v_1$, $\\neg v_2$ and $\\neg v_3$ as its literals. The symbol $\\neg$ is the Boolean NOT that negates (or, flips) the value of its succeeding literal. The symbols $\\vee$ and $\\wedge$ are, respectively, the Boolean OR and AND. The Boolean $f$ is satisfiable if there is an assignment of $v_1, v_2, v_3$ that evaluates to $f(v_1, v_2, v_3) = 1$ (that is, $f$ evaluates to True).\n",
"\n",
"A naive way to find such an assignment is by trying every possible combinations of input values of $f$. Below is the table obtained from trying all possible combinations of $v_1, v_2, v_3$. For ease of explanation, we interchangeably use $0$ and False, as well as $1$ and True. \n",
"\n",
"|$v_1$ | $v_2$ | $v_3$ | $f$ | Comment | \n",
"|------|-------|-------|-----|---------|\n",
"| 0 | 0 | 0 | 1 | **Solution** | \n",
"| 0 | 0 | 1 | 0 | Not a solution because $f$ is False | \n",
"| 0 | 1 | 0 | 0 | Not a solution because $f$ is False | \n",
"| 0 | 1 | 1 | 0 | Not a solution because $f$ is False | \n",
"| 1 | 0 | 0 | 0 | Not a solution because $f$ is False | \n",
"| 1 | 0 | 1 | 1 | **Solution** | \n",
"| 1 | 1 | 0 | 1 | **Solution** | \n",
"| 1 | 1 | 1 | 0 | Not a solution because $f$ is False | \n",
"\n",
"From the table above, we can see that this 3-SAT problem instance has three satisfying solutions: $(v_1, v_2, v_3) = (T, F, T)$ or $(F, F, F)$ or $(T, T, F)$. \n",
"\n",
"In general, the Boolean function $f$ can have many clauses and more Boolean variables. Note that 3SAT problems can be always written in what is known as conjunctive normal form (CNF), that is, a conjunction of one or more clauses, where a clause is a disjunction of three literals; otherwise put, it is an AND of 3 ORs."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## 3. Qiskit Implementation \n",
"\n",
"Let's now use Qiskit Aqua to solve the example 3SAT problem: \n",
"\n",
"\n",
"$$f(v_1,v_2,v_3) = (\\neg v_1 \\vee \\neg v_2 \\vee \\neg v_3) \\wedge (v_1 \\vee \\neg v_2 \\vee v_3) \\wedge (v_1 \\vee v_2 \\vee \\neg v_3) \\wedge (v_1 \\vee \\neg v_2 \\vee \\neg v_3) \\wedge (\\neg v_1 \\vee v_2 \\vee v_3)$$\n",
"\n",
"\n",
"\n",
"First we need to understand the input [DIMACS CNF](http://www.satcompetition.org/2009/format-benchmarks2009.html) format that Qiskit Aqua uses for such problem, which looks like the following for the problem:\n",
"\t\n",
"~~~\n",
"c example DIMACS CNF 3-SAT\n",
"p cnf 3 5\n",
"-1 -2 -3 0\n",
"1 -2 3 0\n",
"1 2 -3 0\n",
"1 -2 -3 0\n",
"-1 2 3 0\n",
"~~~\n",
"\n",
"- Lines that start with `c` are comments\n",
" - eg. `c example DIMACS CNF 3-SAT`\n",
"- The first non-comment line needs to be of the form `p cnf nbvar nbclauses`, where\n",
" - `cnf` indicates that the input is in CNF format\n",
" - `nbvar` is the exact number of variables appearing in the file\n",
" - `nbclauses` is the exact number of clauses contained in the file\n",
" - eg. `p cnf 3 5`\n",
"- Then there is a line for each clause, where \n",
" - each clause is a sequence of distinct non-null numbers between `-nbvar` and `nbvar` ending with `0` on the same line\n",
" - it cannot contain the opposite literals i and -i simultaneously\n",
" - positive numbers denote the corresponding variables\n",
" - negative numbers denote the negations of the corresponding variables\n",
" - eg. `-1 2 3 0` corresponds to the clause $\\neg v_1 \\vee v_2 \\vee v_3$\n",
"\n",
"Similarly the solutions to the problem $(v_1, v_2, v_3) = (T, F, T)$ or $(F, F, F)$ or $(T, T, F)$ can be written as `1 -2 3`, or `-1 -2 -3`, or `1 2 -3`.\n",
"\n",
"With this example problem input, we create the corresponding oracle for our Grover search. In particular, we use the LogicalExpressionOracle component provided by Aqua, which supports parsing DIMACS CNF format strings and constructing the corresponding oracle circuit."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import numpy as np\n",
"from qiskit import BasicAer\n",
"from qiskit.visualization import plot_histogram\n",
"from qiskit.aqua import QuantumInstance\n",
"from qiskit.aqua.algorithms import Grover\n",
"from qiskit.aqua.components.oracles import LogicalExpressionOracle, TruthTableOracle"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"input_3sat = '''\n",
"c example DIMACS-CNF 3-SAT\n",
"p cnf 3 5\n",
"-1 -2 -3 0\n",
"1 -2 3 0\n",
"1 2 -3 0\n",
"1 -2 -3 0\n",
"-1 2 3 0\n",
"'''"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
"oracle = LogicalExpressionOracle(input_3sat)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `oracle` can now be used to create an Grover instance:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"grover = Grover(oracle)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can then configure a simulator backend and run the Grover instance to get the assignment result:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[1, -2, 3]\n"
]
}
],
"source": [
"backend = BasicAer.get_backend('qasm_simulator')\n",
"quantum_instance = QuantumInstance(backend, shots=1024)\n",
"result = grover.run(quantum_instance)\n",
"print(result['assignment'])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"As seen above, a satisfying solution to the specified 3-SAT problem is obtained. And it is indeed one of the three satisfying solutions.\n",
"\n",
"Since we used a simulator backend, the complete measurement result is also returned, as shown in the plot below, where it can be seen that the binary strings `000`, `011`, and `101` (note the bit order in each string), corresponding to the three satisfying solutions all have high probabilities associated with them."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
"