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

Lecture notes in computer science

Constructing SAT Filters with a Quantum Annealer

Adam Douglass, Andrew D. King, Jack Raymond

Published Jan 1, 2015• 40 citations
Publisher

Abstract

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.

DOI
10.1007/978-3-319-24318-4_9

Related papers

Assessment of Quantum Annealing for the Construction of Satisfiability Filters

Marlon Azinović, Daniel Herr, Bettina Heim +2 more

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.

arXiv:1607.03329•SciPost Physics•Apr 7, 2017•22 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 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

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

Max 2-SAT with up to 108 qubits

Siddhartha Santra, Gregory Quiroz, Greg Ver Steeg +1 more

We experimentally study the performance of a programmable quantum annealing processor, the D-Wave One (DW1) with up to 108 qubits, on maximum SAT problem with 2 variables per clause (MAX 2-SAT) problems. We consider ensembles of random problems characterized by a fixed clause density, an external parameter which we tune through its critical value in our experiments. We demonstrate that the DW1 is sensitive to the critical value of the clause density. The DW1 results are verified and compared with akmaxsat , an exact, state-of-the-art algorithm. We study the relative performance of the two solvers and how they correlate in terms of problem hardness. We find that the DW1 performance scales more favorably with problem size and that problem hardness correlation is essentially non-existent. We discuss the relevance and limitations of such a comparison.

arXiv:1307.3931•New Journal of Physics•Apr 8, 2014•60 citations

Probing for quantum speedup in spin-glass problems with planted solutions

Itay Hen, Joshua Job, Tameem Albash +3 more

The availability of quantum annealing devices with hundreds of qubits has made the experimental demonstration of a quantum speedup for optimization problems a coveted, albeit elusive goal. Going beyond earlier studies of random Ising problems, here we introduce a method to construct a set of frustrated Ising-model optimization problems with tunable hardness. We study the performance of a D-Wave Two device (DW2) with up to 503 qubits on these problems and compare it to a suite of classical algorithms, including a highly optimized algorithm designed to compete directly with the DW2. The problems are generated around predetermined ground-state configurations, called planted solutions, which makes them particularly suitable for benchmarking purposes. The problem set exhibits properties familiar from constraint satisfaction (SAT) problems, such as a peak in the typical hardness of the problems, determined by a tunable clause density parameter. We bound the hardness regime where the DW2 device either does not or might exhibit a quantum speedup for our problem set. While we do not find evidence for a speedup for the hardest and most frustrated problems in our problem set, we cannot rule out that a speedup might exist for some of the easier, less frustrated problems. Our empirical findings pertain to the specific D-Wave processor and problem set we studied and leave open the possibility that future processors might exhibit a quantum speedup on the same problem set.

arXiv:1502.01663•Physical Review A•Oct 23, 2015•168 citations
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.
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.
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.
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.
We experimentally study the performance of a programmable quantum annealing processor, the D-Wave One (DW1) with up to 108 qubits, on maximum SAT problem with 2 variables per clause (MAX 2-SAT) problems. We consider ensembles of random problems characterized by a fixed clause density, an external parameter which we tune through its critical value in our experiments. We demonstrate that the DW1 is sensitive to the critical value of the clause density. The DW1 results are verified and compared with akmaxsat , an exact, state-of-the-art algorithm. We study the relative performance of the two solvers and how they correlate in terms of problem hardness. We find that the DW1 performance scales more favorably with problem size and that problem hardness correlation is essentially non-existent. We discuss the relevance and limitations of such a comparison.
The availability of quantum annealing devices with hundreds of qubits has made the experimental demonstration of a quantum speedup for optimization problems a coveted, albeit elusive goal. Going beyond earlier studies of random Ising problems, here we introduce a method to construct a set of frustrated Ising-model optimization problems with tunable hardness. We study the performance of a D-Wave Two device (DW2) with up to 503 qubits on these problems and compare it to a suite of classical algorithms, including a highly optimized algorithm designed to compete directly with the DW2. The problems are generated around predetermined ground-state configurations, called planted solutions, which makes them particularly suitable for benchmarking purposes. The problem set exhibits properties familiar from constraint satisfaction (SAT) problems, such as a peak in the typical hardness of the problems, determined by a tunable clause density parameter. We bound the hardness regime where the DW2 device either does not or might exhibit a quantum speedup for our problem set. While we do not find evidence for a speedup for the hardest and most frustrated problems in our problem set, we cannot rule out that a speedup might exist for some of the easier, less frustrated problems. Our empirical findings pertain to the specific D-Wave processor and problem set we studied and leave open the possibility that future processors might exhibit a quantum speedup on the same problem set.