30.3 VIP-Sat: A Boolean Satisfiability Solver Featuring 5×12 Variable In-Memory Processing Elements with 98% Solvability for 50-Variables 218-Clauses 3-SAT Problems

Boolean satisfiability (SAT), a non-deterministic polynomial (NP)-complete problem, has gained increasing attention with applications in artificial intelligence, machine learning, electronic design automation, and VLSI tests with practical examples, such as AI planning and ML model verification, fault diagnosis, combinational equivalence checking and automatic test pattern generation. The SAT problem is based on testing if a Boolean formula in conjunctive normal form (CNF) can be solved by finding a set of Boolean variables that satisfy the formula (i.e., makes the formula TRUE). Conventionally, software-based SAT-solving algorithms, such as WalkSAT, have been widely used. However, they have limitations in solving large-scale SAT problems with an increasing number of variables due to limited parallelism and a significant latency and energy overhead arising from frequent memory access. Alternatively, dedicated ASIC hardware SAT solvers have demonstrated solving SAT problems using various methods, such as in-memory computing [1], continuous-time dynamics [3], recurrent neural networks [4], and digital processing elements [6]. While most prior works [3–6] have demonstrated low solvability for hard problems with a large number of variables, a recent work [1] has achieved 72% solvability for solving a hard 3-SAT problem (i.e., a reduced SAT problem with at most 3 literals per clause) with 60 variables in 0.713ms while consuming 1.098μJ, which outperforms prior hardware solvers and achieved ~10× speed-up compared to a CPU (Xeon W-2195 at 4.2GHz). However, the prior work [1] operates based on a popular SAT-solving algorithm (WalkSAT), which may limit further advancement in solvability, solution time and energy consumption. In this work, we propose a novel algorithm-hardware co-designed SAT solver with a digital in-memory processing element architecture incorporating a key feature of parallel uncorrelated variable processing element (VPE) for column-by-column fast SAT solving operations with high solvability and minimum energy consumption. Measured results show 98% solvability for 50 variables and 218 clauses in 18.7μs consuming 20.8nJ.