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

IEEE Asia Pacific Conference on Circuits and Systems (APCCAS)

Experimental Analysis of Quantum Annealing for Satisfiability Problems

Remma Ukaku, Tomohisa Kawakami, Hiroyuki Tomiyama

Published Oct 12, 2025• 0 citations
Publisher

Abstract

Quantum computing has emerged as a promising method for solving combinatorial optimization problems. These problems are often encoded as the Satisfiability (SAT) problem. In this study, we explore the quantum annealing based approach to solving the SAT problems. We conduct experiments on uniformly random 3-CNF instances that have 400 propositional variables and 1,000 to 2,499 clauses. We measure the time required to solve them using Fixstars Amplify Annealing Engine. The results show that the monotonic increase in solving time as the number of clauses increases, except for a discontinuity point at approximately 1,800 clauses. In addition, we observe some cases of false UNSAT reports. Our findings demonstrate both the characteristics and the limitations of this quantum annealing based solver. We plan to reproduce the solver on a local machine to inspect the performance when varying the parameters of the quantum annealing and the environment.

DOI
10.1109/apccas67402.2025.11377204

Related papers

Towards Quantum Computing: Solving Satisfiability Problem by Quantum Annealing

Juexiao Su

To date, conventional computers have never been able to efficiently handle certain tasks, where the number of computation steps is likely to blow up as the problem size increases. As an emerging technology and new computing paradigm, quantum computing has a great potential to tackle those hard tasks efficiently. Among all the existing quantum computation models, quantum annealing has drawn significant attention in recent years due to the realization of the commercialized quantum annealer, sparking research interests in developing applications to solve problems that are intractable for classical computers.However, designing and implementing algorithms that manage to harness the enormous computation power from quantum annealer remains a challenging task. Generally, it requires mapping of the given optimization problem into quadratic unconstrained binary optimization(QUBO) problem and embedding the subsequent QUBO onto the physical architecture of quantum annealer. Additionally, practical quantum annealers are susceptible to errors leading to low probability of the correct solution.In this study, we focus on solving Boolean satisfiability (SAT) problem using quantum annealer while addressing practical limitations. We have proposed a mapping technique that maps SAT problem to QUBO, and we have further devised a tool flow that embeds the QUBO onto the architecture of a quantum annealing device. Additionally, We have optimized the proposed embedding flow to reduce run-time in addition to shortening the qubit chain length, leading to robust quantum annealing. To further improve the reliability of quantum annealing, we have also developed a post processing embedding technique that enlarges the energy gap between ground state and the first excited state. To demonstrate the effectiveness of proposed methods, we have conducted experiments on real quantum annealing devices manufactured by D-Wave Systems, showing compelling result of using quantum annealer to solve SAT problem.

•Jan 1, 2018•4 citations

Quantum annealing for combinatorial optimization: a benchmarking study

Seongmin Kim, Sang-Woo Ahn, In‐Saeng Suh +3 more

Quantum annealing (QA) has the potential to significantly improve solution quality and reduce time complexity in solving combinatorial optimization problems compared to classical optimization methods. However, due to the limited number of qubits and their connectivity, the QA hardware did not show such an advantage over classical methods in past benchmarking studies. Recent advancements in QA with more than 5000 qubits, enhanced qubit connectivity, and the hybrid architecture promise to realize the quantum advantage. Here, we use a quantum annealer with state-of-the-art techniques and benchmark its performance against classical solvers. To compare their performance, we solve over 50 optimization problem instances represented by large and dense Hamiltonian matrices using quantum and classical solvers. The results demonstrate that a state-of-the-art quantum solver has higher accuracy (~0.013%) and a significantly faster problem-solving time (~6561×) than the best classical solver. Our results highlight the advantages of leveraging QA over classical counterparts, particularly in hybrid configurations, for achieving high accuracy and substantially reduced problem solving time in large-scale real-world optimization problems.

arXiv:2504.06201•npj Quantum Information•May 16, 2025•46 citations

Quantum Annealing and the Satisfiability Problem

Kristen L. Pudenz, Greg S. Tallant, Todd R. Belote +1 more

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.

arXiv:1612.07258•Dec 21, 2016•5 citations

Quantum Annealing and the Satisfiability Problem

Kristen L. Pudenz, Tallant Gregory S., Todd R. Belote +1 more

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.

Advances in parallel computing•Jan 1, 2017•0 citations

Quantum logic synthesis for Satisfiability Problems.

