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:2303.09353 · International Conference on Quantum Communications, Networking, and Computing (QCNC)

A Quantum SMT Solver for Bit-Vector Theory

Shang‐Wei Lin, Sihan Chen, Lei-Han Yao, Yean-Ru Chen, Yean-Ru Chen

Published Apr 6, 2026• 2 citations
arXivHTMLPDF

Abstract

Satisfiability modulo theory (SMT), a problem of determining the satisfiability of a first-order formula with respect to a decidable first-order theory, has a wide range of applications because of its powerful ability of problem encoding, including formal verification and optimization workflows in both classical and quantum domains. Given an SMT formula$F$, the classical lazy approach for SMT solving tries to (1) abstract$F$to a Boolean formula$F_{B}$, (2) find a Boolean solution to$F_{B}$, and (3) check whether the Boolean solution is consistent with the theory. If the solution found in the Boolean domain is not consistent with that in the theory domain, the SMT solver needs to perform steps (2) and (3) back and forth until a consistent solution is found between the theory and Boolean domains. This classical approach becomes unscalable when the search space is huge. In this work, we develop the first Grover–based quantum SMT solver to solve formulas on the theory of bit-vectors. With the characteristic of superposition in quantum computing, the proposed SMT solver is able to consider all the possible inputs simultaneously and check their consistency between the theory and Boolean domains in one shot, which brings significant speed-up for SMT solving.

DOI
10.1109/qcnc69040.2026.00019

Related papers

Quantum-Based SMT Solving for String Theory

Beatrice Casey, Joanna C. S. Santos, Andrew Hennessee

Satisfiability Modulo Theory (SMT) solvers are a useful tool that can be applied to a variety of problems, such as configuring relationships in distributed systems, detecting race conditions, and program analysis. String constraints are particularly difficult for SMT solvers to navigate, as the search space is generally large. Often times, classical SMT solvers will have to quit generating a solution for string constraints because it takes too long to find the solution. Quantum computing offers the advantages of quantum mechanics (e.g., superposition), which allows a system to explore a large search space much more efficiently. In this work, we explore creating a quantum-enabled SMT solver for string theory by using quantum annealing and Quadratic Unconstrained Binary Optimization (QUBO). Our preliminary results demonstrate that it is feasible to transform these string constraints to QUBO, and generate solutions for given constraints.

ACM International Symposium on High-Performance Parallel and Distributed Computing (HPDC)•Jul 20, 2025•0 citations

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

Implementation of Efficient Quantum Computing Algorithm for Searching

Nirhali Atharva, Malwade Rohit, P. Akshay +2 more

The K-SAT problem is a fundamental challenge in computational theory, widely used in artificial intelligence, cryptography, and optimization. Classical algorithms struggle with exponential time complexity, making them inefficient for large-scale instances. In this research, we propose an efficient quantum computing approach based on Grover’s algorithm to enhance the search process for satisfiable solutions in K-SAT problems. Our implementation leverages quantum superposition and amplitude amplification to explore multiple possible solutions simultaneously, reducing the search complexity from O (2ⁿ) in classical methods to O(√2ⁿ) in quantum computing. We design a quantum oracle that encodes the K-SAT clauses and integrates it into Grover’s iterative search framework. The performance is evaluated through Qiskit simulations, demonstrating a significant improvement in search efficiency compared to classical brute-force techniques. The results highlight the potential of quantum algorithms in solving complex combinatorial problems with enhanced speed and accuracy. This study contributes to the development of quantum-accelerated optimization methods, paving the way for real-world applications in machine learning, cryptanalysis, and large-scale data processing.

International Research Journal on Advanced Engineering Hub (IRJAEH)•May 21, 2025•0 citations

SMT-based Layout Synthesis for Silicon-based Quantum Computing with Crossbar Architecture

Sheng-Tan Huang, Ying-Jie Jiang, Shao‐Yun Fang +1 more

