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.

翻译：随着传统冯·诺依曼架构性能提升的放缓，伊辛机等新型计算范式日益受到关注。这类系统对NP完全优化问题采用了截然不同的求解方法。伊辛机在解决MaxCut等二元优化问题上展现了巨大潜力。本文针对可满足性问题（SAT）对这类系统进行了分析。我们证明，对于3-SAT问题，基本架构无法产生有意义的加速，这在很大程度上归因于传统SAT求解器的持续进步。然而，深入分析表明部分失败源于缺少两个关键组件：三次相互作用和高效随机化启发策略。为克服这些局限，我们在最先进的伊辛机上增加了针对三次相互作用的架构支持。更重要的是，我们提出了一种新颖的语义感知退火调度策略，其搜索空间导航效率远超现有退火启发方法。通过实验分析证明，这种增强型SAT伊辛机（AIMS）在数量级上优于最先进的基于软件、GPU和传统硬件的SAT求解器。我们还验证了AIMS对器件变异和噪声具有较好的鲁棒性。