Augmented Electronic Ising Machine as an Effective SAT Solver

TL;DR

This paper introduces an augmented Ising machine with cubic interactions and a semantic-aware annealing schedule, significantly improving SAT solving efficiency over existing methods and demonstrating robustness against noise.

Contribution

It proposes a novel augmented Ising machine architecture with cubic interactions and a semantic-aware annealing schedule for more effective SAT solving.

Findings

AIMS outperforms state-of-the-art SAT solvers by orders of magnitude.

Adding cubic interactions improves the Ising machine's capability for SAT problems.

The proposed approach is robust against device variation and noise.

Abstract

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.