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

TL;DR

This paper introduces two evolutionary algorithm-based methods to automate the creation of QUBO representations for MAX-3SAT problems, improving efficiency and achieving competitive results with existing approaches using classical and quantum solvers.

Contribution

It presents novel search-based methods using evolutionary algorithms for automatic QUBO construction from MAX-3SAT instances, replacing manual or exhaustive approaches.

Findings

Achieved competitive performance with state-of-the-art baselines.

Validated methods on 500- and 1000-clause 3SAT formulas.

Demonstrated effectiveness with both classical and quantum annealing solvers.

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.