Quantum computers promise to allow for great improvements in the solution of -SAT problem, determining whether a set of clauses with variables have a satisfiable boolean assignment, which is one of the fundamental problems of computational logic. Given the recent advancements of quantum computers, we argue that they allow for great improvements in solving the -SAT problem. In order to evaluate this possibility, in this work, we generalized a pre-existing quantum 3-SAT solver [1] to the most general case for the number of variables, clauses, and , using the IBM Qiskit library [2]. We extended basic gates and steps of the underlying algorithm to reduce the number of used qubits and gates, in order to deal with the decoherence problem [3]. We tested our solution on complex instances of -SAT, which preserved the exponential speedup promised by Grover algorithm [4].
Quantum computing has demonstrated promising results in several areas of computer science and is changing our way of studying algorithms in the following years.
One of the areas that could drastically be touched by the efects of quantum computing is Logic, in particular, the question of equivalence of the and classes. Answering this question will have a powerful impact on areas such as artificial intelligence and security.
-SAT problem—determining whether a given set of clauses have a satisfiable assignment—is
one of the fundamental problems of computational logic, and the first problem proven to be
NP-complete [
This paper evaluates the application of quantum computing to solve arbitrary instances of
the Exactly-1 -SAT problem and to show the enhancements provided by a quantum solver (an
exactly-1 -SAT problem is one where there exists a satisfying assignment with exactly one true
literal in each of the clauses). We discovered the quantum solver introduced by Nannicini [
The rest of this paper is structured as follows: Section 2 reviews state of the art; Section 3 provides preliminary background; Section 4 presents our approach; Section 5 reports the evaluation procedure and its results; finally, Section 6 draws some conclusions and possible future works.
As mentioned earlier, one of the most interesting questions of quantum computing is whether it can prove the equivalence of the and classes.
Grover search algorithm is an important asset to approach this question because it is used to
solve several or -complete problems with considerably reduced computational eforts.
For example, database search problem has improved with Grover’s quadratic speedup as reported
in [
These examples are all indicators of how Grover could be useful to solve other logic problems,
such as the one we are tackling. For instance, an interesting recent work by Porfiris [
This paper relies on the work by Nannicini [
In this section, we explain our implemented generalization of Nanncini’s solver to manage arbitrary numbers of variables and clauses for an Exactly-1 k-SAT problem, by maintaining the structure of the three steps explained in Section 3 and focusing on the following two aspects:
Considering a problem with variables and clauses, the total required qubits in its representing circuit includes for variables, one for the output register, and for clauses. Additionally, the Problem Encoding Step and the Inversion about the Average Step need an dimensional controlled NOT gate for the exploitation of the amplitude amplification principle. However, Qiskit does not allow us to build controlled-NOT gates with dimensions larger than two, and we had to solve this issue by using the smallest number of qubits possible. To realize such gate we concatenate the results of doubly controlled-NOT gates applied on two of the qubits at a time thus introducing additional − 2 ancillary qubits.
Algorithm generalization Provided the preliminaries on the number of qubits, we discuss our implementation in the rest of this section through an illustrative example of an Exactly-1 4-SAT problem with four variables and four clauses. To formalize an exactly-1 k-SAT problem we need to specify the variables on which it is defined, the clauses and the maximal length of the clauses. In the rest of this paper we call the set of the variables of the problem, the set of the clauses and for each clause we define the variables that compose it with their respective polarity. The number of variables in the clauses will never exceed the number k decided, the cardinality of is and the cardinality of is m. In the end remember that this formulation can also be seen as the Conjunctive Normal Form (CNF) of the clauses defined. This representation allows to visualize better the possible solution of the problem and understand a-priori if a solution actually exists.
Hence, the formalization of the exactly-1 4-SAT problem with four variables ( = { 1, 2, 3, 4}) and four clauses ( = { 1, 2, 3, 4}) is: That can be expressed in the CNF as:
≡ ( 1 ∨ 2 ∨ 3 ∨ 4) ∧ ( 1 ∨ 2 ∨ 4) ∧ ( 1 ∨ 2 ∨ 3 ∨ 4) ∧ ( 2 ∨ 3 ∨ 4) We can now list the steps of the generalized algorithm: a. Initialization Step: the initial state of the quantum circuit is set by applying Hadamard gates for each variable and for the output, in order to bring it to the uniform superposition. b. Problem Encoding Step: each clause is encoded in the circuit using gates that allow to bit-flip the qubit corresponding to the clause if and only if it has exactly one true literal (this is the definition of searching for a solution of an Exactly-1 k-SAT problem). Considliteral in the problem. First we bring each variable to ering 1, we want to flip the qubit 10 if and only if 1 ∨ 2 ∨ 3 ∨ 4 by using NOT gates and apply a CNOT of all the variables so that we obtain | 10⟩ = | 10 ⊕ 1 ⊕ 2 ⊕ 3 ⊕ 4⟩. To complete the double implication of flipping 10 for the exactly one true variable, we need a quadruply controlled NOT gate between the four variables targeting 10. Finally we have obtained | 10⟩ = | 10 ⊕ 1 ⊕ 2 ⊕ 3 ⊕ 4 ⊕ ( 1 ∧ 2 ∧ 3 ∧ 4)⟩. Hence, the theoretical circuit that we should realize is showed in the following Figure 1. has exactly one true 10
with their respective polarity | 0⟩ | 1⟩ | 2⟩ | 3⟩ | 00⟩ | 10⟩
However, as we mentioned before, we are not allowed to realize multiply controlled-NOT gates in Qiskit. The procedure that we adopted to encode such gate in the actual quantum circuit is shown in Figure 2. We can see here how ancillary qubits are used to concatenate the results of the doubly controlled-NOT gates and, after the result is stored in 10, we reset the state of these qubits applying once more the same doubly controlled-NOT gates. c. Inversion About the Average Step: in this last step, we modify the coeficients corresponding to the correct solution by applying the unitary operation defined as follows:
= (− ⨂ ) (⨂
) where is the number of variables and is a diagonal matrix (−1, 1, ⋯ , 1) of size 2 . In particular, to realize we needed once more to generalize the algorithm since it consists of a ( − 1)-controlled NOT gate between the first − 1 variables, targeting the last one. As shown in Figure 3, we exploited the same trick to deal with Qiskit’s limitation. Moreover, we see the measurement of the four qubits representing the state, brought to the classical register 0 which stores the final solution. Algorithm specifics The problems are fed to the solver in an input file when running the program. Variables have to be specified with the following notation: followed by the integer that identifies that variable (variable 1 will be 1). If we want to use variables, we can define -es from = 1 up to = ; it is not allowed to define a number of diferent variables with pedices not in the range [1, ]. Each line contains the definition of a clause, line 1 will define clause 1, line 2 corresponds to 2 and so on. Variables in the clauses have to be specified in ascending order, to express the negative polarity a minus sign (−) precedes the respective . Considering the Exactly-1 4-SAT defined in this section, with four variables and four clauses, the file containing its definition (let us call it sat4) will have the following shape:
Additionally, the solver also gets the iteration number of the Problem Encoding and the Inversion About the Average steps as input. The number of times that we run Grover’s algorithm influences the results provided by the solver.
Grover iterations In his original work, Grover [
We evaluated our proposed quantum solver with arbitrary and values up to the 4-SAT problem and achieved correct solutions with very high probability. The results shown in this section are generated by the quantum simulator of the Qiskit library since the execution on real quantum devices is still not possible for such complex instances of the SAT problem. Quantum simulators execute the algorithm on a hardware where noise is minimal, hence allowing to use significant numbers of qubits and gates to implement the algorithms. We have to take this into account when consulting the results on the histograms, being conscious that very high probabilities make us expect that the correct results will be also displayed on the real quantum device since the additional noise introduced is not enough to compromise the execution. To show the results provided by our solver we decided also to highlight the number of iterations needed to find the best solution on each particular problem. As we have already discussed, the number of iterations afects significantly the results; in order to make this evident we will first present the solution obtained with the best number of iterations and then compare it with the results provided if we tried to increase by one this number. We will call the result with the best number of iterations Best solution while the one with one additional repetition as the Next solution. In the Next solution we see that the probability distribution changes a lot, in particular the correct solution drastically decreases its value and random other incorrect combinations increase their probability.
We start with the same problem described by Nannicini in his work [
Problem 1 Consider the 3-SAT problem defined over the set of variables = { 1, 2, 3} and the three clauses = { 1, 2, 3}, such that: 1 = { 1, 2, 3} 2 = { 1, 2, 3} 3 = { 1, 2, 3} The formulation of the problem implies that the solution is = { 1, 2, 3}.
(a) Problem 1 best solution (b) Problem 1 next solution
The result of our solver, shown in Figure 5a, provides the same solution as with a probability near 95%, which is a very promising result and consistent with the one by Nannicini. Figure 5a shows the best solution obtained with 2 iterations of Grover’s algorithm. Comparing it with Figure 5b, obtained with 3 iterations, we see that the probability of the correct solution decreases of around the 60%. In addition, all the other combinations of variables have increased their probability rounding all near the 10% which is very close to the 30% of 101. Problem 2 Consider the 3-SAT problem defined over the set of variables = { 1, 2, 3} and the three clauses = { 1, 2, 3}, such that: 1 = { 1, 2, 3} 2 = { 1, 2, 3} 3 = { 1, 2, 3} This problem seems to be trivially satisfiable, for example, with = { 1, 2, 3}. However, this is not a solution for the Exactly-1 formulation since both 1 and 3 in the second clause make the disjunction true. Thus, the Exactly-1 Problem 2 has no solution.
The result of our solver, shown in Figure 6, confirms the lack of an acceptable answer as the probabilities of all the possible solutions are very close (i.e. around 10% each), which does not allow to choose between one of them.
Problem 3 Consider the 3-SAT problem defined over the set of variables = { 1, 2, 3, 4, 5} and the five clauses = { 1, 2, 3, 4, 5}, such that: 1 = { 1, 2, 3} 2 = { 2, 3, 4} 3 = { 3, 4, 5} 4 = { 4, 5, 1} 5 = { 5, 3, 4} Again, the formulation of the problem suggests the solution to be = { 1, 2, 3, 4, 5}. (a) Problem 3 best solution (b) Problem 3 next solution
The Best solution of our solver (obtained with 3 iterations), shown in Figure 7a, is 11111 which is the same as the expected result . As the figure shows, the answer is provided with a probability of near the 40% which is significantly higher than all the other 5 qubits combinations. In this case, the probability of the Next solution (Figure 7b obtained with 4 iterations) decreases of 15% for the correct result and for the other combinations it distributes the remaining probability; in particular for 00100 that reaches a value around the 16%.
Problem 4 Consider the problem presented in Section 4 which is a 4-SAT problem defined over the set of variables = { 1, 2, 3, 4} and the four clauses = { 1, 2, 3, 4}, such that: 1 = { 1, 2, 3, 4}
2 = { 1, 2, 4} 3 = { 1, 2, 3, 4}
4 = { 2, 3, 4} The formulation of the problem points to = { 1, 2, 3, 4} as the expected solution. (a) Problem 4 best solution (b) Problem 4 next solution
The result from our solver, as shown in figure 8a, is the string 1111 with a probability near 90%, significantly higher than all the other probabilities and conforms to the expected solution. Comparing the Best solution in Figure 8a (obtained with 3 cycles) with the Next one (obtained with 4 cycles) in Figure 8b we see that the probability distribution maintains the same shape and equally spreads on all the other incorrect combinations increasing for each up to around the 3%. The correct solution is still higher than all the other probabilities but decreased of 35% with respect to the one obtained with the best number of iterations.
The Exactly-1 k-SAT problem has a fundamental importance in computational theory. The proposed solver in this paper can tackle any instance of this problem with arbitrary numbers of variables, clauses, and with quadratic speedup, thanks to Grover’s search algorithm.
The four instances reported here are the most significant to show the behavior of the solver. The first three show how it works with more than just three variables and clauses, on the Exactly-1 3-SAT problem which is the most popular in applications. The obtained results seem very promising, as the probability of the correct solution is significantly higher than all the others; we believe that the same results will be obtained also on a real quantum device where the noise is not mitigated as in a simulated computation. The generalization has been tested also on Problem 4 that considers four variables and clauses with a maximal length = 4. Also in this case, the correct solution has probability around 90%, definitely better than all the other combinations.
We compared the Best and the Next solutions and deduced that the correct iteration number for the second and third steps of Grover’s algorithm depends on the complexity of the problem. It is coherent with what these steps do, which is increasing the coeficients of the correct solution. Hence, more complex instances correspond to more possible solutions, and therefore, the probability spreads on a larger set of qubits combinations; more iterations allow for a larger detach between the probability of the correct solution and others. The simple instances studied by Nannicini in his work required at most two iterations while in our study we discovered that already an Exactly-1 3-SAT with five variables and five clauses as well as Problem 4 executes at best with 3 iterations. As future work, we plan to determine the relationship between the complexity of an Exactly-1 k-SAT problem and the best number of iterations, hence a formula that finds the cycles once we provide , and .
The reported histograms are the result of the execution on the qasm_simulator provided by Qiskit which allows for high number of qubits. As we mentioned before, we can conclude that our work will also provide correct results on real quantum devices, given to the high probabilities that we have obtained. We tried to execute the problems also on a real quantum device, in particular ibmq_16_melbourne provided by IBM-Quantum experience. All the executions fail because of the transpilation function of Qiskit. It optimizes the encoding of the quantum algorithm on the real device, trying to reduce the number of qubits needed, adding gates to perform the same quantum operations. For complex algorithms like the one that we implemented, the transpilation has two main issues: (i) adding more gates causes the decoherence problem, and (ii) the huge number of gates which leads to the error reported by the machine. We obtain a too long circuit that needs an execution time greater than the circuit repetition rate.
The current state of quantum technology does not tackle this issue, as the most powerful quantum machine provided by the library that we used is the ibmq_16_melbourne.