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

A hybrid Quantum proposal to deal with 3-SAT problem

Jose J. Paulet, Luis Llana, Hernán I. de la Cruz, Mauro Mezzini, Fernando Cuartero, Fernando L. Pelayo

Published Jun 7, 2023• 0 citations
arXivHTMLPDF

Abstract

Going as far as possible at SAT problem solving is the main aim of our work. For this sake we have made use of quantum computing from its two, on practice, main models of computation. They have required some reformulations over the former statement of 3-SAT problem in order to accomplish the requirements of both techniques. This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.

DOI
10.48550/arxiv.2306.04378

Related papers

Heuristics for Quantum Computing Dealing with 3-SAT

Jose J. Paulet, Luis Llana, Hernán Indíbil de la Cruz Calvo +3 more

The SAT problem is maybe one of the most famous NP-complete problems. This paper deals with the 3-SAT problem. We follow a sort of incremental strategy to save computational costs with respect to the classical quantum computing approach. We present an heuristics that leads this strategy, improving the performance of the purely random incremental scheme. We finally validate our approach by means of a thorough empirical study.

Mathematics•Apr 16, 2023•2 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

Speeding up search algorithms with Quantum Computing

Jose J. Paulet

This thesis focuses on algorithms over Quantum computing applied over NP hard search problems on domains lacking of any order. The partition problem has been addressed as first stage so providing a piece of quantum computing code which amplifies the amplitude of the solution state noticeably. This work continues addressing the problem of the satisfiability of Boolean formulas, in particular 3-SAT, from hybrid computation perspectives over both classical / quantum and purely quantum computing. There have been proposed strategies which include the definition of own heuristics and own metrics. The application of these strategies has meant a review of Grover's algorithm that has led to propose different methods of modifying it.

•Jan 1, 2023•0 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

Assessing fault-tolerant quantum advantage for k -SAT with structure

Martijn Brehm, Jordi R. Weggemans

For many problems, quantum algorithms promise speedups over their classical counterparts. However, these results predominantly rely on asymptotic worst-case analysis, which overlooks significant overheads due to error correction and the fact that real-world instances often contain exploitable structure. In this work, we employ the hybrid benchmarking method to evaluate the potential of quantum Backtracking and Grover's algorithm against the 2023 SAT competition main track winner in solving random k -SAT instances with tunable structure, designed to represent industry-like scenarios, using both T -depth and T -count as cost metrics to estimate quantum run times. Our findings reproduce the results of Campbell, Khurana, and Montanaro (Quantum '19) in the unstructured case using hybrid benchmarking. However, we offer a more sobering perspective in practically relevant regimes: almost all quantum speedups vanish, even asymptotically, when minimal structure is introduced or when T -count is considered instead of T -depth. Moreover, when the requirement is for the algorithm to find a solution within a single day, we find that only Grover's algorithm has the potential to outperform classical algorithms, but only in a very limited regime and only when using T -depth. We also discuss how more sophisticated heuristics could restore the asymptotic scaling advantage for quantum backtracking, but our findings suggest that the potential for practical quantum speedups in more structured k -SAT solving will remain limited.

arXiv:2412.13274•Quantum•Jan 20, 2026•1 citation

Coherent SAT solvers: a tutorial

Sam Reifenstein, Timothee G. Leleu, Timothy P. McKenna +6 more

The coherent Ising machine (CIM) is designed to solve the NP-hard Ising problem quickly and energy efficiently. Boolean satisfiability (SAT) and maximum satisfiability (Max-SAT) are classes of NP-complete and NP-hard problems that are equally important and more practically relevant combinatorial optimization problems. Many approaches exist for solving Boolean SAT, such as quantum annealing and classical stochastic local search (SLS) solvers; however, they all are expected to require many steps to solve hard SAT problems and, thus, require large amounts of time and energy. In addition, a SAT problem can be converted into an Ising problem and solved by an Ising machine; however, we have found that this approach has drawbacks. As well as reviewing existing approaches to solving the SAT problem, we have extended the CIM algorithm and architecture to solve SAT and Max-SAT problems directly. This new technique is termed a coherent SAT solver (CSS). We have studied three implementations of the CSS, all-optical, hybrid optical–digital and all digital (cyber-CSS), and have compared the time-to-solution and energy-to-solution of three machines. The cyber-CSS, which is already implemented using a graphics processing unit (GPU), demonstrates competitive performance against existing SLS solvers such as probSAT. The CSS is also compared with another continuous-time SAT solver known as the CTDS, and the scaling behavior is evaluated for random 3-SAT problems. The hybrid optical–digital CSS is a more performant and practical machine that can be realized in a short term. Finally, the all-optical CSS promises the best energy-to-solution cost; however various technical challenges in nonlinear optics await us in order to build this machine.

