Transformation-Dependent Performance-Enhancement of Digital Annealer for 3-SAT

TL;DR

This paper investigates how different transformations from 3-SAT to QUBO affect the performance of the Digital Annealer, introducing a novel transformation that enhances solution quality and demonstrating its superiority over quantum annealers on hard instances.

Contribution

It introduces a new transformation method for 3-SAT to QUBO that reduces auxiliary variables and improves Digital Annealer performance, supported by performance analysis.

Findings

The novel transformation improves solution quality.

Digital Annealer outperforms quantum annealer on hard 3-SAT instances.

Transformation choice significantly impacts solver performance.

Abstract

Quadratic Unconstrained Binary Optimization (QUBO) problems are NP-hard problems and many real-world problems can be formulated as QUBO. Currently there are no algorithms known that can solve arbitrary instances of NP-hard problems efficiently. Therefore special-purpose hardware such as Digital Annealer, other Ising machines, as well as quantum annealers might lead to benefits in solving such problems. We study a particularly hard class of problems which can be formulated as QUBOs, namely Boolean satisfiability (SAT) problems, and specifically 3-SAT. One intriguing aspect about 3-SAT problems is that there are different transformations from 3-SAT to QUBO. We study the transformations' influence on the problem solution, using Digital Annealer as a special-purpose solver. Besides well-known transformations we investigate a novel in this context not yet discussed transformation, using less auxiliary variables and leading to very good performance. Using exact diagonalization, we explain the differences in performance originating from the different transformations. We envision that this knowledge allows for specifically engineering transformations that improve a solvers capacity to find high quality solutions. Furthermore, we show that the Digital Annealer outperforms a quantum annealer in solving hard 3-SAT instances.