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:2605.16202

Performance Gains in Quantum SAT Solvers Using ESOP Encoding

Majd Assaad, Abhoy Kole, Rolf Drechsler

quant-phcs.ETSubmitted May 15, 2026• Announced May 18, 2026• 0 citations
arXivHTMLPDF

Abstract

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.

Comments
18 pages, 6 figures

Related papers

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

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

SAT-Guided Conversion of Boolean Functions into Reversible Quantum Logic: Minimal Embedding, Exact Synthesis, and Cost-Aware Mapping

Chandan Bandyopadhyay, Saibal Majumder, Haresh Kumar Sharma

A classical Boolean specification need not be one-to-one, whereas every reversible quantum network must preserve distinctions between basis states. SAT-Embed-Q handles this mismatch by first constructing a partial reversible embedding from output-preimage multiplicities and then searching for a compatible mixed-polarity Toffoli network. We implemented two bounded satisfiability encodings, one tracking complete intermediate states and the other tracking individual line values, and evaluated both with a deterministic reference DPLL solver. On the four-line example F(a,b,c)=ab¯∨bc, the minimum-depth CNF contains 42,234 clauses in the direct encoding and 34,194 in the bit-level encoding. The smaller clause set did not translate into faster execution: the direct representation required less time in our solver. A separate exhaustive study of the target-preserving oracle class covers every single-output function of two and three inputs. Within that restricted class, allowing negative controls lowers the summed minimum target-gate count by 34.38% and 46.39%, respectively. We also examine two four-input functions from RevLib, for which fixing the input-preserving oracle structure leads to different gate counts from embedding-optimized benchmark circuits. These experiments characterize bounded synthesis and control-polarity choices for small functions; fault-tolerant resource optimization and large-network scalability remain outside their scope.

Quantum Reports•Oct 26, 2026•0 citations

Quantum algorithm for ESOP minimization

Hrithik Ketineni, Marek A. Perkowski

The Exclusive-OR Sum-of-Product (ESOP) minimization problem has long been of interest to the research community because of its importance in classical logic design (including low-power design and design for test), reversible logic synthesis, and knowledge discovery, among other applications. However, no exact minimal minimization method has been presented for more than seven variables on arbitrary functions. This paper presents a novel quantum-classical hybrid algorithm for the exact minimal ESOP minimization of incompletely specified Boolean functions. This algorithm constructs oracles from sets of constraints and leverages the quantum speedup offered by Grover's algorithm to find solutions to these oracles, thereby improving over classical algorithms. Improved encoding of ESOP expressions results in substantially fewer decision variables compared to many existing algorithms for many classes of Boolean functions. This paper also extends the idea of exact minimal ESOP minimization to additionally minimize the cost of realizing an ESOP expression as a quantum circuit. To the extent of the authors' knowledge, such a method has never been published. This algorithm was tested on completely and incompletely specified Boolean functions via quantum simulation.

Quantum Information and Computation•Jan 29, 2023•2 citations

Automated Theorem Proving for Quantum Circuit Verification using SAT Solvers

Jincheng Zhang

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.

•Sep 5, 2026•0 citations

SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization

Till Schnittka, Julie Maria Raju, Abhoy Kole +1 more

The Quantum Approximate Optimization Algorithm (QAOA) is a promising variational approach for solving Boolean satisfiability (SAT) problems. Existing SAT-to-QAOA workflows first translate Boolean formulas into penalty Hamiltonians before applying generic quantum compilation, thereby discarding SAT-specific information such as clause structure, logical operators, and variable dependencies. Consequently, subsequent compiler optimizations cannot exploit the underlying Boolean formulation. This paper presents SAQC, a SAT-aware compilation framework that introduces a SAT Intermediate Representation (SIR) to preserve Boolean structure during compilation. The proposed framework supports both CNF and XOR-extended CNF (eCNF) formulations and performs SAT-aware optimizations including clause rewriting, dependency analysis, and clause scheduling prior to quantum lowering. Building on the optimized SIR, SAQC provides a unified framework for both penalty Hamiltonian generation and direct clause-to-ansatz synthesis, together with ansatz optimizations based on relative-phase decomposition, ancilla-assisted synthesis, and dynamic uncomputation. Experimental results demonstrate significant reductions in circuit depth, two-qubit gate count, and compilation time compared with conventional Hamiltonian-based workflows while remaining compatible with existing quantum compilation frameworks.

