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:2405.09272 · Genetic and Evolutionary Computation Conference Companion (GECCO Companion)

Using an Evolutionary Algorithm to Create (MAX)-3SAT QUBOs

Sebastian Zielinski, Maximilian Zorn, Thomas Gabor, Sebastian Feld, Claudia Linnhoff–Popien

Published Jul 14, 2024• 1 citation
arXivHTMLPDF

Abstract

A common way of solving satisfiability instances with quantum methods is to transform these instances into instances of QUBO. State-of-the-art transformations from MAX-3SAT to QUBO work by mapping clauses of a 3SAT formula associated with the MAX-3SAT instance to an instance of QUBO and combining the resulting QUBOs into a single QUBO instance representing the whole MAX-3SAT instance. As creating these transformations is currently done manually or via exhaustive search methods and is, therefore, algorithmically inefficient, we see potential for including search-based optimization. In this paper, we propose two methods of using evolutionary algorithms to create QUBO representations of MAX-3SAT problems automatically. We evaluate our created QUBOs on 500 and 1000-clause 3SAT formulae and find competitive performance to state-of-the-art baselines when using both classical and quantum annealing solvers.

DOI
10.1145/3638530.3664153

Related papers

Pattern QUBOs: Algorithmic Construction of 3SAT-to-QUBO Transformations

Sebastian Zielinski, Jonas Nüßlein, Jonas Stein +3 more

One way of solving 3sat instances on a quantum computer is to transform the 3sat instances into instances of Quadratic Unconstrained Binary Optimizations (QUBOs), which can be used as an input for the QAOA algorithm on quantum gate systems or as an input for quantum annealers. This mapping is performed by a 3sat-to-QUBO transformation. Recently, it has been shown that the choice of the 3sat-to-QUBO transformation can significantly impact the solution quality of quantum annealing. It has been shown that the solution quality can vary up to an order of magnitude difference in the number of correct solutions received, depending solely on the 3sat-to-QUBO transformation. An open question is: what causes these differences in the solution quality when solving 3sat-instances with different 3sat-to-QUBO transformations? To be able to conduct meaningful studies that assess the reasons for the differences in the performance, a larger number of different 3sat-to-QUBO transformations would be needed. However, currently, there are only a few known 3sat-to-QUBO transformations, and all of them were created manually by experts, who used time and clever reasoning to create these transformations. In this paper, we will solve this problem by proposing an algorithmic method that is able to create thousands of new and different 3sat-to-QUBO transformations, and thus enables researchers to systematically study the reasons for the significant difference in the performance of different 3sat-to-QUBO transformations. Our algorithmic method is an exhaustive search procedure that exploits properties of 4×4 dimensional pattern QUBOs, a concept which has been used implicitly in the creation of 3sat-to-QUBO transformations before, but was never described explicitly. We will thus also formally and explicitly introduce the concept of pattern QUBOs in this paper.

arXiv:2305.02659•Electronics•Aug 17, 2023•12 citations

Solving Max-3SAT Using QUBO Approximation

Sebastian Zielinski, Jonas Nüßlein, Michael Kölle +3 more

As contemporary quantum computers do not possess error correction, any calculation performed by these devices can be considered an involuntary approximation. To solve a problem on a quantum annealer, it has to be expressed as an instance of Quadratic Unconstrained Binary Optimization (QUBO). In this work, we thus study whether systematically approximating QUBO representations of the MAX-3SAT problem can improve the solution quality when solved on contemporary quantum hardware, compared to using exact, non-approximated QUBO representations. For a MAX-3SAT instance consisting of a 3SAT formula with$n$variables and$m$clauses, we propose a method of systematically creating approximate QUBO representations of dimension$(n\times n)$, which is significantly smaller than the QUBO matrices of any exact, non-approximated MAX-3SAT QUBO transformation. In an empirical evaluation, we demonstrate that using our QUBO approximations for solving MAX-3SAT problems on D-Wave's quantum annealer Advantage_System6.4 can yield better results than using state-of-the-art exact QUBO transformations. Furthermore, we demonstrate that using naive QUBO approximation methods, based on removing values from exact$(n+m)\times(n+m)-\mathbf{dimensional}$QUBO representations of MAX-3SAT instances, is ineffective.

