Chameleon-SAT: an Adaptive Boolean Satisfiability Accelerator Using Mixed-Signal In-Memory Computing for Versatile SAT Problems

Boolean satisfiability (SAT), the first proven non-deterministic polynominal-complete problem, is crucial in dataintensive applications. Different applications have a wide spectrum of SAT problem sets (scale, complexity) and also various solution requirements (algorithm completeness, speed). Current SAT solvers are insufficient for providing ideal solutions under different scenarios. This work presents the Chameleon-SAT, the first ASIC-based SAT accelerator that can support local search, Davis-Putnam- Logemann-Lovel, Conflict-Driven Clause Learning algorithms, while leveraging the efficient mixed-signal inmemory computing architecture to achieve orders-of-magnitude improvements in speed compared to the prior SAT solvers. By judiciously selecting the reconfiguration mode, Chameleon-SAT is able to solve a wide range of the SAT problems to achieve smallscale, high-complexity cases (>= 90x for 20 variables/ 86 clauses, satisfiable problems), medium-scale, structured cases (>= 19x for 50 variables/ 215 clauses, unsatisfiable problems), and largescale, high-complexity cases (>= 7x for 100 variables/ 430 clauses, satisfiable problems).