SKI-SAT: A CMOS-compatible Hardware for Solving SAT Problems

TL;DR

The paper introduces SKI-SAT, a CMOS-based hardware system that efficiently solves SAT problems by mapping variables to capacitor voltages and using a network of coupling units, achieving significant speed and power improvements.

Contribution

A novel CMOS-compatible hardware architecture for SAT solving that employs capacitor voltage mapping and a unique perturbation scheme to enhance performance.

Findings

Over 10x faster solution times compared to existing solvers.

300x reduction in power consumption.

Demonstrated high performance through simulation results.

Abstract

Nature-inspired computation is receiving increasing attention. Various Ising machine implementations have recently been proven to be effective in solving numerous combinatorial optimization problems including maximum cut, low density parity check (LDPC) decoding, and Boolean satisfiability (SAT) problems. In this paper, a novel method is presented to solve SAT or MAX-SAT problems with a CMOS circuit implementation. The technique solves a SAT problem by mapping the SAT variables onto quantized capacitor voltages generated by an array of nodes that interact through a network of coupling units. The nodal interaction is achieved through coupling currents produced by the coupling units, which charge or discharge capacitor voltages, implementing a gradient descent along the SAT problem's cost function to minimize the number of unsatisfied clauses. The system also incorporates a unique low-complexity perturbation scheme to avoid settling in local minima, greatly enhancing the performance of the system. The simulation results demonstrate that the proposed SKI-SAT is a high-performance and low-energy alternative that surpasses existing solvers by significant margins, achieving more than 10 times faster solution and 300 times less power.