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:1307.3931 · New Journal of Physics

Max 2-SAT with up to 108 qubits

Siddhartha Santra, Gregory Quiroz, Greg Ver Steeg, Daniel A. Lidar

Published Apr 8, 2014• 60 citations
arXivHTMLPDF

Abstract

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.

DOI
10.1088/1367-2630/16/4/045006

Related papers

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

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

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

Comparing the hardness of MAX 2-SAT problem instances for quantum and classical algorithms

Puya Mirkarimi, Adam Callison, Lewis Light +2 more

An algorithm for a particular problem may find some instances of the problem easier and others harder to solve, even for a fixed input size. We numerically analyze the relative hardness of MAX 2-SAT problem instances for various continuous-time quantum algorithms and a comparable classical algorithm. This has two motivations: To investigate whether small-sized problem instances, which are commonly used in numerical simulations of quantum algorithms for benchmarking purposes, are a good representation of larger instances in terms of their hardness to solve, and to determine the applicability of continuous-time quantum algorithms in a portfolio approach, where we take advantage of the variation in the hardness of instances between different algorithms by running them in parallel. We find that, while there are correlations in instance hardness between all of the algorithms considered, they appear weak enough that a portfolio approach would likely be desirable in practice. Our results also show a widening range of hardness of randomly generated instances as the problem size is increased, which demonstrates both the difference in the distribution of hardness at small sizes and the value of a portfolio approach that can reduce the number of extremely hard instances. We identify specific weaknesses of these quantum algorithms that can be overcome with a portfolio approach, such their inability to efficiently solve satisfiable instances (which is easy classically).

arXiv:2206.06876•Physical Review Research•Jun 5, 2023•7 citations

Efficient digital quadratic unconstrained binary optimization solvers for SAT problems

Robert Simon Fong, Yanming Song, Alexander Yosifov

Abstract Boolean satisfiability (SAT) is a propositional logic problem of determining whether an assignment of variables satisfies a Boolean formula. Many combinatorial optimization problems can be formulated in Boolean SAT logic—either as k-SAT decision problems or Max k-SAT optimization problems, with conflict-driven clause learning (CDCL) solvers being the most prominent. Despite their ability to handle large instances, CDCL-based solvers have fundamental scalability limitations. In light of this, we propose recently-developed quadratic unconstrained binary optimization (QUBO) solvers as an alternative platform for 3-SAT problems. To utilize them, we implement a 2-step [3-SAT]-[Max 2-SAT]-[QUBO] conversion procedure and present a novel approach using linear systems and Diophantine equation to calculate the number of both satisfied and violated clauses of the original 3-SAT instance from the transformed Max 2-SAT formulation. We then demonstrate, through numerical simulations on several benchmark instances, that digital QUBO solvers can achieve state-of-the-art accuracy on 78-variable 3-SAT benchmark problems. Our work facilitates the broader use of quantum annealers on noisy intermediate-scale quantum devices, as well as their quantum-inspired digital counterparts, for solving 3-SAT problems.

arXiv:2408.03757•New Journal of Physics•Jan 1, 2025•1 citation
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.
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.
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.
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.
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.
An algorithm for a particular problem may find some instances of the problem easier and others harder to solve, even for a fixed input size. We numerically analyze the relative hardness of MAX 2-SAT problem instances for various continuous-time quantum algorithms and a comparable classical algorithm. This has two motivations: To investigate whether small-sized problem instances, which are commonly used in numerical simulations of quantum algorithms for benchmarking purposes, are a good representation of larger instances in terms of their hardness to solve, and to determine the applicability of continuous-time quantum algorithms in a portfolio approach, where we take advantage of the variation in the hardness of instances between different algorithms by running them in parallel. We find that, while there are correlations in instance hardness between all of the algorithms considered, they appear weak enough that a portfolio approach would likely be desirable in practice. Our results also show a widening range of hardness of randomly generated instances as the problem size is increased, which demonstrates both the difference in the distribution of hardness at small sizes and the value of a portfolio approach that can reduce the number of extremely hard instances. We identify specific weaknesses of these quantum algorithms that can be overcome with a portfolio approach, such their inability to efficiently solve satisfiable instances (which is easy classically).
Abstract Boolean satisfiability (SAT) is a propositional logic problem of determining whether an assignment of variables satisfies a Boolean formula. Many combinatorial optimization problems can be formulated in Boolean SAT logic—either as k-SAT decision problems or Max k-SAT optimization problems, with conflict-driven clause learning (CDCL) solvers being the most prominent. Despite their ability to handle large instances, CDCL-based solvers have fundamental scalability limitations. In light of this, we propose recently-developed quadratic unconstrained binary optimization (QUBO) solvers as an alternative platform for 3-SAT problems. To utilize them, we implement a 2-step [3-SAT]-[Max 2-SAT]-[QUBO] conversion procedure and present a novel approach using linear systems and Diophantine equation to calculate the number of both satisfied and violated clauses of the original 3-SAT instance from the transformed Max 2-SAT formulation. We then demonstrate, through numerical simulations on several benchmark instances, that digital QUBO solvers can achieve state-of-the-art accuracy on 78-variable 3-SAT benchmark problems. Our work facilitates the broader use of quantum annealers on noisy intermediate-scale quantum devices, as well as their quantum-inspired digital counterparts, for solving 3-SAT problems.