Accelerating Hybrid XOR$-$CNF SAT Problems Natively with In-Memory Computing

TL;DR

The work tackles the challenge of efficiently solving hybrid XOR--CNF SAT problems by proposing a native XOR--CNF solver implemented on in-memory computing hardware. It introduces WalkSAT-XNF, a full-neighborhood gradient-based local search that operates directly on XNF representations, and an IMC accelerator architecture using memristor crossbars to evaluate CNF and XOR clauses in parallel. Experimental demonstrations with TaO$_x$ memristors and 28-nm simulations show significant improvements: up to roughly 10× faster and up to 1000× more energy-efficient than CPU-based solvers, with a substantial chip-area reduction when using XNF. The results indicate strong potential for energy-efficient, high-throughput hardware solvers for cryptographic and industrial SAT problems, and point to scalable paths via multi-tile crossbar deployments and integrated preprocessing strategies.

Abstract

The Boolean satisfiability (SAT) problem is a computationally challenging decision problem central to many industrial applications. For SAT problems in cryptanalysis, circuit design, and telecommunication, solutions can often be found more efficiently by representing them with a combination of exclusive OR (XOR) and conjunctive normal form (CNF) clauses. We propose a hardware accelerator architecture that natively embeds and solves such hybrid CNF$-$XOR problems using in-memory computing hardware. To achieve this, we introduce an algorithm and demonstrate, both experimentally and through simulations, how it can be efficiently implemented with memristor crossbar arrays. Compared to the conventional approaches that translate CNF$-$XOR problems to pure CNF problems, our simulations show that the accelerator improves computation speed, energy efficiency, and chip area utilization by $\sim$10$\times$ for a set of hard cryptographic benchmarking problems. Moreover, the accelerator achieves a $\sim$10$\times$ speedup and a $\sim$1000$\times$ gain in energy efficiency over state-of-the-art SAT solvers running on CPUs.

Figures (8)

• Figure 1: (a) XNF SAT instance containing CNF and XOR clauses and a solution that certifies its satisfiability. (b) Strategies for converting CNF instances to XNF instances. (c) Average variable and clause compression rates obtained by the preprocessing strategies on three classes of XNF problems. Error bars show the standard deviation. (d) Advantages in iterations-to-solution for the WalkSAT-XNF heuristic when comparing different problem representations to the CNF formulation. The box-and-whiskers plots shows the median and interquartile range.
• Figure 2: Hardware architecture for implementing WalkSAT-XNF with IMC. An iteration of WalkSAT-XNF is performed sequentially by the register (1), clause lookup crossbar array (2), clause evaluation circuits (3), make and break computation crossbar array (4), gradient computation (5), winner-takes-all circuit (6), and variable flip (7). The function of these elements is shown for the example SAT problem in Fig. \ref{['fig1']}a and an initial variable assignment $x_1=1$, $x_2=1$, $x_3=0$, and $x_4=1$.
• Figure 3: (a) Conductance map of the memristor crossbar arrays used for clause evaluation (array 1) and make and break value computations (array 2). (b) Histogram of the conductance values in array 1. (c) Histogram of the output currents of array 1 for 400 random variable assignments. The histogram is split and coloured according to the expected number of true literals. Vertical lines indicate the discretization levels applied for clause evaluation. (d) Cumulative success rate when solving the par-8-1-c problem instance when implemented experimentally in the memristor crossbar arrays and simulations of Algorithm \ref{['alg:walksat-fn']} for $\sigma=2.5$. (e) Comparison of iterations-to-solution values for different noise levels between experiments and simulations. Errorbars for (d) and (e) depict the standard error noori2025repeats.
• Figure 4: (a) Relative crossbar area between XNF and CNF benchmarking instances. (b) Average energy per iteration of WalkSAT-XNF for XNF and CNF benchmarking instances. (c) and (d) Relative contribution of the different hardware components to the energy consumption for the CNF and XNF representations of the benchmarking instances "McEliece" (c) and "MDP" (d).
• Figure 5: (a) Relative speedup of XNF over CNF (top) and TTS for the XNF and CNF representations (bottom) for the benchmarking instances using WalkSAT-XNF. (b) Relative energy advantage (top) and ETS for the XNF and CNF representations (bottom) for the benchmarking instances using WalkSAT-XNF. No data is shown for p-16-5, as no solution was found for the CNF representation.