Shuai Yang, Wei Zi, Bujiao Wu +3 more

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(k^2 m^2/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 $\Omega(m^\epsilon)$ (for any $\epsilon > 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.

•Jan 14, 2021•1 citation

Boolean satisfiability verification by quantum annealing

Maria Maltseva, Александр Сергеевич Румянцев, Mariya Maltseva +1 more

The Boolean satisfiability problem (SAT) is widely applied in modern tasks of microelectronics design automation. An important application of such a task is the design of logic circuits with specified characteristics from a given set of logic gates. To solve an SAT problem, both standard solvers and modern optimization tools can be used, including a relatively new hardware tool for solving the quantum annealing problem. The solution of this problem can be performed on a quantum annealing system by constructing a socalled Boolean network according to special rules and selecting an appropriate objective function. The article discusses the practical application of quantum annealing to the construction of short logic circuits by solving an SAT problem based on the methods proposed in the literature, and also analyzes the practical aspects of applying such methods to the construction of quantum circuits.

Proceedings of the Karelian Research Centre of the Russian Academy of Sciences•Jun 23, 2023•1 citation
Quantum computing has emerged as a promising method for solving combinatorial optimization problems. These problems are often encoded as the Satisfiability (SAT) problem. In this study, we explore the quantum annealing based approach to solving the SAT problems. We conduct experiments on uniformly random 3-CNF instances that have 400 propositional variables and 1,000 to 2,499 clauses. We measure the time required to solve them using Fixstars Amplify Annealing Engine. The results show that the monotonic increase in solving time as the number of clauses increases, except for a discontinuity point at approximately 1,800 clauses. In addition, we observe some cases of false UNSAT reports. Our findings demonstrate both the characteristics and the limitations of this quantum annealing based solver. We plan to reproduce the solver on a local machine to inspect the performance when varying the parameters of the quantum annealing and the environment.
To date, conventional computers have never been able to efficiently handle certain tasks, where the number of computation steps is likely to blow up as the problem size increases. As an emerging technology and new computing paradigm, quantum computing has a great potential to tackle those hard tasks efficiently. Among all the existing quantum computation models, quantum annealing has drawn significant attention in recent years due to the realization of the commercialized quantum annealer, sparking research interests in developing applications to solve problems that are intractable for classical computers.However, designing and implementing algorithms that manage to harness the enormous computation power from quantum annealer remains a challenging task. Generally, it requires mapping of the given optimization problem into quadratic unconstrained binary optimization(QUBO) problem and embedding the subsequent QUBO onto the physical architecture of quantum annealer. Additionally, practical quantum annealers are susceptible to errors leading to low probability of the correct solution.In this study, we focus on solving Boolean satisfiability (SAT) problem using quantum annealer while addressing practical limitations. We have proposed a mapping technique that maps SAT problem to QUBO, and we have further devised a tool flow that embeds the QUBO onto the architecture of a quantum annealing device. Additionally, We have optimized the proposed embedding flow to reduce run-time in addition to shortening the qubit chain length, leading to robust quantum annealing. To further improve the reliability of quantum annealing, we have also developed a post processing embedding technique that enlarges the energy gap between ground state and the first excited state. To demonstrate the effectiveness of proposed methods, we have conducted experiments on real quantum annealing devices manufactured by D-Wave Systems, showing compelling result of using quantum annealer to solve SAT problem.
Quantum annealing (QA) has the potential to significantly improve solution quality and reduce time complexity in solving combinatorial optimization problems compared to classical optimization methods. However, due to the limited number of qubits and their connectivity, the QA hardware did not show such an advantage over classical methods in past benchmarking studies. Recent advancements in QA with more than 5000 qubits, enhanced qubit connectivity, and the hybrid architecture promise to realize the quantum advantage. Here, we use a quantum annealer with state-of-the-art techniques and benchmark its performance against classical solvers. To compare their performance, we solve over 50 optimization problem instances represented by large and dense Hamiltonian matrices using quantum and classical solvers. The results demonstrate that a state-of-the-art quantum solver has higher accuracy (~0.013%) and a significantly faster problem-solving time (~6561×) than the best classical solver. Our results highlight the advantages of leveraging QA over classical counterparts, particularly in hybrid configurations, for achieving high accuracy and substantially reduced problem solving time in large-scale real-world optimization problems.
The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.
The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.
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)O(k^2 m^2/n)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ϵ)\Omega(m^\epsilon)Ω(mϵ) (for any ϵ>0\epsilon > 0ϵ>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.
The Boolean satisfiability problem (SAT) is widely applied in modern tasks of microelectronics design automation. An important application of such a task is the design of logic circuits with specified characteristics from a given set of logic gates. To solve an SAT problem, both standard solvers and modern optimization tools can be used, including a relatively new hardware tool for solving the quantum annealing problem. The solution of this problem can be performed on a quantum annealing system by constructing a socalled Boolean network according to special rules and selecting an appropriate objective function. The article discusses the practical application of quantum annealing to the construction of short logic circuits by solving an SAT problem based on the methods proposed in the literature, and also analyzes the practical aspects of applying such methods to the construction of quantum circuits.