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

TL;DR

This work systematically analyzes solving structured SAT workloads on Ising machines, using semiprime factorization as a representative case. It reveals that tight constraints induced by arithmetic CNF encodings distort Ising dynamics and are amplified by decomposition, and it proposes a hybrid CNF preprocessing plus decomposition flow to mitigate these effects. Through experiments on 8×45-spin CMOS Ising chips, the authors demonstrate a substantial increase in solvable problem size—from 8-bit to 11-bit semiprimes—without hardware changes, illustrating the practical potential of hardware-software co-design. The results emphasize constraint handling as a central bottleneck and argue that hybrid flows are a promising path to unlock Ising machines’ long-term utility for real-world, structured optimization problems.

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.

Figures (13)

• Figure 1: Proposed Hybrid Flow
• Figure 2: 2SAT Conditioning Decision Flow
• Figure 3: Replaced Value Propagation
• Figure 4: Clause Cleaning
• Figure 5: Impact of tightly-constrained variable branching considering an 8-bit semiprime factorization example.