With the announcement of the most advanced silicon spin quantum-bit (qubit) chip by Intel, silicon-based quantum circuit manufacturing technology has shown the superior potential to realize quantum computing to other technologies because of the mature semiconductor manufacturing technologies and the compatibility with electronics. Due to the bottleneck in scalability caused by interconnections in silicon-based quantum circuits, crossbar architectures serve as one of the most promising solutions for circuitry implementation. This paper proposes the first satisfiability modulo theories (SMT) formulation to optimally solve the layout synthesis problem by simultaneously performing scheduling, mapping, and routing for silicon-based quantum systems with a specific crossbar architecture. The experiments demonstrate that the proposed method can effectively generate layout synthesis results with minimal usage of swap and shuttle gates within the shortest circuit depths, and the solutions greatly outperform those derived from a state-of-the-art work.

•Oct 27, 2024•3 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

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
Satisfiability modulo theory (SMT), a problem of determining the satisfiability of a first-order formula with respect to a decidable first-order theory, has a wide range of applications because of its powerful ability of problem encoding, including formal verification and optimization workflows in both classical and quantum domains. Given an SMT formulaFFF, the classical lazy approach for SMT solving tries to (1) abstractFFFto a Boolean formulaFBF_{B}FB​, (2) find a Boolean solution toFBF_{B}FB​, and (3) check whether the Boolean solution is consistent with the theory. If the solution found in the Boolean domain is not consistent with that in the theory domain, the SMT solver needs to perform steps (2) and (3) back and forth until a consistent solution is found between the theory and Boolean domains. This classical approach becomes unscalable when the search space is huge. In this work, we develop the first Grover–based quantum SMT solver to solve formulas on the theory of bit-vectors. With the characteristic of superposition in quantum computing, the proposed SMT solver is able to consider all the possible inputs simultaneously and check their consistency between the theory and Boolean domains in one shot, which brings significant speed-up for SMT solving.
Satisfiability Modulo Theory (SMT) solvers are a useful tool that can be applied to a variety of problems, such as configuring relationships in distributed systems, detecting race conditions, and program analysis. String constraints are particularly difficult for SMT solvers to navigate, as the search space is generally large. Often times, classical SMT solvers will have to quit generating a solution for string constraints because it takes too long to find the solution. Quantum computing offers the advantages of quantum mechanics (e.g., superposition), which allows a system to explore a large search space much more efficiently. In this work, we explore creating a quantum-enabled SMT solver for string theory by using quantum annealing and Quadratic Unconstrained Binary Optimization (QUBO). Our preliminary results demonstrate that it is feasible to transform these string constraints to QUBO, and generate solutions for given constraints.
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 K-SAT problem is a fundamental challenge in computational theory, widely used in artificial intelligence, cryptography, and optimization. Classical algorithms struggle with exponential time complexity, making them inefficient for large-scale instances. In this research, we propose an efficient quantum computing approach based on Grover’s algorithm to enhance the search process for satisfiable solutions in K-SAT problems. Our implementation leverages quantum superposition and amplitude amplification to explore multiple possible solutions simultaneously, reducing the search complexity from O (2ⁿ) in classical methods to O(√2ⁿ) in quantum computing. We design a quantum oracle that encodes the K-SAT clauses and integrates it into Grover’s iterative search framework. The performance is evaluated through Qiskit simulations, demonstrating a significant improvement in search efficiency compared to classical brute-force techniques. The results highlight the potential of quantum algorithms in solving complex combinatorial problems with enhanced speed and accuracy. This study contributes to the development of quantum-accelerated optimization methods, paving the way for real-world applications in machine learning, cryptanalysis, and large-scale data processing.
With the announcement of the most advanced silicon spin quantum-bit (qubit) chip by Intel, silicon-based quantum circuit manufacturing technology has shown the superior potential to realize quantum computing to other technologies because of the mature semiconductor manufacturing technologies and the compatibility with electronics. Due to the bottleneck in scalability caused by interconnections in silicon-based quantum circuits, crossbar architectures serve as one of the most promising solutions for circuitry implementation. This paper proposes the first satisfiability modulo theories (SMT) formulation to optimally solve the layout synthesis problem by simultaneously performing scheduling, mapping, and routing for silicon-based quantum systems with a specific crossbar architecture. The experiments demonstrate that the proposed method can effectively generate layout synthesis results with minimal usage of swap and shuttle gates within the shortest circuit depths, and the solutions greatly outperform those derived from a state-of-the-art work.
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.
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.