In-Memory Continuous-Time SAT Solver Based on Bidirectional 11-T SRAM Macro

Abstract

We propose a scalable continuous-time (CT) Boolean satisfiability (SAT) solver based on a bidirectional 11-T SRAM macro for solving hard SAT instances in the analog domain. Unlike conventional digital or clocked mixed-signal SAT solvers, the proposed system operates asynchronously using capacitor-based gradient integration, eliminating the need for clocking and maximizing the parallelism offered by in-memory computing (IMC). The 11T SRAM cell array supports both forward and backward in-memory operations, enabling massively parallel evaluation of clauses and make/break values, respectively, through current-mode multiply-accumulate operations. To improve solving efficiency, we introduce a gating scheme that selectively activates the dynamics, which can reduce unnecessary updates and minimize energy consumption. We verify the proposed solver with circuit simulation using GlobalFoundries 55 nm CMOS technology, and analyze scalability and performance across various SAT benchmarks. The solver achieves an average time-to-solution (TTS) of 1.36 mu s on 50-variable SAT instances, which results in a reduced TTS and energy-to-solution by 67.9% and 44.3%, respectively, compared to the prior CT SAT solver. These results demonstrate the potential of in-memory CT solvers as efficient, scalable hardware accelerators for SAT problems.