Solving Boolean satisfiability problems with resistive content addressable memories

TL;DR

The paper addresses the challenge of solving high-order SAT problems efficiently on hardware by introducing KLIMA, a k-local in-memory accelerator that combines resistive CAMs (TCAM) with Dot-Product Engines (DPEs) to map CNF-SAT natively without auxiliary variables. This hardware-software co-design enables parallel computation of make, break, and gain metrics to drive stochastic local search heuristics, achieving up to $182\times$ energy-to-solution improvements over digital baselines and compelling performance versus CPU WalkSAT. By leveraging in-memory computing and a native CNF representation, KLIMA reduces coupling term overhead and enables flexible exploration of solvers such as GNSAT, MNSAT, and WalkSAT variants. The results suggest KLIMA as a scalable building block for optimization and sampling workloads in heterogeneous systems, with substantial practical impact for industry-scale SAT and related optimization tasks.

Abstract

Solving optimization problems is a highly demanding workload requiring high-performance computing systems. Optimization solvers are usually difficult to parallelize in conventional digital architectures, particularly when stochastic decisions are involved. Recently, analog computing architectures for accelerating stochastic optimization solvers have been presented, but they were limited to academic problems in quadratic polynomial format. Here we present KLIMA, a k-Local In-Memory Accelerator with resistive Content Addressable Memories (CAMs) and Dot-Product Engines (DPEs) to accelerate the solution of high-order industry-relevant optimization problems, in particular Boolean Satisfiability. By co-designing the optimization heuristics and circuit architecture we improve the speed and energy to solution up to 182x compared to the digital state of the art.

Figures (8)

• Figure 1: (a) Conjunctive Normal Form (CNF) of a Boolean Satisfiability problem. (b) Solution tree of the formula in (a). Green leaves are satisfied solutions while red leaves are unsatisfied solutions. (c) Crossbar array of RRAM implementing a Dot Product Engine (DPE). (d) Hopfield Neural Network (HNN) for optimization using a DPE. (e) Example of energy landscape navigation with an HNN. (f) Mapping of the problem in (a) into a QUBO formulation for being solved with an HNN.
• Figure 2: (a) Content Addressable Memory (CAM) realized with a 2T2R RRAM structure, with the output current on the ML representing the Hamming distance of the input and the stored word. (b) Proposed $k-$Local Interactions In-Memory Accelerator (KLIMA) using TCAM for computing interactions and DPE for computing gradients. (c) Example of computing the make value $m$ using KLIMA on the formula in Fig. \ref{['fig:intro']}. First, the interactions between variables are evaluated using the TCAM by computing ML which is then compared with a sense amplifier (SA) to threshold $\text{MLm}=\text{ML}<\Theta_h$ in order to evaluate the location of violated clauses. Then $\text{MLm}$ is used to compute $m$ with a dot product operation. (d) Computing the break value $b$ with KLIMA. The ML interactions are compared with two thresholds to evaluate which clauses are satisfied by only one literal, namely $\text{MLb}=(\Theta_l<\text{ML}<\Theta_h)$. $\text{MLb}$ is then used to compute the break count, by first accumulating the contribution of each member variable in a clause and comparing it with the current input $x$. (e) Computing the gain with KLIMA as $g=m-b$. (f) Mapping advantage of KLIMA compared to HNN in terms number of coupling terms $\Sigma$ as a function of order $k$ for random k-SAT problems at the computational phase transition.
• Figure 3: (a) Median ITS as a function of the number of variables for solving 3-SAT and (b) 4-SAT problems with multiple heuristics. (c) Median energy per cycle as a function of the number of variables for multiple KLIMA operations solving 3-SAT and (d) 4-SAT problems.
• Figure 4: (a) Median TTS as a function of the number of variables for solving 3-SAT and (b) 4-SAT problems with multiple heuristics. (c) Median energy per cycle as a function of the number of variables for multiple KLIMA operations solving 3-SAT and (d) 4-SAT problems.
• Figure S1: Conceptual operation of TCAM implemented with a crossbar array for multiple search (a,b,c,d,e,f) and compute (g) operations.