quant-pharXiv:2609.05737•Sep 8, 2026•0 citations
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+TTT 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 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.
A classical Boolean specification need not be one-to-one, whereas every reversible quantum network must preserve distinctions between basis states. SAT-Embed-Q handles this mismatch by first constructing a partial reversible embedding from output-preimage multiplicities and then searching for a compatible mixed-polarity Toffoli network. We implemented two bounded satisfiability encodings, one tracking complete intermediate states and the other tracking individual line values, and evaluated both with a deterministic reference DPLL solver. On the four-line example F(a,b,c)=ab¯∨bc, the minimum-depth CNF contains 42,234 clauses in the direct encoding and 34,194 in the bit-level encoding. The smaller clause set did not translate into faster execution: the direct representation required less time in our solver. A separate exhaustive study of the target-preserving oracle class covers every single-output function of two and three inputs. Within that restricted class, allowing negative controls lowers the summed minimum target-gate count by 34.38% and 46.39%, respectively. We also examine two four-input functions from RevLib, for which fixing the input-preserving oracle structure leads to different gate counts from embedding-optimized benchmark circuits. These experiments characterize bounded synthesis and control-polarity choices for small functions; fault-tolerant resource optimization and large-network scalability remain outside their scope.
The Exclusive-OR Sum-of-Product (ESOP) minimization problem has long been of interest to the research community because of its importance in classical logic design (including low-power design and design for test), reversible logic synthesis, and knowledge discovery, among other applications. However, no exact minimal minimization method has been presented for more than seven variables on arbitrary functions. This paper presents a novel quantum-classical hybrid algorithm for the exact minimal ESOP minimization of incompletely specified Boolean functions. This algorithm constructs oracles from sets of constraints and leverages the quantum speedup offered by Grover's algorithm to find solutions to these oracles, thereby improving over classical algorithms. Improved encoding of ESOP expressions results in substantially fewer decision variables compared to many existing algorithms for many classes of Boolean functions. This paper also extends the idea of exact minimal ESOP minimization to additionally minimize the cost of realizing an ESOP expression as a quantum circuit. To the extent of the authors' knowledge, such a method has never been published. This algorithm was tested on completely and incompletely specified Boolean functions via quantum simulation.
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.
The Quantum Approximate Optimization Algorithm (QAOA) is a promising variational approach for solving Boolean satisfiability (SAT) problems. Existing SAT-to-QAOA workflows first translate Boolean formulas into penalty Hamiltonians before applying generic quantum compilation, thereby discarding SAT-specific information such as clause structure, logical operators, and variable dependencies. Consequently, subsequent compiler optimizations cannot exploit the underlying Boolean formulation. This paper presents SAQC, a SAT-aware compilation framework that introduces a SAT Intermediate Representation (SIR) to preserve Boolean structure during compilation. The proposed framework supports both CNF and XOR-extended CNF (eCNF) formulations and performs SAT-aware optimizations including clause rewriting, dependency analysis, and clause scheduling prior to quantum lowering. Building on the optimized SIR, SAQC provides a unified framework for both penalty Hamiltonian generation and direct clause-to-ansatz synthesis, together with ansatz optimizations based on relative-phase decomposition, ancilla-assisted synthesis, and dynamic uncomputation. Experimental results demonstrate significant reductions in circuit depth, two-qubit gate count, and compilation time compared with conventional Hamiltonian-based workflows while remaining compatible with existing quantum compilation frameworks.