29.2 Snap-SAT: A One-Shot Energy-Performance-Aware All-Digital Compute-in-Memory Solver for Large-Scale Hard Boolean Satisfiability Problems
Shanshan Xie, Mengtian Yang, S. Andrew Lanham, Yipeng Wang, Meizhi Wang, Sirish Oruganti, Jaydeep P. Kulkarni
Abstract
Boolean satisfiability (SAT) is a non-deterministic polynomial time (NP)-complete problem with many practical and industrial data-intensive applications [1]. Examples (Fig. 29.2.1) include anti-aircraft mission planning in defense, gene prediction in vaccine development, network routing in the data center, automatic test pattern generation in electronic design automation (EDA), and model checking in software. The objective of a SAT solver is to identify the values of <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$n$</tex> Boolean variables <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$x_{i}$</tex> that satisfy all clauses in a conjunctive normal form (CNF) [5]. However, the time required to determine the satisfiability of a SAT problem increases exponentially with respect to the variable size, which is energy and resource-consuming. A prior software SAT solver [3] requires frequent data transfer and memory access due to the CPU computations, solution-search, and repetitive variable updates, increasing the computational latency and energy cost. Another approach to designing a SAT solver is to leverage a continuous-time dynamical system using analog circuitry [5]. However, such dedicated analog arithmetic components incur a large area and energy overhead as they cannot be reused during non-SAT applications. Moreover, the analog SAT computations necessitate frequent SRAM read/write access which increase hardware implementation costs. Therefore, there is a critical need for advancing energy and area-efficient hardware SAT solver designs.