Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2604.09980

A parallel and distributed fixed-point quantum search algorithm for solving SAT problems

He Wang, Jinyang Yao

quant-phSubmitted Apr 11, 2026• Announced Apr 14, 2026• 0 citations
arXivHTMLPDF

Abstract

Boolean satisfiability (SAT) problem is of fundamental importance in computer science and many application domains. For Grover's algorithm, solving the SAT problem requires $\mathcal{O}(\sqrt{2^n})$ queries--where n denotes the number of logic variables in the problem. However, Grover's algorithm suffers from the Souffle problem: specifically, when the number of solutions is unknown, terminating the algorithm too early or too late leads to a significant reduction in the probability of obtaining a solution. In this paper, we propose a parallel fixed-point (PFP) search algorithm to solve the SAT problem. By exploiting entanglement, each clause in the conjunctive normal form (CNF) formula can be processed independently, leading to a significant reduction in circuit depth. We also discuss how to perform the algorithm in distributed manner. These make the PFPS algorithm particularly suitable for the noisy intermediate-scale quantum (NISQ) era.

Related papers

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation

Shang‐Wei Lin, Tzu‐Fan Wang, Yean-Ru Chen +3 more

Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover's algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexity O(m) -- linear to the number of clauses m -- per Grover iteration. In this work, we develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We have proved the correctness of our approaches and demonstrated them in simulations.

arXiv:2308.03344•Aug 7, 2023•0 citations

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation

Shang‐Wei Lin, Tzu‐Fan Wang, Yean-Ru Chen +3 more