arXiv:2409.15891•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 15, 2024•4 citations

Analyzing the impact of 3SAT-to-QUBO transformations on simulated annealing-based optimization

Marina Maroto Gallardo

The increasing complexity of computational problems in various fields entails the development of efficient methods to solve them. Thus, the emerging technology of quantum computers comes with algorithms, such as quantum annealing, that could solve optimization problems exponentially faster. In particular, to solve the 3SAT problem on quantum annealers, it must be transformed into an instance of Quadratic Unconstrained Binary Optimization (QUBO). Given that the choice of 3SAT-to-QUBO transformation affects the solution quality on quantum annealing, an algorithmic method for creating numerous 3SAT-to-QUBO transformations has recently been proposed, aiming to investigate more deeply such effect. This represents a challenge when deciding which is the best performing 3SAT-to-QUBO transformation that should be used when solving a 3SAT instance on quantum annealing. To overcome this issue, this work investigates the impact of different 3SAT-to-QUBO transformations on the solution quality of simulated annealing, as a classical analogue to quantum annealing. We demonstrate that different QUBO encodings of the same 3SAT instance can lead to different outcomes in terms of energy and clause satisfaction. We also reveal some correlations between 3SAT features, QUBO structural properties, and solution quality. These findings underscore the importance of the choice of 3SAT-to-QUBO transformation in simulated annealing, and provide a foundation for the future development of machine learning models for guiding encoding choices in both classical and quantum environments.

•Jul 4, 2025•0 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

Finding solutions to NP problems: philosophical differences between quantum and evolutionary search algorithms

G.W. Greenwood

This paper uses instances of SAT, 3SAT and TSP to describe how evolutionary search (running on a classical computer) differs from quantum search (running on a quantum computer) for solving NP problems.

IEEE Congress on Evolutionary Computation (CEC)•Nov 13, 2002•32 citations

Finding Solutions to NP Problems: Philosophical Difference Between Quantum and Evolutionary Search Algorithms

Greenwood, G. W.

There is no known polynomial-time algorithm that can solve an NP problem. Evolutionary search has been shown to be a viable method of finding acceptable solutions within a reasonable time period. Recently quantum computers have surfaced as another alternative method. But these two methods use radically different philosophies for solving NP problems even though both search methods are non-deterministic. This paper uses instances of {\bf SAT}, {\bf 3SAT} and {\bf TSP} to describe how these two methods differ in their approach to solving NP problems.

