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.18218

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

Shang-Wei Lin, Ji-Qing Yan, Yean-Ru Chen, Zhe Hou, David Sanán

quant-phSubmitted Apr 20, 2026• Announced Apr 21, 2026• 0 citations
arXivHTMLPDF

Abstract

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.

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

qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

Abhoy Kole, Mohammed Elkacem Djeridane, Lennart Weingarten +2 more

The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime in several instances. In this work, we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover’s algorithm. The Exclusive-Sum-of-Product (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover’s iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open source Qiskit platform and IBM quantum computer.

arXiv:2409.03917•ACM Journal on Emerging Technologies in Computing Systems•Apr 10, 2025•1 citation

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 Computing Approach for Solving Exactly-1 3-SAT Using Grover's Algorithm

E. Afreen Banu, Amol Atmaram Dhumal, Lukesh Kadu +3 more

This study investigates the application of quantum computing to the Boolean satisfaction problem (SAT), with a special focus on the special case of the Exactly-1 3-SAT problem. Quantum computing has shown significant advantages in solving various computational problems and achieving exponential accelerations. This study designs and implements a quantum algorithm to identify assignments that prove Boolean formulas of bound form using the Grover search algorithm. We tested the implementation of three quantum circuits using as many quantum techniques as possible using the IBM quantum simulator. Only the second implementation showed consistent results due to the number of qubits, decoherence time, and circuit complexity. This study demonstrates that the design of algorithms meets hardware constraints and lays the foundation for future research as quantum devices improve.

International Conference for Advancement in Technology (ICONAT)•Sep 19, 2025•0 citations

Quantum Algorithm for Maximum Satisfiability

Abdirahman Alasow, Marek A. Perkowski

Satisfiability (SAT) problem in engineering and computer science is to find the set of assignment values of input variables for the given Boolean function that evaluate this function to TRUE or prove that such satisfying values do not exist. For POS SAT Problem, we propose a novel quantum algorithm for the maximum satisfiability (MAX-SAT) which returns the maximum number of OR terms that are satisfied for the SAT-unsatisfiable function, providing us with the information how far the given Boolean function is from the SAT satisfaction. We use Grover's algorithm with a new block called quantum counter in the oracle circuit.

IEEE International Symposium on Multiple-Valued Logic (ISMVL)•May 1, 2022•7 citations

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

He Wang, Jinyang Yao

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.

quant-pharXiv:2604.09980•Apr 14, 2026•0 citations
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.
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.
The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential runtime in several instances. In this work, we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover’s algorithm. The Exclusive-Sum-of-Product (ESOP)-based generation of the Conjunctive Normal Form (CNF) equivalent clauses demands less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover’s iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open source Qiskit platform and IBM quantum computer.
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.
This study investigates the application of quantum computing to the Boolean satisfaction problem (SAT), with a special focus on the special case of the Exactly-1 3-SAT problem. Quantum computing has shown significant advantages in solving various computational problems and achieving exponential accelerations. This study designs and implements a quantum algorithm to identify assignments that prove Boolean formulas of bound form using the Grover search algorithm. We tested the implementation of three quantum circuits using as many quantum techniques as possible using the IBM quantum simulator. Only the second implementation showed consistent results due to the number of qubits, decoherence time, and circuit complexity. This study demonstrates that the design of algorithms meets hardware constraints and lays the foundation for future research as quantum devices improve.
Satisfiability (SAT) problem in engineering and computer science is to find the set of assignment values of input variables for the given Boolean function that evaluate this function to TRUE or prove that such satisfying values do not exist. For POS SAT Problem, we propose a novel quantum algorithm for the maximum satisfiability (MAX-SAT) which returns the maximum number of OR terms that are satisfied for the SAT-unsatisfiable function, providing us with the information how far the given Boolean function is from the SAT satisfaction. We use Grover's algorithm with a new block called quantum counter in the oracle circuit.
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.