Solving Max-3SAT Using QUBO Approximation

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 <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$n$</tex> variables and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$m$</tex> clauses, we propose a method of systematically creating approximate QUBO representations of dimension <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(n\times n)$</tex>, 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 <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(n+m)\times(n+m)-\mathbf{dimensional}$</tex> QUBO representations of MAX-3SAT instances, is ineffective.