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.

本文讲述了基于 Ising 机的解决最优化问题方法。作者发现缺少了立方相互作用和高效的随机化启发式算法成为了失误的原因。最后，作者增加了一个合适的框架和一个新的方法，提高了搜索的效率，实验结果在以往硬件和软件求解最优化问题算法的基础上取得了更高的效果。