Efficient Digital Quadratic Unconstrained Binary Optimization Solvers for 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.

10 pages, 2 figures

References in corpus (13)

• Ising formulations of many NP problems
• Quantum Approximate Optimization Algorithm: Performance, Mechanism, and Implementation on Near-Term Devices
• The random K-satisfiability problem: from an analytic solution to an efficient algorithm
• Warm-starting quantum optimization
• Error corrected quantum annealing with hundreds of qubits
• Reachability Deficits in Quantum Approximate Optimization
• Hiding solutions in random satisfiability problems: A statistical mechanics approach
• MAX 2-SAT with up to 108 qubits
• A Direct Mapping of Max k-SAT and High Order Parity Checks to a Chimera Graph
• Quantum Approximate Optimization Algorithm with Adaptive Bias Fields
• Quantum Computational Phase Transition in Combinatorial Problems
• Quantum annealing for hard 2-SAT problems : Distribution and scaling of minimum energy gap and success probability
• SAT, Gadgets, Max2XOR, and Quantum Annealers