Abstract Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover’s algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexityO(m), linear to the number of clausesm,per Grover iteration. In this work, we develop aparallelquantum SAT solver, which reduces the time complexity in each iteration to constant timeO(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We prove the correctness of our approaches and evaluate them in simulations and real quantum computers.

Lecture notes in computer science•Jan 1, 2024•2 citations

Quantum logic synthesis for Satisfiability Problems.

Shuai Yang, Wei Zi, Bujiao Wu +3 more

To demonstrate the advantage of quantum computation, many attempts have been made to attack classically intractable problems, such as the satisfiability problem (SAT), with quantum computer. To use quantum algorithms to solve these NP-hard problems, a quantum oracle with quantum circuit implementation is usually required. In this manuscript, we first introduce a novel algorithm to synthesize quantum logic in the Conjunctive Normal Form (CNF) model. Compared with linear ancillary qubits in the implementation of Qiskit open-source framework, our algorithm can synthesize an m clauses n variables k-CNF with $O(k^2 m^2/n)$ quantum gates by only using three ancillary qubits. Both the size and depth of the circuit can be further compressed with the increase in the number of ancillary qubits. When the number of ancillary qubits is $\Omega(m^\epsilon)$ (for any $\epsilon > 0$), the size of the quantum circuit given by the algorithm is O(km), which is asymptotically optimal. Furthermore, we design another algorithm to optimize the depth of the quantum circuit with only a small increase in the size of the quantum circuit. Experiments show that our algorithms have great improvement in size and depth compared with the previous algorithms.

•Jan 14, 2021•1 citation

Solving the integer case constraint satisfiability problem using Grover's algorithm

Gayathree M. Vinod, Anil Shaji

Constraint satisfiability problems, crucial to several applications, are solved on a quantum computer using the Grover's search algorithm, leading to a quadratic improvement over the classical case. The solutions are obtained with high probability for several cases and are illustrated for the cases involving 2 variables for both 3-bit and 4-bit numbers. Methods are defined for inequality comparisons and these are combined according to the form of the satisfiability formula, to form the oracle for the algorithm. The circuit is constructed using IBM Qiskit and is verified on an IBM simulator. It is further executed on one of the Noisy Intermediate-Scale Quantum (NISQ) processors from IBM on the cloud. Noise levels in the processor at present are found to be too high for successful execution. Running the algorithm on the simulator with a custom noise model lets us identify the noise threshold for successful execution.

•Jun 18, 2021•0 citations

Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

Shang-Wei Lin, Ji-Qing Yan, Yean-Ru Chen +2 more

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.

quant-pharXiv:2604.18218•Apr 21, 2026•0 citations

Finding Solutions to the Integer Case Constraint Satisfiability Problem Using Grover’s Algorithm

Gayathree M. Vinod, Anil Shaji

Constraint satisfiability problems, crucial to several applications, are solved on a quantum computer using Grover's search algorithm, leading to a quadratic improvement over the classical case. The solutions are obtained with high probability for several cases and are illustrated for the cases involving two variables for both 3- and 4-bit numbers. Methods are defined for inequality comparisons, and these are combined according to the form of the satisfiability formula, to form the oracle for the algorithm. The circuit is constructed using IBM Qiskit and is verified on an IBM simulator. It is further executed on one of the Noisy Intermediate-Scale Quantum (NISQ) processors from IBM on the cloud. Noise levels in the processor at present are found to be too high for successful execution. Running the algorithm on the simulator with a custom noise model lets us identify the noise threshold for successful execution.

arXiv:2106.09976•IEEE Transactions on Quantum Engineering•Jan 1, 2021•12 citations
Boolean satisfiability (SAT) problem is of fundamental importance in computer science and many application domains. For Grover's algorithm, solving the SAT problem requires O(2n)\mathcal{O}(\sqrt{2^n})O(2n​) queries--where n denotes the number of logic variables in the problem. However, Grover's algorithm suffers from the Souffle problem: specifically, when the number of solutions is unknown, terminating the algorithm too early or too late leads to a significant reduction in the probability of obtaining a solution. In this paper, we propose a parallel fixed-point (PFP) search algorithm to solve the SAT problem. By exploiting entanglement, each clause in the conjunctive normal form (CNF) formula can be processed independently, leading to a significant reduction in circuit depth. We also discuss how to perform the algorithm in distributed manner. These make the PFPS algorithm particularly suitable for the noisy intermediate-scale quantum (NISQ) era.
Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover's algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexity O(m) -- linear to the number of clauses m -- per Grover iteration. In this work, we develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We have proved the correctness of our approaches and demonstrated them in simulations.
Abstract Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover’s algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexityO(m), linear to the number of clausesm,per Grover iteration. In this work, we develop aparallelquantum SAT solver, which reduces the time complexity in each iteration to constant timeO(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We prove the correctness of our approaches and evaluate them in simulations and real quantum computers.
To demonstrate the advantage of quantum computation, many attempts have been made to attack classically intractable problems, such as the satisfiability problem (SAT), with quantum computer. To use quantum algorithms to solve these NP-hard problems, a quantum oracle with quantum circuit implementation is usually required. In this manuscript, we first introduce a novel algorithm to synthesize quantum logic in the Conjunctive Normal Form (CNF) model. Compared with linear ancillary qubits in the implementation of Qiskit open-source framework, our algorithm can synthesize an m clauses n variables k-CNF with O(k2m2/n)O(k^2 m^2/n)O(k2m2/n) quantum gates by only using three ancillary qubits. Both the size and depth of the circuit can be further compressed with the increase in the number of ancillary qubits. When the number of ancillary qubits is Ω(mϵ)\Omega(m^\epsilon)Ω(mϵ) (for any ϵ>0\epsilon > 0ϵ>0), the size of the quantum circuit given by the algorithm is O(km), which is asymptotically optimal. Furthermore, we design another algorithm to optimize the depth of the quantum circuit with only a small increase in the size of the quantum circuit. Experiments show that our algorithms have great improvement in size and depth compared with the previous algorithms.
Constraint satisfiability problems, crucial to several applications, are solved on a quantum computer using the Grover's search algorithm, leading to a quadratic improvement over the classical case. The solutions are obtained with high probability for several cases and are illustrated for the cases involving 2 variables for both 3-bit and 4-bit numbers. Methods are defined for inequality comparisons and these are combined according to the form of the satisfiability formula, to form the oracle for the algorithm. The circuit is constructed using IBM Qiskit and is verified on an IBM simulator. It is further executed on one of the Noisy Intermediate-Scale Quantum (NISQ) processors from IBM on the cloud. Noise levels in the processor at present are found to be too high for successful execution. Running the algorithm on the simulator with a custom noise model lets us identify the noise threshold for successful execution.
Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.
Constraint satisfiability problems, crucial to several applications, are solved on a quantum computer using Grover's search algorithm, leading to a quadratic improvement over the classical case. The solutions are obtained with high probability for several cases and are illustrated for the cases involving two variables for both 3- and 4-bit numbers. Methods are defined for inequality comparisons, and these are combined according to the form of the satisfiability formula, to form the oracle for the algorithm. The circuit is constructed using IBM Qiskit and is verified on an IBM simulator. It is further executed on one of the Noisy Intermediate-Scale Quantum (NISQ) processors from IBM on the cloud. Noise levels in the processor at present are found to be too high for successful execution. Running the algorithm on the simulator with a custom noise model lets us identify the noise threshold for successful execution.