TY - GEN
T1 - A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
AU - Lin, Shang Wei
AU - Wang, Tzu Fan
AU - Chen, Yean Ru
AU - Hou, Zhe
AU - Sanán, David
AU - Teo, Yon Shin
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024
Y1 - 2024
N2 - 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 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 prove the correctness of our approaches and evaluate them in simulations and real quantum computers.
AB - 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 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 prove the correctness of our approaches and evaluate them in simulations and real quantum computers.
UR - http://www.scopus.com/inward/record.url?scp=85192253577&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85192253577&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-57249-4_18
DO - 10.1007/978-3-031-57249-4_18
M3 - Conference contribution
AN - SCOPUS:85192253577
SN - 9783031572487
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 363
EP - 382
BT - Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings
A2 - Finkbeiner, Bernd
A2 - Kovács, Laura
PB - Springer Science and Business Media Deutschland GmbH
T2 - 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Y2 - 6 April 2024 through 11 April 2024
ER -