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

TL;DR

The simulation results demonstrate that the proposed SKI-SAT is a high-performance and low-energy alternative that surpasses existing software-based SAT solvers by significant margins, achieving more than 10 times faster solution and over 300 times less power.

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.

Figures (10)

• Figure 1: Example CMOS circuit for a computational node in SKI-SAT. The reset voltage $V_{CM}$ is typically chosen to be equal or close to threshold $V_{th}$ of the comparator.
• Figure 2: SKI-SAT top-level circuit architecture.
• Figure 3: Example unit element of the Variables-to-Clauses $N \times N_C$ array for a 3-SAT implementation.
• Figure 4: The CFCCS unit with clause perturbation logic and perturbation signal $P$, satisfiability signal $T_j$ and early termination signal $ETS$.
• Figure 5: Clause to the coupling current (C2CC) unit for a 3-literal SAT solver implementation.