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:1607.03329 · SciPost Physics

Assessment of Quantum Annealing for the Construction of Satisfiability Filters

Marlon Azinović, Daniel Herr, Bettina Heim, Ethan Brown, Matthias Troyer

Published Apr 7, 2017• 22 citations
arXivHTMLPDF

Abstract

Satisfiability filters are a new and promising type of filters for set membership testing. In order to construct satisfiability filters, it is necessary to find disparate solutions to hard random k k -SAT problems. This paper compares simulated annealing, simulated quantum annealing and WalkSAT, an open-source SAT solver, in terms of their ability to find such solutions. The results indicate that solutions found by simulated quantum annealing are generally less disparate than solutions found by the other solvers and therefore less useful for the construction of satisfiability filters.

DOI
10.21468/scipostphys.2.2.013

Related papers

Constructing SAT Filters with a Quantum Annealer

Adam Douglass, Andrew D. King, Jack Raymond

SAT filters are a novel and compact data structure that can be used to quickly query a word for membership in a fixed set. They have the potential to store more information in a fixed storage limit than a Bloom filter. Constructing a SAT filter requires sampling diverse solutions to randomly constructed constraint satisfaction instances, but there is flexibility in the choice of constraint satisfaction problem. Presented here is a case study of SAT filter construction with a focus on constraint satisfaction problems based on MAX-CUT clauses (Not-all-equal 3-SAT, 2-in-4-SAT, etc.) and frustrated cycles in the Ising model. Solutions are sampled using a D-Wave quantum annealer, and results are measured against classical approaches. The SAT variants studied are of interest in the context of SAT filters, independent of the solvers used.

Lecture notes in computer science•Jan 1, 2015•40 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

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 annealing for hard 2-satisfiability problems: Distribution and scaling of minimum energy gap and success probability

Vrinda Mehta, Fengping Jin, Hans A. De Raedt +1 more

In recent years, quantum annealing has gained the status of being a promising candidate for solving various optimization problems. Using a set of hard 2-satisfiability (2-SAT) problems, consisting of problems of up to 18 variables, we analyze the scaling complexity of the quantum annealing algorithm and study the distributions of the minimum energy gap and the success probability. We extend the analysis of the standard quantum annealing Hamiltonian by introducing an additional term, the trigger Hamiltonian, which can be of two types: ferromagnetic and antiferromagnetic. We use these trigger Hamiltonians to study their influence on the success probability for solving the selected 2-SAT problems. We find that although the scaling of the runtime is exponential for the standard and modified quantum annealing Hamiltonians, the scaling constant in the case of adding the trigger Hamiltonians can be significantly smaller. Furthermore, certain choices for the trigger Hamiltonian and annealing times can result in a better scaling than that for simulated annealing. Finally, we also use the quantum annealers of D-Wave Systems Inc. to study their performance in solving the 2-SAT problems and compare it with the simulation results.

arXiv:2202.00118•Physical Review A•Jun 3, 2022•11 citations

Experimental Analysis of Quantum Annealing for Satisfiability Problems

Remma Ukaku, Tomohisa Kawakami, Hiroyuki Tomiyama

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.

IEEE Asia Pacific Conference on Circuits and Systems (APCCAS)•Oct 12, 2025•0 citations
Satisfiability filters are a new and promising type of filters for set membership testing. In order to construct satisfiability filters, it is necessary to find disparate solutions to hard random k k -SAT problems. This paper compares simulated annealing, simulated quantum annealing and WalkSAT, an open-source SAT solver, in terms of their ability to find such solutions. The results indicate that solutions found by simulated quantum annealing are generally less disparate than solutions found by the other solvers and therefore less useful for the construction of satisfiability filters.
SAT filters are a novel and compact data structure that can be used to quickly query a word for membership in a fixed set. They have the potential to store more information in a fixed storage limit than a Bloom filter. Constructing a SAT filter requires sampling diverse solutions to randomly constructed constraint satisfaction instances, but there is flexibility in the choice of constraint satisfaction problem. Presented here is a case study of SAT filter construction with a focus on constraint satisfaction problems based on MAX-CUT clauses (Not-all-equal 3-SAT, 2-in-4-SAT, etc.) and frustrated cycles in the Ising model. Solutions are sampled using a D-Wave quantum annealer, and results are measured against classical approaches. The SAT variants studied are of interest in the context of SAT filters, independent of the solvers used.
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.
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.
In recent years, quantum annealing has gained the status of being a promising candidate for solving various optimization problems. Using a set of hard 2-satisfiability (2-SAT) problems, consisting of problems of up to 18 variables, we analyze the scaling complexity of the quantum annealing algorithm and study the distributions of the minimum energy gap and the success probability. We extend the analysis of the standard quantum annealing Hamiltonian by introducing an additional term, the trigger Hamiltonian, which can be of two types: ferromagnetic and antiferromagnetic. We use these trigger Hamiltonians to study their influence on the success probability for solving the selected 2-SAT problems. We find that although the scaling of the runtime is exponential for the standard and modified quantum annealing Hamiltonians, the scaling constant in the case of adding the trigger Hamiltonians can be significantly smaller. Furthermore, certain choices for the trigger Hamiltonian and annealing times can result in a better scaling than that for simulated annealing. Finally, we also use the quantum annealers of D-Wave Systems Inc. to study their performance in solving the 2-SAT problems and compare it with the simulation results.
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.