arXiv:quant-ph/0010021•Oct 5, 2000•3 citations
A common way of solving satisfiability instances with quantum methods is to transform these instances into instances of QUBO. State-of-the-art transformations from MAX-3SAT to QUBO work by mapping clauses of a 3SAT formula associated with the MAX-3SAT instance to an instance of QUBO and combining the resulting QUBOs into a single QUBO instance representing the whole MAX-3SAT instance. As creating these transformations is currently done manually or via exhaustive search methods and is, therefore, algorithmically inefficient, we see potential for including search-based optimization. In this paper, we propose two methods of using evolutionary algorithms to create QUBO representations of MAX-3SAT problems automatically. We evaluate our created QUBOs on 500 and 1000-clause 3SAT formulae and find competitive performance to state-of-the-art baselines when using both classical and quantum annealing solvers.
One way of solving 3sat instances on a quantum computer is to transform the 3sat instances into instances of Quadratic Unconstrained Binary Optimizations (QUBOs), which can be used as an input for the QAOA algorithm on quantum gate systems or as an input for quantum annealers. This mapping is performed by a 3sat-to-QUBO transformation. Recently, it has been shown that the choice of the 3sat-to-QUBO transformation can significantly impact the solution quality of quantum annealing. It has been shown that the solution quality can vary up to an order of magnitude difference in the number of correct solutions received, depending solely on the 3sat-to-QUBO transformation. An open question is: what causes these differences in the solution quality when solving 3sat-instances with different 3sat-to-QUBO transformations? To be able to conduct meaningful studies that assess the reasons for the differences in the performance, a larger number of different 3sat-to-QUBO transformations would be needed. However, currently, there are only a few known 3sat-to-QUBO transformations, and all of them were created manually by experts, who used time and clever reasoning to create these transformations. In this paper, we will solve this problem by proposing an algorithmic method that is able to create thousands of new and different 3sat-to-QUBO transformations, and thus enables researchers to systematically study the reasons for the significant difference in the performance of different 3sat-to-QUBO transformations. Our algorithmic method is an exhaustive search procedure that exploits properties of 4×4 dimensional pattern QUBOs, a concept which has been used implicitly in the creation of 3sat-to-QUBO transformations before, but was never described explicitly. We will thus also formally and explicitly introduce the concept of pattern QUBOs in this paper.
As contemporary quantum computers do not possess error correction, any calculation performed by these devices can be considered an involuntary approximation. To solve a problem on a quantum annealer, it has to be expressed as an instance of Quadratic Unconstrained Binary Optimization (QUBO). In this work, we thus study whether systematically approximating QUBO representations of the MAX-3SAT problem can improve the solution quality when solved on contemporary quantum hardware, compared to using exact, non-approximated QUBO representations. For a MAX-3SAT instance consisting of a 3SAT formula withnnnvariables andmmmclauses, we propose a method of systematically creating approximate QUBO representations of dimension(n×n)(n\times n)(n×n), which is significantly smaller than the QUBO matrices of any exact, non-approximated MAX-3SAT QUBO transformation. In an empirical evaluation, we demonstrate that using our QUBO approximations for solving MAX-3SAT problems on D-Wave's quantum annealer Advantage_System6.4 can yield better results than using state-of-the-art exact QUBO transformations. Furthermore, we demonstrate that using naive QUBO approximation methods, based on removing values from exact(n+m)×(n+m)−dimensional(n+m)\times(n+m)-\mathbf{dimensional}(n+m)×(n+m)−dimensionalQUBO representations of MAX-3SAT instances, is ineffective.
The increasing complexity of computational problems in various fields entails the development of efficient methods to solve them. Thus, the emerging technology of quantum computers comes with algorithms, such as quantum annealing, that could solve optimization problems exponentially faster. In particular, to solve the 3SAT problem on quantum annealers, it must be transformed into an instance of Quadratic Unconstrained Binary Optimization (QUBO). Given that the choice of 3SAT-to-QUBO transformation affects the solution quality on quantum annealing, an algorithmic method for creating numerous 3SAT-to-QUBO transformations has recently been proposed, aiming to investigate more deeply such effect. This represents a challenge when deciding which is the best performing 3SAT-to-QUBO transformation that should be used when solving a 3SAT instance on quantum annealing. To overcome this issue, this work investigates the impact of different 3SAT-to-QUBO transformations on the solution quality of simulated annealing, as a classical analogue to quantum annealing. We demonstrate that different QUBO encodings of the same 3SAT instance can lead to different outcomes in terms of energy and clause satisfaction. We also reveal some correlations between 3SAT features, QUBO structural properties, and solution quality. These findings underscore the importance of the choice of 3SAT-to-QUBO transformation in simulated annealing, and provide a foundation for the future development of machine learning models for guiding encoding choices in both classical and quantum environments.
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.
There is no known polynomial-time algorithm that can solve an NP problem. Evolutionary search has been shown to be a viable method of finding acceptable solutions within a reasonable time period. Recently quantum computers have surfaced as another alternative method. But these two methods use radically different philosophies for solving NP problems even though both search methods are non-deterministic. This paper uses instances of {\bf SAT}, {\bf 3SAT} and {\bf TSP} to describe how these two methods differ in their approach to solving NP problems.