Advances in Optics and Photonics•Mar 22, 2023•17 citations
Going as far as possible at SAT problem solving is the main aim of our work. For this sake we have made use of quantum computing from its two, on practice, main models of computation. They have required some reformulations over the former statement of 3-SAT problem in order to accomplish the requirements of both techniques. This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
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.
This thesis focuses on algorithms over Quantum computing applied over NP hard search problems on domains lacking of any order. The partition problem has been addressed as first stage so providing a piece of quantum computing code which amplifies the amplitude of the solution state noticeably. This work continues addressing the problem of the satisfiability of Boolean formulas, in particular 3-SAT, from hybrid computation perspectives over both classical / quantum and purely quantum computing. There have been proposed strategies which include the definition of own heuristics and own metrics. The application of these strategies has meant a review of Grover's algorithm that has led to propose different methods of modifying it.
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.
For many problems, quantum algorithms promise speedups over their classical counterparts. However, these results predominantly rely on asymptotic worst-case analysis, which overlooks significant overheads due to error correction and the fact that real-world instances often contain exploitable structure. In this work, we employ the hybrid benchmarking method to evaluate the potential of quantum Backtracking and Grover's algorithm against the 2023 SAT competition main track winner in solving random k -SAT instances with tunable structure, designed to represent industry-like scenarios, using both T -depth and T -count as cost metrics to estimate quantum run times. Our findings reproduce the results of Campbell, Khurana, and Montanaro (Quantum '19) in the unstructured case using hybrid benchmarking. However, we offer a more sobering perspective in practically relevant regimes: almost all quantum speedups vanish, even asymptotically, when minimal structure is introduced or when T -count is considered instead of T -depth. Moreover, when the requirement is for the algorithm to find a solution within a single day, we find that only Grover's algorithm has the potential to outperform classical algorithms, but only in a very limited regime and only when using T -depth. We also discuss how more sophisticated heuristics could restore the asymptotic scaling advantage for quantum backtracking, but our findings suggest that the potential for practical quantum speedups in more structured k -SAT solving will remain limited.
The coherent Ising machine (CIM) is designed to solve the NP-hard Ising problem quickly and energy efficiently. Boolean satisfiability (SAT) and maximum satisfiability (Max-SAT) are classes of NP-complete and NP-hard problems that are equally important and more practically relevant combinatorial optimization problems. Many approaches exist for solving Boolean SAT, such as quantum annealing and classical stochastic local search (SLS) solvers; however, they all are expected to require many steps to solve hard SAT problems and, thus, require large amounts of time and energy. In addition, a SAT problem can be converted into an Ising problem and solved by an Ising machine; however, we have found that this approach has drawbacks. As well as reviewing existing approaches to solving the SAT problem, we have extended the CIM algorithm and architecture to solve SAT and Max-SAT problems directly. This new technique is termed a coherent SAT solver (CSS). We have studied three implementations of the CSS, all-optical, hybrid optical–digital and all digital (cyber-CSS), and have compared the time-to-solution and energy-to-solution of three machines. The cyber-CSS, which is already implemented using a graphics processing unit (GPU), demonstrates competitive performance against existing SLS solvers such as probSAT. The CSS is also compared with another continuous-time SAT solver known as the CTDS, and the scaling behavior is evaluated for random 3-SAT problems. The hybrid optical–digital CSS is a more performant and practical machine that can be realized in a short term. Finally, the all-optical CSS promises the best energy-to-solution cost; however various technical challenges in nonlinear optics await us in order to build this machine.