Boolean satisfiability (SAT) continues to serve as the fundamental NP-Complete problem of computer science, where many practical problems in cryptography, circuit design, and verification have been translated into large SAT problems. Many hardware approaches rely on clause evaluation, which can become computationally infeasible on traditional von Neumann architectures. Crossbar arrays with emerging nonvolatile memory (NVM) devices provide a fast solution for vector-matrix multiplication (VMM), and clause evaluation can be expressed as a VMM. Leveraging the power of Computing-in-Memory (CiM) we introduce SATurn, a ferroelectric field-effect transistor (FeFET)-based architecture for performing stochastic local search (SLS) with the WalkSAT-XNF heuristic on SAT problems. We compare our design with two other CiM SLS SAT solver architectures, achieving energy consumption improvements of up to 5.72 × for clause evaluation, 6.52 × for heuristic calculation, and 20.63 × for the make/break value computations under the same latency constraints.

Inspired by the human brain, Hyperdimensional Computing (HDC) processes information efficiently by operating in high-dimensional space using hypervectors. While previous works focus on optimizing pregenerated hypervectors in software, this study introduces a novel on-the-fly vector generation method in hardware with $O(1)$ complexity, compared to the $O(N)$ iterative search used in conventional approaches to find the best orthogonal hypervectors. Our approach leverages Hadamard binary coefficients and unary computing to simplify encoding into addition-only operations after the generation stage in ASIC, implemented using inmemory computing. The proposed design significantly improves accuracy and computational efficiency across multiple benchmark datasets.