UMBC ebiquity
American Geophysical Union, Fall Meeting 2018, abstract #IN41B-27
Solving Hard SAT Instances with Adiabatic Quantum Computers
December 10, 2018
Regardless of debates between "P" and "NP", current classical computers can only approximate global optimum solutions through applying heuristics and meta-heuristics. Despite remarkable advancements that have been provided through distributing the computations over many processing units, exploring exponentially large spaces is still out of reach for indecomposable problems. Boolean satisfiability problem (SAT) plays a cornerstone role for countless complex real-world problems -ranging from model checking and fault diagnosis to planning and scheduling. Unlike many NP-hard problems (such as optimization instances) approximating the global optimum solution cannot satisfy the propositional logic formulas. We propose a novel quantum annealer based SAT solver that provides significantly higher performance and robustness compared to current quantum SAT solvers. From the performance point of view, acknowledging the fact that fabricating the quantum annealers is restricted to the sparse connectivity architectures, our SAT solver utilizes the available qubits more efficiently through applying high-performance computing for mapping the SAT instances into quadratic unconstrained binary objective functions. From robustness attitude, the probability of determining the satisfiable SAT instances as unsatisfiable in our model approaches zero by employing the central limit theorem. To evaluate our approach, we have applied D-Wave quantum annealer with more than 2,000 qubits for solving hard SAT instances. Experimental results revealed that our quantum annealer based SAT solver demonstrates a more robust behavior.
American Geophysical Union,
Abstract only