Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

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

TL;DR

This work tackles the challenge of converting MAX-3SAT instances into QUBO representations suitable for quantum annealing by automating the transformation process with evolutionary algorithms. It introduces two complementary EA-based methods: one to automatically create Pattern QUBOs for individual 3SAT clauses, and another to select per-clause Pattern QUBOs to assemble a complete MAX-3SAT QUBO, enabling diverse solution landscapes. Through extensive experiments on 500- and 1000-clause formulas, the proposed methods outperform several baselines and show competitive performance against state-of-the-art approaches, including on real quantum hardware, demonstrating practical potential for automated QUBO design. The results indicate that evolutionary search can efficiently generate principled QUBO structures, reducing manual effort and offering adaptability to solver and hardware characteristics with implications for scalable quantum optimization of SAT-related problems.

Abstract

A common way of solving satisfiability instances with quantum methods is to transform these instances into instances of QUBO, which in itself is a potentially difficult and expensive task. State-of-the-art transformations from MAX-3SAT to QUBO currently 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, therefore, algorithmically inefficient, we see potential for including search-based optimization. In this paper, we propose two methods of using evolutionary algorithms to automatically create QUBO representations of MAX-3SAT problems. 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.

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

TL;DR

This work tackles the challenge of converting MAX-3SAT instances into QUBO representations suitable for quantum annealing by automating the transformation process with evolutionary algorithms. It introduces two complementary EA-based methods: one to automatically create Pattern QUBOs for individual 3SAT clauses, and another to select per-clause Pattern QUBOs to assemble a complete MAX-3SAT QUBO, enabling diverse solution landscapes. Through extensive experiments on 500- and 1000-clause formulas, the proposed methods outperform several baselines and show competitive performance against state-of-the-art approaches, including on real quantum hardware, demonstrating practical potential for automated QUBO design. The results indicate that evolutionary search can efficiently generate principled QUBO structures, reducing manual effort and offering adaptability to solver and hardware characteristics with implications for scalable quantum optimization of SAT-related problems.

Abstract

A common way of solving satisfiability instances with quantum methods is to transform these instances into instances of QUBO, which in itself is a potentially difficult and expensive task. State-of-the-art transformations from MAX-3SAT to QUBO currently 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, therefore, algorithmically inefficient, we see potential for including search-based optimization. In this paper, we propose two methods of using evolutionary algorithms to automatically create QUBO representations of MAX-3SAT problems. 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.
Paper Structure (16 sections, 4 equations, 2 figures, 4 tables)

This paper contains 16 sections, 4 equations, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Foundations
  3. Satisfiability Problems
  4. Quadratic Unconstrained Binary Optimization (QUBO)
  5. Pattern QUBOs
  6. Population-Based Optimization
  7. Related Work
  8. Method
  9. Evolutionary Pattern QUBO Creation
  10. Evolutionary Pattern QUBO Selection
  11. Baselines
  12. Experiments
  13. Evaluation EA QUBO Search
  14. Evaluation EA QUBO Selection
  15. Conclusion & Future Work
  16. ...and 1 more sections

Figures (2)

  • Figure 1: Frequency over time (a) and distribution of found pattern types (b) in evolutionary search across three smaller integer spaces: $[-1, 1], [-2, 2]$, and $[-3, 3]$ over 2 runs each. Comparisons are made between searches for correct patterns (b, left), patterns with an energy gap requirement (here gap:$1$, b, mid-left), patterns with a sparsity requirement (here sparsity:$7$, b, mid-right), and patterns satisfying both gap and sparsity constraints (b, right). Each run consists of $5000$ total generations ($500$ repetitions of fresh populations evolving over $10$ generations, $100$ individuals per population with mut-rate, rec-rate$= 0.5$, elt-rate, mig-rate$=0.1$). To show adaptability to larger ranges we repeat the experiment of finding correct patterns over time (c) and the corresponding count per pattern type (d) with three big spaces ($[-10, 10], [-20, 20]$, and $[-40, 40]$) as well. Each of the $3$ runs in (c,d) consists of $10,000$ total generations ($100$ repetitions of fresh populations evolving over $100$ generations, $300$ individuals per population with mut-rate, rec-rate$= 0.5$, elt-rate, mig-rate$=0.1$).
  • Figure 2: Evolutionary pattern selection across datasets with varying clause length and clause complexity. (a) Performance distribution on a 500-clause dataset with a standard difficulty ratio, showcasing the number of clauses satisfied by our EA (blue) in comparison to baseline methods chancellor (gold), fixed-patterns (teal) and individual-pattern (grey). (b) Outcomes on a more complex 1000-clause dataset against the same baselines. (c) Performance of the EA on a 500-clause dataset using the D-Wave Advantage_system6.4 quantum computer, compared to chancellor, nüsslein (violet) and random guessing (brown) indicating the transfer-ability of EA optimizations from proxy solvers to actual quantum hardware. Results are obtained using parameters of 100 individuals over 50 generations, 5-tabu reads with 150ms timeout for the EA, and best results of $50*5$-tabu reads (also 150ms timeout) for all other baselines.

Theorems & Definitions (3)

  • Definition 1: Boolean formula arora2009computational
  • Definition 2: Conjunctive Normal Form arora2009computational
  • Definition 3: QUBO glover2018tutorial