3SAT on an All-to-All-Connected CMOS Ising Solver Chip

TL;DR

This paper demonstrates solving 3SAT, an NP-complete problem, on a CMOS-based all-to-all-connected Ising hardware chip by exploring problem formulations, decomposition strategies, and hardware mapping to improve solution quality.

Contribution

It introduces a comprehensive framework for mapping 3SAT problems onto CMOS Ising hardware, addressing practical challenges and optimizing solution strategies.

Findings

Decomposition and mapping strategies significantly improve SAT solution quality.

Without the proposed methods, the hardware cannot solve SATLIB benchmarks.

Experimental results validate the effectiveness of the proposed approaches.

Abstract

This work solves 3SAT, a classical NP-complete problem, on a CMOS-based Ising hardware chip with all-to-all connectivity. The paper addresses practical issues in going from algorithms to hardware. It considers several degrees of freedom in mapping the 3SAT problem to the chip - using multiple Ising formulations for 3SAT; exploring multiple strategies for decomposing large problems into subproblems that can be accommodated on the Ising chip; and executing a sequence of these subproblems on CMOS hardware to obtain the solution to the larger problem. These are evaluated within a software framework, and the results are used to identify the most promising formulations and decomposition techniques. These best approaches are then mapped to the all-to-all hardware, and the performance of 3SAT is evaluated on the chip. Experimental data shows that the deployed decomposition and mapping strategies impact SAT solution quality: without our methods, the CMOS hardware cannot achieve 3SAT solutions on SATLIB benchmarks.