Assessing the Viability of Quantum SAT Solvers: A Comparative Study Using Grover’s Algorithm and Quantum Hardware
摘要
This work investigates the application of quantum computing to the Boolean Satisfiability Problem (SAT), a fundamental NP-complete problem. The study identifies two primary bottlenecks in employing Grover’s algorithm: inefficient qubit utilization and excessive quantum circuit depth. To address these challenges, three distinct quantum circuit designs based on Grover’s algorithm are proposed: a classical formulation, a depth-optimized version that reduces circuit depth, and a space-optimized version that minimizes qubit usage. These designs are evaluated using key metrics, including qubit count, circuit depth, and gate complexity, in order to assess their scalability and practical viability on both simulated and real quantum hardware. The experimental results indicate that, at present, only the classical formulation is executable on real quantum devices–and only for highly simplified problem instances. These findings underscore the current limitations of Noisy Intermediate-Scale Quantum (NISQ) systems. Nevertheless, the proposed approaches suggest that solving SAT on qubit-constrained quantum hardware may become feasible, provided gate errors are reduced and coherence times are extended.