Efficient Digital Quadratic Unconstrained Binary Optimization Solvers for SAT Problems

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.LINK

Code is open-sourced at LINK

Joint work with Y. Song and A. Yosifov

Robert Simon Fong, Yanming Song, and Alexander Yosifov. Efficient digital quadratic unconstrained binary optimization solvers for sat problems. New Journal of Physics, 27(1):013027, Jan 2025
Download Paper