Augmented Electronic Ising Machine as an Effective SAT Solver
This addresses the problem of solving NP-complete optimization problems like SAT more efficiently for applications in computing, though it is incremental as it builds on existing Ising machine paradigms.
The paper tackled the challenge of using Ising machines to solve satisfiability (SAT) problems, showing that a basic architecture fails to accelerate 3-SAT due to lack of cubic interactions and efficient randomization, but an augmented version with cubic support and a novel semantic-aware annealing schedule outperforms state-of-the-art SAT solvers by orders of magnitude.
With the slowdown of improvement in conventional von Neumann systems, increasing attention is paid to novel paradigms such as Ising machines. They have very different approach to NP-complete optimization problems. Ising machines have shown great potential in solving binary optimization problems like MaxCut. In this paper, we present an analysis of these systems in satisfiability (SAT) problems. We demonstrate that, in the case of 3-SAT, a basic architecture fails to produce meaningful acceleration, thanks in no small part to the relentless progress made in conventional SAT solvers. Nevertheless, careful analysis attributes part of the failure to the lack of two important components: cubic interactions and efficient randomization heuristics. To overcome these limitations, we add proper architectural support for cubic interaction on a state-of-the-art Ising machine. More importantly, we propose a novel semantic-aware annealing schedule that makes the search-space navigation much more efficient than existing annealing heuristics. With experimental analyses, we show that such an Augmented Ising Machine for SAT (AIMS), outperforms state-of-the-art software-based, GPU-based and conventional hardware SAT solvers by orders of magnitude. We also demonstrate AIMS to be relatively robust against device variation and noise.