Efficient Digital Quadratic Unconstrained Binary Optimization Solvers for SAT Problems

TL;DR

This paper introduces an efficient digital QUBO solver approach for 3-SAT problems, providing a novel conversion method and demonstrating state-of-the-art accuracy on benchmark instances, thus broadening the applicability of quantum-inspired solvers.

Contribution

The paper presents a new 2-step conversion from 3-SAT to QUBO with a rigorous proof, enabling digital QUBO solvers to effectively solve large 3-SAT instances.

Findings

Achieved state-of-the-art accuracy on 78-variable 3-SAT benchmarks.

Developed a rigorous method to relate QUBO solutions to original SAT clause satisfaction.

Facilitated the use of quantum and quantum-inspired solvers for complex SAT problems.

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 (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 rigorous proof to explicitly 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 (NISQ) devices, as well as their quantum-inspired digital counterparts, for solving 3-SAT problems.