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

TL;DR

This study explores the limitations of Ising machines in solving structured SAT problems, using semiprime factorization as a case, and proposes a hybrid approach to improve their problem-solving capacity.

Contribution

It is the first systematic analysis of structured SAT on Ising machines, revealing how constraint complexity affects their performance and proposing a hybrid classical-quantum method.

Findings

Hybrid approach more than doubles solvable problem size.

Constraint handling is a key obstacle for Ising machines.

Demonstrated increased problem size from 94 to 190 variables on a 45-spin chip.

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.