Presentation
Chameleon-SAT: An Adaptive Boolean Satisfiability Accelerator Using Mixed-Signal In-Memory Computing for Versatile SAT Problems
DescriptionBoolean satisfiability (SAT), the first proven non-deterministic polynominal (NP)-complete problem, is crucial in data-intensive applications. Different applications have a wide spectrum of SAT problem sets (scale, complexity), also the various solution requirements (algorithm completeness, speed). The current SAT solvers are insufficient to provide an optimal solution under different scenarios.
In this work, we designed the Chameleon-SAT, an adaptive SAT accelerator using mixed-signal in-memory computing which support local search, DPLL and CDCL algorithms, and yet leverage the efficient mixed-signal computing architecture, achieving orders of magnitude improvement in speed compared to the prior SAT solvers. By judiciously selecting the reconfiguration mode, Chameleon-SAT are able to solve a wide range of the SAT problems achieving small-scale, high-complexity cases ($ \geq 90 \times$ for 20 variables/ 86 clauses, satisfiable problems), medium-scale, structured ($ \geq 19 \times$ for 50 variables/ 215 clauses, unsatisfiable problems) and large-scale, high-complexity cases ($ \geq 7 \times$ for 100 variables/ 430 clauses, satisfiable problems).
In this work, we designed the Chameleon-SAT, an adaptive SAT accelerator using mixed-signal in-memory computing which support local search, DPLL and CDCL algorithms, and yet leverage the efficient mixed-signal computing architecture, achieving orders of magnitude improvement in speed compared to the prior SAT solvers. By judiciously selecting the reconfiguration mode, Chameleon-SAT are able to solve a wide range of the SAT problems achieving small-scale, high-complexity cases ($ \geq 90 \times$ for 20 variables/ 86 clauses, satisfiable problems), medium-scale, structured ($ \geq 19 \times$ for 50 variables/ 215 clauses, unsatisfiable problems) and large-scale, high-complexity cases ($ \geq 7 \times$ for 100 variables/ 430 clauses, satisfiable problems).
Event Type
Research Manuscript
TimeMonday, June 232:00pm - 2:15pm PDT
Location3002, Level 3
Design
DES2B: In-memory and Near-memory Computing Architectures, Applications and Systems