Quantum hybrid algorithm for solving SAT problem

https://doi.org/10.1016/j.engappai.2023.106058Get rights and content

Abstract

Combinatorial problems usually have a large search space, and almost all classical algorithms for solving this class of problems are inefficient for real-life input sizes. Quantum algorithms have been introduced with the aim of reducing computational time. In addition, to speed up the computation while solving combinatorial problems, another approach is to reduce the search space and focus on a restricted area. In this work, we study a parameter that helps reduce the search space for the solution to the satisfiability problem (SAT). We propose an approach based on Grover’s algorithm that considers the defined parameter to reduce the search space for the solution of the SAT problem. Our algorithm has a complexity of the order O(N/S), or O(N/lS) if there are l good solutions among the initial solutions, with N the number of potential solutions and S the reduction or subdivision factor of the space.

Introduction

Quantum computing consists of developing algorithms inspired by the properties of quantum physics such as superposition and entanglement. This new generation of algorithms is capable of solving most difficult problems for classical supercomputers with great efficiency. Among these difficult problems, there are combinatorial optimization problems.
Combinatorial optimization problems, especially the satisfiability (SAT) problem, find their applications in several areas of life such as social networks (Jabbour et al., 2020), the design of computer systems (Nam et al., 2018, Bryant and Heule, 2021, He et al., 2018, Khurshid and Marinov, 2004, Tucker et al., 2007), planning (Gasquet et al., 2018, Froleyks et al., 2021, Erós et al., 2021), pedigree consistency checking (Konovalenko, 2019), generation of test pattern used for digital systems (Stava, 2021), design debugging and diagnosis (Gaber et al., 2020), integrated circuit design (McGeer et al., 1991), identification of functional dependencies in boolean functions (Dixit and Kolaitis, 2019), diabetes detection and bioinformatic (Kasihmuddin et al., 2018, Luo et al., 2022), just to name a few.
Solving combinatorial problems requires a factorial time, which remains a challenge on classical computers, even for small real-life input sizes, due to the search space of solutions, which in general is very large. Most of the existing classical algorithms are known to have factorial complexity, and therefore they are inefficient. This limitation has fostered the development of several quantum algorithms for combinatorial optimization problems.
One of the largely used algorithms that has been the basis of several others is Grover’s algorithm. It allows us to find a good solution with a complexity of O(N) against O(N) classically, with N the total number of elements or potential solutions. Several Grover-based quantum algorithms have been developed to solve combinatorial problems, including the 3 -SAT problem (Yang et al., 2009, Cheng and Tao, 2007, Leporati and Felloni, 2007, Zhang et al., 2020, Campos et al., 2021, Fernandes and Dutra, 2019). But most of these algorithms based on Grover start with a uniform superposition of all the potential solutions or elements and work on the principle of amplification, which consists of augmenting the amplitude of the good solution compared to the others.
The fact that there is equiprobability or a uniform superposition requires many iterations before finding the good solution, and the quantum state thus obtained by superposition must follow a law of unitarity of the norm. However, the computation time can be reduced by searching for the right search space of the solution. In fact, a good technique for solving combinatorial problems is the preliminary study of parameters that can reduce the search space. Such a reduction of the search space can disturb the uniformity of the initial superposition, and consequently speed up the computation. Thus, the objective of this work is to decrease the computation time of algorithms for combinatorial optimization problems by introducing a disturbance of the initial uniform superposition. By applying the same technique, a data parallelism approach in Grover’s algorithm is described.
The remainder of this paper is organized as follows. Section 2 presents the basics of quantum computing. Section 3 summarizes the related work and our contributions. Section 4 presents the SAT problem and in Section 5 introduces a factor that can influence the solution of the SAT problem. Section 6 presents the Grover algorithm and Section 7 presents the proposed algorithm and studies its complexity. The Section 8 is dedicated to the results and discussions, and finally Section 9 concludes the article and provides future research directions.

Section snippets

Quantum computation

