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.
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.
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.
The Boolean Satisfiability (SAT) problem is a canonical NP-complete problem and a natural candidate for quantum acceleration via search-based algorithms. In Grover-based quantum SAT solvers, the dominant computational cost stems from the construction of a reversible oracle that evaluates the Boolean formula, rendering the choice of SAT encoding crucial for overall quantum resource efficiency. Although SAT instances are conventionally expressed in Conjunctive Normal Form (CNF), such encodings typically translate into quantum circuits with significant qubit overhead and high non-Clifford gate complexity.
In this work, we investigate an Exclusive-Sum-of-Products (ESOP)-based CNF (e-CNF) representation tailored for quantum SAT solving and analyze its impact on oracle construction. We derive tighter upper bounds on qubit requirements and Clifford+T gate counts for Grover-based SAT solvers when e-CNF encodings are employed in place of standard CNF. In addition, we propose a scalable transformation from Boolean formulas to e-CNF and present a systematic procedure for interpreting e-CNF representations as reversible quantum circuits suitable for oracle implementation. Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources, including qubit count, T-gate complexity, and circuit depth, when compared to CNF-based oracle constructions. These results establish e-CNF as an effective quantum-aware SAT encoding that significantly improves the practicality of oracle-based quantum SAT solving.
The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.
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) 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ϵ) (for any ϵ>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.
This study explores how well Grover's Algorithm performs in solving the Boolean Satisfiability Problem (SAT) using quantum circuits. The algorithm is implemented with IBM's Qiskit framework and compared to classical brute-force methods. Experiments focus on 3-SAT, 4-SAT, and 5-SAT problems, using quantum simulators and IBM quantum hardware. The results show that Grover's Algorithm is more efficient, offering a theoretical quadratic speedup over classical methods. However, practical issues like limited qubit availability, hardware noise, and optimization challenges impact its current performance. The data highlights the potential for quantum computing to scale and solve NP-complete problems. This research shows how quantum computing can improve problem-solving and lays the groundwork for future studies on more complex SAT problems and advanced quantum hardware.
Formal verification of power side-channel leakage and its countermeasures in cryptographic algorithms is challenging, as SAT-based methods fail to scale on XOR-heavy, time-unrolled cryptographic circuits with realistic leakage models. We construct compact Conjunctive Normal Form (CNF) cases modeling one-bit leakage under two-trace conditions, linking key dependence and state evolution. Classical solvers quickly reach complexity limits, so we propose Q-LEAK, a quantum-based verification approach using Grover's algorithm, compiling each CNF into an oracle and applying amplitude amplification to search in O(sqrt(N)) oracle calls, with oracles that encode the two-trace leakage predicate and the CNF constraints. Benchmarking against classical SAT shows both potential gains and practical resource limits. In noiseless tests on 5-7 variable benchmarks, Q-LEAK consistently recovered a satisfying assignment within 1-4 tries, with marked bitstrings amplified clearly above the background distribution, exceeding 20 percent probability. The evaluation of Q-LEAK on real quantum hardware revealed at least one classically verified SAT assignment, despite the presence of noise. These results point to a potential path toward quantum-assisted verification of side-channel protections.