On Solving Structured SAT on Ising Machines: A Semiprime Factorization Study

Abstract

Ising machines are emerging as a new technology for solving various classes of computationally hard problems of practical importance, yet their limits on structured SAT workloads, representative of numerous real-world applications, remain unexplored. We present the first systematic study of such problems, using semiprime factorization as a representative case. Our results show that highly restrictive, 'tight' constraints, when mapped into optimization form, fundamentally distort Ising dynamics, and that these distortions are amplified when problems are decomposed to fit within limited hardware. We propose a hybrid approach that offloads constraint-heavy components to classical preprocessing while reserving the computationally challenging part for the Ising machine. Structured SAT represents a crucial step toward real-world applications, which remain out of reach today due to Ising machine limitations. Our findings reveal that constraint handling is a central obstacle and highlight hybrid hardware-software approaches as the path forward to unlocking the long-term potential of Ising machines. We conduct our evaluation on the manufactured Ising chips and demonstrate that our flow more than doubles the solvable problem size on a 45-spin all-to-all Ising chip, from 8-bit (94 variables) to 11-bit (190 variables), without hardware changes.