The smallest unit of information in quantum computing is called the qubit. To represent the behavior of quantum phenomena, Dirac introduced an adapted notation (Munoz and Delgado, 2016) to describe the states of quantum systems and the transformations that act on them. This notation is called the bra/ket notation. The bit in classical computation takes two possible values, 0 and 1. In contrast, in quantum computing (QC), the quantum bit takes the value |0〉 (Dirac notation) for 0 and |1〉 for 1

Related works

The SAT problem has been widely discussed in the scientific literature. It is a combinatorial problem of great theoretical and practical interest. Like all combinatorial problems, finding a solution is a time-consuming operation, which increases factorially with the size of inputs. It is one of the first problems to be recognized as NP-Complete (Cook, 1971). Because of its practical interest, several methods have been proposed for its resolution, both classical and quantum based.
A k-SAT problem

SAT problem

Let x1,x2,…,xn be binary variables that take the value 0 or 1. And let ¬, ∨, and ∧ be the logical NOT operator, the logical OR connector, and the logical AND connector, respectively.

Definition 1

A literal is a variable x or its negation ¬x. A clause is a disjunction of literals C=(x1∨⋯∨xn), with each variable xi, where i=1,…,n, which can be represented or replaced by its opposite ¬xi or may not exist.

Definition 2

A SAT problem or a Boolean satisfiability problem is defined by a formula F consisting of conjunctions of a

Study of the influence factor of the SAT solution

In this section, we first study a factor that affects the position of the solution of the SAT problem to reduce the search space. We are looking for a way to decrease or divide the search space that will guide the decrease in the amplitude of the potential bad solutions and the increase in the amplitude of the potential good ones.
The following observations are made:
  • •
    Case 1: All variables are positive. For an SAT problem where all variables are positive, that is, without ¬xi, a solution is the

Grover algorithm

The Grover algorithm is a search algorithm that allows you to find one or more elements, for example w, that meet a given criterion in an unsorted list of N elements.
A typical example is the search in a database, or a telephone directory, of the name that corresponds to a given telephone number.
By exploiting quantum properties, the Grover algorithm uses a quantum oracle to achieve its goals. This oracle efficiently checks whether an element respects a given search criterion or not (see Fig. 1).

Proposed algorithm

In this section, we present the generalized principle of the quantum approach adapted to the solution of combinatorial problems.
In the following we consider that the given combinatorial problem has at least one good solution, namely |w〉, among N possible solutions |0〉,|1〉,…,|w〉,…,|N−1〉.
The Grover algorithm (see Section 6) for finding the correct solution starts by making a uniform superposition, as shown in Fig. 5. The search space is materialized by {|0〉,|1〉,…,|w〉,…,|N−1〉} or simply {0,1,…,w,⋅,

Results and discussions

To test the performance of the proposed algorithm, it is implemented concurrently with the original Grover algorithm. The tests are performed on the 32 qubits IMB QASM quantum simulator and the results are obtained after 1024 shots on an Intel© Pentium© CPU 2020M @ 2.40 GHz × 2, memory 4 GiB, with a Linux Mint 20.1 Cinnamon as operating system.
Tests are performed on SAT problems with 4 variables. The limitation in terms of variables is due to the QASM simulator that can support up to only 5

Conclusion

This work introduced an efficient algorithm for solving combinatorial problems based on quantum properties such as superposition of states. Combinatorial problems are problems that have a very large search space for the solution. The proposed algorithm uses a technique of reduction or subdivision of the search space in order to reduce the number of computations. This is done by introducing a uniform amplitude perturbation that aims to reduce or cancel the amplitudes of some solutions while

CRediT authorship contribution statement

Charles Moudina Varmantchaonala: Conceptualization, Methodology, Software, Writing – original draft. Jean Louis Kedieng Ebongue Fendji: Conceptualization, Methodology, Validation, Writing – review & editing, Supervision. Jean Pierre Tchapet Njafa: Methodology, Validation, Writing – review & editing. Marcellin Atemkeng: Validation, Writing – review & editing.

Declaration of Competing Interest

The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

Acknowledgment

We thank Pr. Serge Guy NANA ENGO for his helpful discussions and remarks.

References (61)

Cited by (5)

View full text
© 2023 Elsevier Ltd. All rights reserved.