Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing

Domain: physics
Published: 2026-02-19
Editorial outcome: major_revision

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 XOR–CNF 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 XOR–CNF problems to pure CNF problems, our simulations show that the accelerator improves computation speed, energy efficiency, and chip area utilization of in-memory accelerators by ~10× for a set of hard cryptographic benchmarking problems. Moreover, the accelerator achieves a ~10× speedup and a ~1000× gain in energy efficiency over state-of-the-art SAT solvers running on CPUs.

Introduction
The Boolean satisfiability (SAT) problem is a fundamental decision problem that was the first problem to be proven NP-complete1,2. Solving a SAT problem involves determining whether there is an assignment of Boolean variables satisfying a given propositional logic formula. Many problems in engineering and computer science reduce to SAT problems with a polynomial-time overhead, which then can be tackled with SAT solvers employing local search heuristics or exhaustive search. SAT solvers are thus widely employed in many industry-relevant applications, such as scheduling, planning, cryptanalysis, and integrated circuit design3,4, as well as being used as the engine for more-general constrained optimization solvers5. Yet, due to the computational complexity of SAT problems, the cost of finding solutions could, in the worst case, scale exponentially with the number of variables.

Due to the ubiquity of SAT problems in industrial optimization applications, there is an ongoing effort to improve algorithms for SAT solvers, as well as to develop dedicated hardware accelerators6–14 that can find solutions faster and more energy efficiently. A promising line of research has been the study of SAT solvers in hybrid problem formulations15–17. SAT problems are typically formulated in conjunctive normal form (CNF), where a set of clauses containing Boolean variables are connected by logical OR operations. However, many applications naturally involve clauses linked by exclusive-OR (XOR) operations, such as channel decoding in wireless receivers18, model counting15, circuit fault testing3, and cryptographic decoding attacks19. These problems can be formulated natively as hybrid XOR–CNF SAT problems containing both CNF and XOR clauses. Although XOR clauses can be reduced to CNF clauses using Tseitin transformations20, doing so introduces a significant performance overhead as it increases the number of variables and clauses in the problem. Hybrid XOR–CNF SAT solvers that support both CNF and XOR clauses have therefore been found to considerably outperform pure CNF SAT solvers17,21.

While hybrid XOR–CNF solvers have predominantly been implemented as software solutions running on digital computers16,22, there is potential in harnessing the benefits of native XOR–CNF problem formulations using in-memory hardware accelerators. In-memory computing (IMC), leveraging analog crossbar arrays for low latency and parallel linear algebra computations, is a promising technology for building hardware accelerators23. IMC accelerators have already demonstrated their ability to enhance both speed and energy efficiency for SAT solvers in the case of pure CNF SAT problems, outperforming conventional CPUs8,9,24. Combining the advantages of a hybrid XOR–CNF formulation with IMC hardware could offer considerable advantages in tackling computationally challenging SAT problems with inherent XOR clauses. However, compared to pure CNF problems, evaluating XOR clauses requires more complex and energy-intensive circuits that can potentially offset the efficiency and latency advantages of IMC hardware. Moreover, XOR clauses can contain many literals, whereas SAT hardware accelerators can often support only a few literals per clause. For IMC hardware, a large number of literals can also make it more challenging to retain low error rates during computation, as the corresponding analog signals exhibit an increased dynamic range.

Therefore, in this work, we set to address the open question of whether IMC is suitable for accelerating the solving of hybrid XOR–CNF problems efficiently. We present an IMC accelerator architecture that can be used to natively implement and solve hybrid XOR–CNF problems. As part of this architecture, we propose WalkSAT-XNF, an XOR-native implementation of the WalkSAT stochastic local search (SLS) heuristic, where all variables within unsatisfied clauses are candidates for being flipped. We propose an efficient method for XOR–CNF clause evaluation and gradient computation using analog crossbar arrays. To demonstrate feasibility on hardware, we experimentally implement WalkSAT-XNF on crossbar arrays based on TaOx memristors for a small-scale minimal disagreement parity (MDP) problem. Additionally, we simulate a memristor-based accelerator architecture in a 28 nm complementary metal-oxide-semiconductor (CMOS) process and evaluate the computation speed and energy consumption on benchmarking problems from cryptographic applications including the McEliece–Niederreiter cryptosystem25,26 and the Advanced Encryption Standard (AES)27,28. Compared to solving problems in their CNF representation with an IMC accelerator, our approach achieves an order-of-magnitude improvement in computation speed and energy consumption, within a 10 × smaller chip area, by employing hybrid XOR–CNF representations. Furthermore, compared to state-of-the-art SAT solvers running on CPUs, our accelerator solves benchmarking problems with up to 300 variables and 1016 clauses ~10× faster while consuming ~1000× less energy. Our results highlight the potential of IMC accelerators for efficiently implementing hybrid XOR–CNF SAT solvers, enabling native problem representations for solving a variety of complex industry-relevant problems.

Results
A SAT problem for a set of Boolean variables x i ∈{0,1} and clauses C i is given by the conjunction (∧)

F(x 1 ,...,x n )=C 1 ∧C 2 ∧...∧C i . (1)

The problem is said to be satisfiable if an assignment of the Boolean variables exists where all clauses C j are true. In a CNF representation, each C j is a clause formed from a disjunction (∨) of literals l k as C CNF,j=l k ∨⋯∨l m, where the literals l k are either propositions (x k) or their negations (x k) of the Boolean variables. XOR SAT problems, on the other hand, are SAT problems where clauses are formed using XOR operations (⊕) between literals:

C XOR,j=l k ⊕...⊕l m .

Problems formulated in XOR-and-OR normal form (XNF) are then hybrid XOR–CNF SAT problems, where the propositional logic formula (1) contains both CNF and XOR clauses. Figure 1a illustrates an XNF instance with three CNF and two XOR clauses. Here, the variable assignment x 1 = 1, x 2 = 0, x 3 = 0, x 4 = 1 guarantees satisfiability. In general, an XOR clause with k literals x 1 , …, x k can be equivalently represented using 2 k−1 CNF clauses, each containing k literals. These clauses represent all possible combinations of an even number of negated variables

C XOR,j= ±x 1 ⊕...⊕ ±x k ,

where ± denotes the possible permutations for propositions (+) of literals or their negations (−). For instance, the first XOR clause in Fig. 1a has the equivalent CNF representation (x 1 ∨x 2 ∨x 3 )∧(x 1 ∨x 2 ∨x 3 )∧(x 1 ∨x 2 ∨x 3 )∧(x 1 ∨x 2 ∨x 3 ). Translating XOR clauses into CNF clauses incurs an exponential increase in the number of additional clauses, hence making clause evaluation computationally more expensive.

In practice, this exponential overhead can partly be mitigated by employing the Tseitin transformation20, yet this method provides a clear trade-off between the reduction of overall clauses and the number of additional variables that need to be considered16. Conversely, translating a SAT problem in CNF representation into an XOR SAT problem is generally impossible, though many key SAT applications, such as integer factorization, circuit fault testing4, and cryptographic decoding attacks19, originate from XOR-based logic. In these cases, XOR clauses can be reconstructed from the CNF clauses by reversing the transformation in Eq. (2), typically reducing both clause and variable counts.

We demonstrate the differences between CNF and XNF formulations in Fig. 1 for SAT problems from cryptographic attacks on the McEliece–Niederreiter and AES cryptosystems, as well as instances generated from the minimal disagreement parity (MDP) problem (details of the instances are provided in the Methods section). All instances inherit native XOR clauses but are initially provided with CNF clauses only. We explore two methods of generating hybrid XOR–CNF instances from these original problems. First, we convert directly the CNF instances to the XNF representation employing the cnf2xnf tool within the xnfSAT solver16. The final representation of this process is denoted by XNF in Fig. 1b. After this conversion, the resulting problems contain 2–43% XOR clauses. Additionally, we employ a SAT preprocessing (PP) tool29 to the CNF instances (generating new instance denoted by CNF-PP in Fig. 1b) before applying the conversion tool to generate XNF instances. The final representation of this process is denoted by XNF-PP in Fig. 1b. Such preprocessing techniques are widely used to compress CNF problem size and to enhance solver performance. Details of the preprocessing procedure and the per-instance preprocessing runtime are reported in Section “Methods”.

Figure 1c shows the compression ratio for the number of variables in relation to the original CNF representation. Direct XNF conversion reduces the number of variables by (2.0 ± 0.5)× on average. When applying preprocessing, the average number of variables initially remains almost unchanged ((1.1±0.1)×) but is considerably reduced once the problem has been converted to an XNF representation. The preprocessing followed by XNF conversion achieves a compression ratio of (4.6±1.0)×, on average. We also analyze the compression ratio for the number of clauses in relation to the CNF representation. With direct XNF conversion, we find that the number of clauses is reduced by (3.7±1.2)×, on average. When applying preprocessing to the CNF representation, we again observe a small initial reduction in the number of clauses by (2.0 ± 0.9)×, while conversion of the preprocessed instances to an XNF representation reduces the number of clauses by (5.4 ± 1.8)×, on average, compared to the CNF representation.

These results show the advantages of mapping problems to an XNF representation, with the greatest benefits often observed when combining preprocessing with XNF conversion. Compared to using a pure CNF representation, the resulting reduction in the problem size can enhance SAT solver performance and significantly lowers compute resource requirements17,21. Moreover, for SAT hardware accelerators, the comparatively smaller XNF instances enable reduced chip sizes and energy consumption. Therefore, these results serve as a strong motivation to develop hardware accelerators capable of supporting both CNF and XOR clauses simultaneously.

To leverage the described mapping advantages, we propose a heuristic called WalkSAT-XNF, designed to solve XNF problems in their native form. We then show how this algorithm can be realized efficiently in an accelerator using IMC. WalkSAT-XNF employs a local search heuristic and is inspired by prior work on IMC accelerators for CNF SAT problems8. Similar to the widely used WalkSAT solvers30,31, WalkSAT-XNF computes gradients based on ‘make’ and ‘break’ values. The make value counts the number of violated clauses that become satisfied, while the break value counts the number of satisfied clauses that become violated when flipping a variable. WalkSAT-XNF then flips a variable found in violated clauses that maximizes the value obtained by subtracting the break value from the make value. In contrast to the standard WalkSAT heuristic, WalkSAT-XNF performs a full-neighborhood evaluation, where gradients for all variables present in unsatisfied clauses are considered, as opposed to evaluating only the variables in a randomly chosen violated clause.

Table 1 shows the pseudocode of the WalkSAT-XNF heuristic. The algorithm starts with an initial variable configuration and iteratively searches the space until it finds a solution or reaches the iteration limit. Each iteration computes gradients based on make and break values for all variables by evaluating the clauses in which they appear. A CNF clause is satisfied if at least one literal is true. Hence, the make value is the number of violated clauses containing the variable, as flipping it would satisfy them. The break value, on the other hand, corresponds to the number of satisfied clauses, where the variable is the only true literal, as flipping it would break clause satisfaction. For an XOR clause to be satisfied, an odd number of true literals is required. Thus, the make value corresponds to the number of violated clauses containing the variable, as flipping it would satisfy them. Similarly, break values are equal to the number of satisfied clauses containing the variable. The break value subtracted from the make value yields the gain value, or gradient. After computing the full gradient, Gaussian noise with a standard deviation σ is added to help escape local minima or avoid cycles. The variable with the highest noise-adjusted gain value is then flipped, and the process repeats.

Figure 1d shows the algorithmic efficiency of WalkSAT-XNF when solving the McEliece, MDP, and AES benchmarking instances using CNF-PP, XNF, and XNF-PP compared to the CNF formulation. We quantify the performance with the iterations-to-solution (ITS 99) metric32, defined as

ITS 99(iter) := iter * log(0.01) / log(1 - θ(iter)), (3)

where θ(iter) is the success probability of solving the problem as a function of iterations. The ITS 99 metric estimates the iterations required to observe at least one successful trial with a probability of 99%. Since WalkSAT-XNF stops once a solution is found, an optimized ITS 99opt metric can be obtained by evaluating ITS 99 at solution-finding trial lengths within reasonable error bounds. Compared to the CNF formulation, WalkSAT-XNF solves problems using fewer iterations, achieving a median improvement of ~23× (CNF-PP), ~10× (XNF), and ~68× (XNF-PP). The greatest performance gains are observed for preprocessed instances.

In what follows, we thus solely focus on the preprocessed instances for CNF and XNF problems, referring to them simply as CNF and XNF for brevity. Complete benchmarking results for all problem representations are available in Supplementary Note 1.

To realize WalkSAT-XNF with IMC hardware, we propose the accelerator architecture depicted in Fig. 2, which shows the steps performed in each iteration of the heuristic (i.e., clause evaluation, make and break value computations, and a variable update) using seven distinct hardware blocks.

The Boolean variable configuration is initially stored in a register ((1) in Fig. 2). The variables and their respective conjugates are then provided as an input signal to a crossbar array to evaluate violation of the individual CNF and XOR clauses (2). For problems with N variables and C clauses, the crossbar has 2N columns and C rows. The input to the crossbar is applied as binary voltage signals at the columns. Each variable x j and its negation x j are mapped to the column pairs {2j, 2j+1}, while clauses correspond to the rows of the crossbar. Each literal is represented by a binary-valued crossbar connection b ij ∈{0,1} that allows current to flow from a column to a row. Here, positive literals x j connect rows to columns with even indices 2j, while negative literals x j connect to columns with odd indices 2j+1. These connections are facilitated by memory devices at each crossbar that can be switched between an ON and an OFF state, such as resistive random-access memory (RRAM)8, static random-access memory (SRAM), or embedded Flash memory cells33. This crossbar array functions as a C-by-2N matrix, with entries of 1 where literals appear and 0 elsewhere. The output current at each row is then equivalent to a matrix–vector multiplication between the input signal and the array. Using the matrix encoding of the clauses described above, the output signals of the crossbar rows are proportional to the number of true literals in the clauses for the current assignment of variables.

Depending on the clause type, the output signals from the crossbar array are evaluated by the circuits (3) of Fig. 2. These circuits indicate whether a clause is violated and provide the input signals for the subsequent make and break value computations. For XOR clauses, a low-resolution analog-to-digital converter (ADC) with log 2(k) bits, where k is the maximum number of literals, performs a parity check using the least-significant bit (LSB). The LSB is provided as input for the break value computation, as it indicates whether the clause is currently satisfied and can be broken by flipping one of its member variables. Conversely, an inversion of the LSB is given as input for the make value computation. For CNF clause evaluations, two comparators8 determine if the number of true literals is 0 (for the make value) or 1 (for the break value). The outputs of these comparators are used as input for make and break computations.

The make and break values are computed via a crossbar array (4) that is the transpose of (2). After applying the input signals to the rows, the output signals from related pairs of columns are added to derive the make and break values for each variable. To calculate the break values for CNF clauses, the column outputs are additionally multiplied with the variable configuration using pass transistors to identify true literals. Adding the make and break values from XOR and CNF clauses provides the input signals for the subsequent gradient computation (5). Here, a Gaussian white noise signal σ generated by a pseudo-random number generator (PRNG) in conjunction with an array of digital-to-analog converters (DAC) is added to the make value, and the break values are subtracted from the make values using differential amplifiers to calculate the gradient for each variable. Finally, a winner-takes-all (WTA) circuit identifies the variable with the highest gradient (6) and the output signal is used to update the register state using XOR gates (7).

Crucially, the relative simplicity of WalkSAT-XNF enables us to map every computational step to an equivalent analog circuit, enabling rapid continuous computation. As with other IMC concepts8,34, the crossbar arrays in Fig. 2 enable parallel gradient computations for both the CNF and XOR clauses within a single clock cycle. Performing an entire operation of WalkSAT-XNF is achieved within just three clock cycles, without the need for a complex control system, while also circumventing frequent time-intensive communication with external co-processors or memory systems. Both XOR and CNF clauses can be evaluated using the same array, allowing for an area-efficient design. Moreover, the crossbar array can implement a number of literals per clause that is equal to the number of variables, hence supporting highly complex clauses common in industry workloads.

As with other mixed-signal computing systems, realizing WalkSAT-XNF in hardware requires it to be sufficiently resilient against hardware non-idealities in the analog circuits. Studies have identified variations in the RRAM cells and noise in the crossbar array’s analog readout circuit as the dominant non-idealities that can result in a deterioration in performance35. To evaluate the feasibility of realizing WalkSAT-XNF in hardware, we implement a hybrid version of the architecture in Fig. 2 on an RRAM crossbar array chip. We experimentally validate the analog computation of clause evaluation and make/break value computation using an RRAM crossbar array chip, while the register, the circuits for checking clause satisfaction, the WTA circuit, and the Gaussian noise injection are emulated on a digital computer. The RRAM chip is a custom CMOS circuit in a 180 nm technology node with back-end-of-the-line (BEOL) monolithically integrated TaOx 1T1M RRAM cells36,37. For the experiment, we use the XNF instance derived from the par-8-1-c MDP problem38, consisting of 13 variables and 42 clauses, including one XOR clause. To implement the crossbar’s ON and OFF states b ij, the RRAM cells are programmed to either a high-resistance state (HRS, or OFF state) or a low-resistance state (LRS, or ON state). Figure 3a shows the conductance values of the RRAM cells after programming. Here, the LRS is set to 100 μS and the HRS is set to 1 μS. Two separate arrays are used for the clause evaluation (array 1) and the make and break value computations (array 2). Figure 3b shows a histogram of the memristor conductances of array 1. The memristors exhibit typical device-to-device variations during programming39, where the LRS and HRS are programmed to have a tolerance of ±10 μS. While further optimization is possible40, we find that this accuracy is sufficient for our purposes.

To evaluate the capability of this crossbar array to perform clause evaluation (array 1 in Fig. 3a), we supply 400 random variable configurations as input signals and record the output current from the array. Figure 3c shows a histogram of the results, with distributions color-coded by the expected number of satisfied literals (H), showing a clear separation. It is thus possible to infer the number of satisfied literals directly from the array’s analog output signal using the threshold levels indicated by the dotted lines in Fig. 3c with an average error of ~1%. The second array can be used similarly to evaluate the make and break values. We perform the make and break value computations sequentially here, but a parallel, pipelined evaluation is possible by employing two separate crossbar arrays. We then employ the gradient computation as part of the full WalkSAT-XNF heuristic. Figure 3d shows the cumulative success rate for solving par-8-1-c problem instance. We have performed 500 repeats at a noise level of σ = 2.5, where the solver runs for a maximum of 2000 iterations per repeat. The solver consistently finds a satisfying solution within this limit and experimental results align well with ideal (i.e., variation-free and noiseless) simulations despite hardware non-idealities.

We also compare experiments and simulations by varying the noise level σ. To quantify differences in the cumulative success rate, we analyze the iterations-to-solution (ITS 99opt). In Fig. 3e, we show ITS 99opt for different noise levels and compare it against simulation-based results. Our results agree well with the experimental results, within the margin of error of the simulations. Overall, our results demonstrate that WalkSAT-XNF can be implemented using RRAM-based analog IMC hardware. The agreement between experiments and simulations highlights the robustness of the WalkSAT-XNF heuristic to hardware non-idealities, making it well-suited for implementation in custom CMOS circuits. This observation is also supported by a simulation-based sensitivity study, the results of which are presented in Supplementary Note 5. We believe this robustness to be due to the fact that the weights and the input states in our architecture are binary. The results of the crossbar array’s operations are discrete integer values, thereby providing additional robustness against noise, compared to, for example, floating point operations.

To evaluate our accelerator architecture illustrated in Fig. 2, we designed and simulated an architecture implementation using TaOx RRAM crossbar arrays realized in a 28nm CMOS process. For the simulations, we have derived latency and energy models from detailed circuit simulations and have evaluated them using activity simulations for the different SAT instances in Fig. 1. As our architecture supports both XOR and CNF clauses, we compare the CNF and XNF representations for the same problems on the same accelerator architecture to highlight the advantages for IMC accelerators of converting CNF instances to XNF instances. Figure 4a shows the average area advantage of XNF representations over CNF representations. We define the area advantage as A CNF /A XNF, where A is the number of memory cells in the crossbar arrays required for a given benchmarking instance. We find that XNF representations provide a (12.2 ± 4.7)× average area advantage for the crossbar arrays due to there being a reduced number of variables and clauses. This significantly reduces the footprint, thereby enhancing the cost-effectiveness, scalability, and energy efficiency of the accelerator. Figure 4b shows the average energy per iteration of the WalkSAT-XNF heuristic. The median energy uptake for the XNF representation is 36 pJ (interquartile range (IQR): 47 pJ) compared to 107 pJ (IQR: 119 pJ) for the CNF representation, thereby achieving a ~3× improvement in energy efficiency. Figure 4c provides a breakdown of energy consumption across hardware components for a McEliece instance. For the CNF representation with 174 variables and 623 clauses, the average energy per iteration is ~90 pJ. Here, the majority of energy is consumed by the circuits responsible for generating the Gaussian noise signal (PRNG, ~80%), while the second-largest contributor (the clause evaluation array) accounts for only ~9% of the energy uptake. The make and break computation array, the evaluation circuits, and the WTA circuit combined contribute to ~10% of the energy consumption. For the XNF representation with 32 variables and 96 clauses (13 of which are XOR clauses), energy consumption drops to ~33 pJ, that is, only a third of the CNF instance. Moreover, we find that the relative energy contributions between the two representations are notably different as approximately a third of the energy consumption of the XNF representation is dedicated to the clause evaluation circuits. The XOR clause evaluation is energetically more expensive, which accounts for 93% of the energy uptake of the evaluation circuits. Figure 4d shows a comparison of this breakdown for a 16-bit MDP instance. The XNF representation shows lower relative energy consumption by the evaluation circuits compared to Fig. 4c, due to a lower XOR-to-CNF clause ratio (7% in the MDP instance versus 23% in the McEliece instance). Overall, while an XNF representation significantly reduces energy consumption, it introduces a trade-off: problem size reduction increases the number of XOR clauses which are more energy-intensive to evaluate.

Figure 5a shows the relative advantage of the time-to-solution (TTS) for the CNF and XNF representations. Here, the TTS is attained by multiplying ITS 99opt with the latency of performing one iteration. We find that, in all instances, the TTS for the XNF instances is improved over the CNF representation with a median advantage of 3.7× (IQR: 22.2). Separated by instance classes, MDP instances show the greatest improvement (546×, IQR: 27,496.2), followed by McEliece (3.7×, IQR: 0.8) and AES (1.7×, IQR: 0.2). A further comparison between the CPU and hardware implementations of WalkSAT-XNF is provided in Supplementary Note 1, highlighting the additional speedups gained through IMC hardware acceleration.

To analyze the energy consumption of the accelerator architecture for the different problem representations, we consider the energy-to-solution (ETS). The ETS is calculated by multiplying ITS 99opt with the average energy consumed per iteration. Figure 5b shows the relative ETS advantage of the XNF representation over the CNF representation. We find that energy consumption is improved over CNF with a median of 11.4× (IQR: 65.4). Separated by instance classes, we again observe that the MDP instances benefit most (1644.1×, IQR: 83540.7), followed by McEliece (11.4×, IQR: 3.4) and AES (3.9×, IQR: 0.6).

Beyond this comparison of different problem representations for IMC hardware accelerators, we benchmark our accelerator against SAT solvers running on a CPU. For our benchmarking, the ETS and TTS were measured when running solvers on a 2.6 GHz Xeon CPU, and compared to the results for the XNF instances in Fig. 5. The TTS of the benchmarking solvers is directly derived from the CPU runtime. For the SAT solvers, we consider the SLS-solvers xnfSAT16 and WalkSAT-SKC30, alongside the conflict-driven clause learning (CDCL) solvers CryptoMiniSat22 and Kissat41. The xnfSAT and CryptoMiniSat solvers are capable of solving problems in XNF representation and are therefore evaluated with XNF instances (see Supplementary Note 2 for more details). For xnfSAT, we initially noted that performance for preprocessed XNF instances is considerably worse compared to unprocessed XNF instances. To provide the fairest comparison, we therefore decided to evaluate the performance of xnfSAT using the unprocessed XNF instances, while WalkSAT-XNF and CryptoMiniSat were evaluated using the XNF-PP instances. WalkSAT-SKC and Kissat on the other hand support only CNF clauses and were therefore evaluated using the CNF representation of the benchmarking instances.

Figure 6 presents correlation plots comparing TTS and ETS for XNF-native solvers (a) and CNF-native solvers (b) against our WalkSAT-XNF accelerator. Table 2 summarizes the median relative performance. Compared to the best-performing software solver CryptoMiniSat, WalkSAT-XNF improves the median TTS by 9.1× and the ETS by 2.3⋅10 3×. Notably, while our accelerator outperforms CryptoMiniSat for the McEliece instances, most MDP and AES problems are solved faster by CryptoMiniSat. This indicates that the structure of such problems may be more favorable to CDCL-types solvers compared to the SLS heuristic employed in WalkSAT-XNF. However, WalkSAT-XNF demonstrates a smaller ETS in most instances compared to the CDCL-types solvers. We also note that, while WalkSAT-XNF is always able to find a solution, the SLS solvers xnfSAT and WalkSAT-SKC are unable to solve a portion of the MDP instances. Moreover, xnfSAT exhibits a large variance, while WalkSAT-XNF forms distinct clusters for similar class and size instances. This clustering pattern allows for a more stable prediction of performance of similar instances and can likely be attributed to the full-neighborhood evaluation, compared to xnfSAT’s individual clause evaluation.

Methods
McEliece–Niederreiter cryptosystem. The McEliece instances are derived from cryptographic attacks25,51 on the McEliece–Niederreiter cryptosystem52,53. This cryptosystem was proposed as the first code-based public-key cryptosystem in the 1970s and has been elected by the National Institute of Standards and Technology (NIST) as a quantum-resistant public-key cryptographic algorithm for evaluating post-quantum cybersecurity54.

For the encryption and decryption of a cipher, the receiver generates three matrices: the n-by-k generator matrix G typically using Goppa codes; an n-by-n permutation matrix P; and a random k-by-k invertible matrix S. The receiver publishes a public key G 0 := SGP. The message sender prepares a plaintext message m and creates the ciphertext y=mTG 0+e, where e is an error vector with a Hamming weight of t. The receiver then uses an error-correction algorithm55 to identify the error vector e and obtains m via G, P, and S. A potential attack on the McEliece cryptosystem involves identifying the error vector e. In particular, the authors in ref. 25 interpret the problem as finding the minimum-weight codeword. Let H be an (n−k)×n matrix, with H i,j being the (i,j)-th element of the matrix H. The linear system Hc = 0 is then written over the binary field with the XOR logical operator ⊕. For instance, the i-th equality of Hc = 0 is

H i,1 c 1 ⊕ H i,2 c 2 ⊕ ... ⊕ H i,n c n = 0. (4)

A decoding attack on the system involves finding a solution c to Hc = 0 having the desired Hamming weight.

Based on this attack, the McEliece instances are generated via the PySA package56 (further details can be found in refs. 26,57). Each instance is first generated as a set of XOR equations as shown in Eq. (4). The XOR equations are then translated to CNF clauses, and the Hamming weight of the desired solution c is incorporated using additional CNF clauses. We use 10 CNF instances with a code length equal to 16. We label these instances from McE-i, where i ∈ {0,…,9}. The numbers of variables and clauses range from 171 to 183, and 611 to 659, respectively.

Minimal disagreement parity problem. The MDP instances are generated from the minimal disagreement parity problem described in ref. 38. Given an m-by-n binary matrix X, a binary vector y of length m, and an integer k, the MDP problem seeks to find a binary vector a∈{0,1} n satisfying

Σ i=1 m Σ j=1 n X i,j a j ⊕ y i ≤ k. (5)

The difficulty in solving the MDP problem has been explored in the literature, and an algorithm for solving the inequality (5), relying on XOR clauses only, was suggested in ref. 58. A total of 15 MDP instances were proposed by Crawford38 and added to the DIMACS library59, with the instances translated to a CNF representation. We selected 10 instances, par-8-i-c and par-16-i-c, i ∈ {1, …, 5}, from the DIMACS library59, and they can be accessed from ref. 57. We labeled these instances p-8-i, p-16-i, where i ∈ {1,…,5}. The numbers of variables and clauses lie in the ranges [64,74] and [254,298] for the par-8-i-c family, and [317,349] and [1264,1392] for the par-16-i-c family.

Advanced encryption standard. The Advanced Encryption Standard (AES)27,28 is a symmetric key encryption algorithm selected by the National Institute of Standards and Technology (NIST). It was developed to replace an older data encryption standard (DES) that was shown to be vulnerable to decryption attacks, particularly with the advent of stronger computational resources. Applications of AES include securing communications for online financial transactions and encrypting data in a database60. XOR operations are one of the key components of the encryption process that utilizes the so-called round keys, which are inherent to AES and finding them is indicative of a successful cryptographic attack. Instances pertaining to AES are available in the dataset from the 2012 SAT competition61, and they can be accessed from ref. 57. Solving these problem instances is viewed as a successful cryptographic attack to AES. As mentioned in ref. 61, these instances inherit XOR operations, but are translated into a CNF representation, making it possible to utilize SAT solvers that operate only CNF clauses. We use instances called aes_32_1_keyfind_i, where i=1,2 and label them AES-1 and AES-2 in the benchmarking experiment below. The numbers of variables and clauses are 300 and 1056, respectively.

We provide the details on the conversion process for generating the formulation classes CNF-PP, XNF, and XNF-PP, which illustrated in Fig. 1b. We incorporated CNF preprocessing using PySAT62, a Python library designed to work with SAT instances with CNF clauses only. We use PySAT to access the CaDiCaL solver’s preprocessor29. To produce preprocessed CNF instances (denoted by CNF-PP in the figure), the parameter named ‘rounds’ was set to 3, indicating the number of preprocessing rounds. PySAT supports a variety of preprocessing techniques, including blocked clause elimination, covered clause elimination, globally blocked clause elimination, equivalent literal substitution, bounded variable elimination, failed literal probing, hyperbinary resolution, clause subsumption, and clause vivification. Details on each technique can be found in ref. 29. All available preprocessing techniques supported by the package were employed, provided by the following parameters: block, cover, condition, decompose, elim, probe, probehbr, subsume, and vivify. The time to process a CNF instance to its preprocessed counterpart CNF-PP ranges approximately from 2 ⋅ 10−3 to 1 ⋅ 10−2s, with an average time of around 7 ⋅ 10−3s.

To convert an instance in CNF representation into XNF form, we employed the cnf2xnf tool, which is a utility present in the xnfSAT solver16. The cnf2xnf tool is designed to transform CNF instances by identifying and extracting XOR clauses from given CNF clauses. The resulting hybrid representation retains the structure of the original CNF instance while introducing XOR clauses, making the clauses more compact. The processing time to convert a CNF instance to an XNF instance ranges from ~3 ⋅ 10−3 to 3 ⋅ 10−2s, with an average time of around 4 ⋅ 10−3s. For converting a CNF instance to XNF form, the processing time ranges from 2 ⋅ 10−3 to 4 ⋅ 10−3s, with an average time of around 3 ⋅ 10−3s.

Table 3 presents the average of clause densities of each instance class, where the density is calculated by summing the number of literals in each clause and dividing by the total number of variables. We present further observations regarding the literals per clause densities d CNF and d XOR of the XNF and XNF-PP formulation classes in Supplementary Note 1.

The TTS and ETS of xnfSAT, CryptoMiniSat, WalkSAT-SKC, and Kissat were calculated using an Intel Xeon CPU running at 2.60GHz with 512GB of system memory and 128 virtual cores. For the ITS and TTS estimations, the number of trials was set to 1000 by all algorithms and instances in order to obtain a reliable success probability θ63. For CryptoMiniSat, the parameter named ‘maxsol’ was set to 1, quantifying the number of targeted solutions found by the algorithm. The maximum allowed runtime for Kissat was set to 300s. For WalkSAT-XNF, WalkSAT-SKC, and xnfSAT, each trial was capped at 10 9 maximum allowed bitflips. The noise parameters used for WalkSAT-XNF were optimized in a grid search for the different problem classes. The optimized parameters are displayed in Table 4a. The computation of the ETS for each solver is outlined in Table 4b.

To estimate the energy consumption of solvers that solely depend on software, 1.5 joules per second (i.e., 1.5 watts) was used. We benchmarked several instances using CryptoMiniSat on an AMD Epyc server while tracking the energy usage using the Powertop package64. In all cases, we observed 1.5 watts, which we used as the baseline energy usage for all CPU-based solvers. Of note, the full benchmarking experiments were performed on Intel Xeon CPUs running at 2.80GHz with 90GB of RAM and 64 logical cores on the Google Cloud Platform (GCP), on which it is not possible to measure the energy directly. We believe our estimate of 1.5 watts is conservative, as the per-core thermal design can have a higher power ceiling.

The components of the hardware architecture in Fig. 2 have been designed, validated, and modeled in a TSMC 28nm technology node. The crossbar array is modeled for a BEOL integrated RRAM device using TaOx memristors based on data from previously fabricated test chips37. The output currents at the bit lines are detected and processed using transimpedance amplifiers with active common-drain feedback. For CNF clauses, output signals are evaluated with comparators based on a StrongARM latch architecture. For the XOR clause evaluation, we model the energy consumption of the ADCs based on a regression analysis of the ADC survey data in refs. 65,66. Based on the maximum number of literals for the benchmarking problems (see Table 3), we assume an ADC bit resolution of 4 bits, which can support clauses with up to 15 literals. For an ADC with a sampling rate of 900 million samples per second and a bit resolution of 4 bits, we estimate an energy consumption per operation of 0.718 pJ and an area of 3.9 ⋅ 10−3 mm 2. The Gaussian noise signal is generated from an XORSHIFT-64 PRNG using the Alias method. The normal-distributed random number sequence generated by the PRNG is converted to analog signals using R2R ladder DACs at each bit line of the gradient evaluation crossbar ((4) in Fig. 2). The WTA circuit is realized using voltage-controlled delay lines, whose output is evaluated using merger trees and arbiters. The one-hot encoded output of the WTA circuit is fed into an array of XOR gates, whose other input is the current variable configuration stored in the register. The output is used to set the new state of the register.

The circuit is driven and synchronized by a central clock signal, where the signal provided by the register sequentially progresses through the individual circuit blocks shown in Fig. 2. A single iteration of WalkSAT-XNF is performed in three clock cycles. During the first clock cycle, the signals are applied to the first crossbar array and the output signals are analyzed using the readout circuit. During the second clock cycle, the second crossbar array is operated in the same way. During the third clock cycle, the WTA operation is performed, and the register state is updated. The combined latency of these components per iteration of WalkSAT-XNF was modeled as taking t iter = 6ns. Once the register is initialized, the entire circuit will continuously repeat this flow until a predefined number of iterations is reached or until a satisfying solution has been identified. Additional details about the circuit designs and the hardware parameters can be found in ref. 8. From these modeling results, a semi-analytical model has been derived, which evaluates the energy consumption of the individual components based on average signal levels and activity patterns. For the benchmarking, we have built a custom cycle-accurate simulator that derives instance-specific activity patterns and signal levels when running the WalkSAT-XNF heuristic. Using the semi-analytical model, we derive the mean energy consumption for each instance without the need for extensive SPICE-like simulations, which would be intractable. We derived the mean energy consumption per iteration of the WalkSAT-XNF heuristic E mean/iter for each instance and calculated the energy to solution as ETS = E mean/iter ⋅ ITS.

The experimental setup used to realize our IMC architecture comprises a custom chip fabricated in a TSMC 180nm technology node and houses three 64-by-64 memristor crossbar arrays. The 1T1M cells are based on Ta/TaOx/Pt RRAM that was monolithically integrated in-house in a BEOL process. To perform in-memory computations, the chip contains digital control and analog sensing circuits. Input signals to each array’s word line are applied digitally and the analog output is reconstructed using the ‘shift and add’ method67. To convert and measure the signals from the array’s bit lines, transimpedance amplifiers and sample-and-hold circuits are employed that rapidly convert the output currents to voltage signals and sample them. The signals are then converted to digital signals using ADCs. The chip is hosted on a custom-printed circuit board, which facilitates the voltage supply to the chip and provides a digital interface to access, control, and program the individual crossbar arrays. Additional details about the layout and the fabrication of the chip may be found in ref. 36. For the implementation of the WalkSAT-XNF heuristic, a custom Python program was written that performs the matrix operations in Fig. 2 on the crossbar arrays. Here, the matrices in Fig. 3a were programmed into two of the chip’s arrays. During the matrix operations, the binary input signals are communicated to the chip and the output signals are measured and returned via the digital interface. For the clause evaluation, the number of true literals is inferred from the output signal using equidistant quantization levels. These levels have been optimized to yield the lowest error rate.

Peer review rounds
[{"round": 1, "reviewer_comments": {"reviewer_1": "This paper proposes an in-memory computing architecture that implements and solves hybrid XOR-CNF (XNF) problems. A WalkSAT-XNF heuristic and a corresponding RRAM-based in-memory computing circuits are proposed to improve the speed and energy efficiency. The key novelty stems from providing XNF-native support through the algorithm-hardware co-design. The authors demonstrate a proof-of-concept implementation using fabricated RRAM arrays, and simulations show improved performance over CPU-based SAT solvers. However, the evaluation lacks comprehensiveness, and comparisons with state-of-the-art works are insufficiently addressed.\n- The paper does not sufficiently introduce the state-of-the-art works in XNF solvers. Without this context, it is difficult to assess the novelty of WalkSAT-XNF. The authors are encouraged to review and discuss existing XNF solvers, their performance bottlenecks, and how the proposed approach addresses these limitations.\n- The challenges of implementing the proposed architecture for XNF problems are unclear. While the concept of using in-memory computing for SAT solving is not new, the specific challenges in extending it to support hybrid XOR-CNF formulations are not clearly articulated.\n- The conversion from CNF to XNF is confusing. The authors claimed that translating XOR clauses to CNF clauses is computationally expensive, but the benchmarks in this work seem to be implemented initially in CNF clauses and require conversion to XNF. Is this procedure also costly? Besides, for an XNF problem, is it required to be converted to CNF for preprocessing and afterwards converted back to XNF? A clear explanation would be appreciated.\n- A major weakness of this work is the lack of comparison with the state-of-the-art works, making the improvement of this work less convincing. In addition to intrinsic comparison between XNF and CNF, the proposed architecture is only benchmarked with CPU implementations.\n  What is the improvement of the proposed in-memory computing architecture over existing in-memory computing works for SAT problems? Some references are listed below:\n[1] D. Kim, N. M. Rahman and S. Mukhopadhyay, \"29.1 A 32.5mW Mixed-Signal Processing-in-Memory-Based k-SAT Solver in 65nm CMOS with 74.0% Solvability for 30-Variable 126-Clause 3-SAT Problems,\" 2023 IEEE International Solid-State Circuits Conference (ISSCC), San Francisco, CA, USA, 2023, pp. 28-30.\n[2] C. Shim, J. Bae and B. Kim, \"30.3 VIP-Sat: A Boolean Satisfiability Solver Featuring 5×12 Variable In-Memory Processing Elements with 98% Solvability for 50-Variables 218-Clauses 3-SAT Problems,\" 2024 IEEE International Solid-State Circuits Conference (ISSCC), San Francisco, CA, USA, 2024, pp. 486-488.\n  What is the improvement of the proposed WalkSAT-XNF algorithm over existing CNF and XNF solvers if both implemented on CPUs?\n-The evaluation of the detailed improvement of in-memory architecture is also missing, which makes the necessity of using in-memory computing unclear. Please provide the improvement of the proposed architecture compared with implementing WalkSAT-XNF on CPUs.\n- What is the maximum problem size (in terms of variables and clauses) that the proposed RRAM crossbar arrays can support considering device non-idealities?\n- What is the solvability performance of the proposed algorithm and architecture?", "reviewer_2": "In this paper, the authors introduced a WalkSAT-XNF, a stochastic local search (SLS) heuristic designed to natively handle hybrid XOR–CNF Boolean formulas. The key idea is to extend the classical WalkSAT framework to directly evaluate both CNF and XOR clauses without requiring conversion into pure CNF form. The authors further demonstrate how this algorithm can be efficiently implemented using analog crossbar arrays based on memristive devices, leveraging their parallelism for gradient computation in variable selection. However, my major concern is that the experimental evaluation lacks sufficient comparison with modern XOR-CNF SAT solvers (aaai.v33i01.33011592)(978-3-030-53288-8_22)(s11786-024-00594-x), especially those that already support native XOR clause handling. The lack of relevant comparisons also worries me about the innovation level of the algorithm. Secondly, there is also a lack of comparison with existing IMC-based solvers (ISSCC42615.2023.10067380) in terms of hardware; only comparing with CPU-based solvers is limited.\nBelow are the suggestions:\n1. The paper primarily compares WalkSAT-XNF with traditional CNF-only solvers (e.g., Kissat, WalkSAT-SKC), which is insufficient. A meaningful comparison should include Advanced XOR-SAT solvers (aaai.v33i01.33011592 / 978-3-030-53288-8_22 / s11786-024-00594-x), specifically designed to handle CNF-XOR formulas arising from hashing-based approximate model counting. Without such comparisons, it is unclear whether the observed performance improvements are due to the IMC architecture or simply because the problems are better suited to XOR-enhanced formulations.\n2. The paper claims that WalkSAT-XNF is uniquely suitable for IMC acceleration, but does not clearly explain why other algorithms (e.g., CDCL + Gauss-Jordan elimination) cannot be adapted to similar architectures.\n3. No discussion is provided regarding why certain problem classes benefit more from one approach over another, nor is there a breakdown of structural features (e.g., XOR clause density, clause length, variable dependencies) that influence solver performance.\n4. The paper emphasizes the acceleration and energy efficiency advantages of the IMC architecture over traditional CPUs, but does not compare with other IMC-based SAT accelerators such as Snap-SAT (ISSCC42615.2023.10067380).\n5. Figure 2 of the paper illustrates the hardware module partitioning of WalkSAT-XNF, including clause evaluation, make/break computation, WTA, and other components, but provides no detailed description of its control logic or synchronization mechanisms. How do these modules coordinate with each other? Is there any control bottleneck?\n6. WalkSAT-XNF utilizes analog signals to perform parallel evaluation of make/break values, but does not quantify the precision loss of analog components such as ADCs and comparators. What is the impact of different ADC resolutions on ITS (Iterations-to-Solution)?"}, "author_response": "-> We would like to thank the reviewer for taking the time to read our manuscript and for the thoughtful questions. We appreciate the opportunity to clarify and have provided direct responses to each comment below.\n1. The paper does not sufficiently introduce the state-of-the-art works in XNF solvers. Without this context, it is difficult to assess the novelty of WalkSAT-XNF. The authors are encouraged to review and discuss existing XNF solvers, their performance bottlenecks, and how the proposed approach addresses these limitations.\n-> We thank the referee for pointing out the need to better position our work within the landscape of existing XNF solvers.\nIn the revised manuscript, we have incorporated a more detailed discussion of prior work on CryptoMiniSat and xnfSAT, which we believe represent the current state-of-the-art XNF solvers. This view is supported by recent work such as `SAT Solving Using XOR-OR-AND Normal Forms, Mathematics in Computer Science, 18, 1 (2024) by Andraschko et al.’ published last year, which identifies these two solvers as leading approaches for handling XOR+CNF instances. We used xnfSAT as a baseline for stochastic-local-search algorithm and CryptoMiniSat as a baseline solver following the CDCL-paradigm.\nWalkSAT-XNF differs significantly in methodology from the CPU-based solvers. To the best of our knowledge, there are few, if any, published works that adapt stochastic-local-search algorithms to natively handle XOR constraints using `IMC hardware’. This distinction is important, as IMC architectures impose constraints that are fundamentally different from those of CPU-based implementations.\nWe provide detailed replies within the second question below to address the novelty of our approach. We also added Section 2 in the Supplementary Information to include discussions of existing benchmarking of XNF solvers along with their performance bottlenecks; the application of CryptoMiniSat; a broader class of instances called XOR-OR-AND normal form, which can be solved using 2-Xornado and WDSat, and the challenges that arise when converting instances into a formulation suitable for CNF+XOR solvers.\n2. The challenges of implementing the proposed architecture for XNF problems are unclear. While the concept of using in-memory computing for SAT solving is not new, the specific challenges in extending it to support hybrid XOR-CNF formulations are not clearly articulated.\n-> We agree with the referee that we should do a better job highlighting the challenges and the novelty of our approach, compared to in-memory accelerators for solving SAT problems in CNF formulation. For solving XNF problems with hardware accelerators, we observe two major challenges:\n(i) Compared to CNF problems, XNF problems require considerably more complex hardware for clause evaluation. To evaluate CNF clauses, it is only necessary to check whether at least one literal is true. In our in-memory architecture, this can easily be performed with a single comparator. For XOR clause evaluation on the other hand, we need to know the number of true literals and the associated parity. In our in-memory approach, this requires the ability to obtain the Hamming distance from the crossbar array output with low error. It also requires an additional circuit that can perform the parity check using the analog output signal. It was initially not obvious whether the overhead of this more complex evaluation circuit offsets the higher algorithmic efficiency of converting SAT problems to XNF. To our knowledge, our work is the first that demonstrates an advantage for hardware accelerators in solving XNF problems instead of equivalent CNF problems, even when taking into account the additional overhead required for XOR evaluations.\n(ii) XNF problems can require support for many literals. While the original CNF versions of our benchmark problems do not have more than 3 literals per clause, the XNF problems can have up to 15 literals per clause. In hardware accelerators, we observe that implementing such dense clauses can be challenging, as high clause densities can require more circuit elements to perform the clause evaluation. For example, with a binary tree of OR gates, the number of logic gates required for clause evaluation grows linearly with the number of literals. We thus find that most hardware accelerators reported in the literature are limited to ~3 literals per clause. Our work shows that supporting a high number of literals in XNF clauses using in-memory computing is feasible and can be energy-efficient enough to show a notable advantage over SAT accelerators that implement the problems using low-density CNF clauses.\nIn response, we have modified the Introduction section:\n“Combining the advantages of a hybrid XOR--CNF formulation with IMC hardware could offer considerable advantages in tackling computationally challenging SAT problems with inherent XOR clauses. However, compared to pure CNF problems, evaluating XOR clauses requires more complex and energy-intensive circuits that can potentially offset the efficiency and latency advantages of IMC hardware. Moreover, XOR clauses can contain many literals, whereas SAT hardware accelerators can often only support few literals per clause. For IMC hardware, the high number of literals can also make it more challenging to retain low error rates during computation, as analog signals will have an increased dynamic range. It is thus still an open question whether IMC is suitable to efficiently accelerate hybrid CNF--XNF problems. Therefore, in this work we set to address the open question of whether IMC is suitable to efficiently accelerate hybrid CNF--XNF problems.”\nWe have also extended TABLE 2 in Section 4.2 to show the maximum number of literals per clause required to embed the SAT benchmark problems in CNF and XNF representation.\n3. The conversion from CNF to XNF is confusing. The authors claimed that translating XOR clauses to CNF clauses is computationally expensive, but the benchmarks in this work seem to be implemented initially in CNF clauses and require conversion to XNF. Is this procedure also costly? Besides, for an XNF problem, is it required to be converted to CNF for preprocessing and afterwards converted back to XNF? A clear explanation would be appreciated.\n-> We thank the referee for highlighting the need to improve this section in the manuscript.\nDirect encoding of XOR clauses into CNF clauses is costly, particularly when the XOR clauses contain many literals, as it leads to an exponential number of CNF clauses. This exponential blow-up is illustrated in equation (2) of the manuscript. This is one of the key motivations behind using a native representation for the XOR constraints. We argue that solving an instance in its CNF form typically requires more computational resources, as it introduces more variables and clauses compared to its XNF counterpart. This observation is illustrated in FIG. 5 in Section 2.5 and FIG. 1 in the Supplementary materials.\nIn our experiments, all benchmark instances were originally sourced in the pure CNF formulation, as stated in the sentence “All instances inherit native XOR clauses but are initially provided with CNF clauses only.” in the manuscript. Our goal is to demonstrate that when these instances are reformulated as XOR+CNF, the resulting formulation is not only more compact but also more amenable for efficient solving by XOR-aware SAT solvers. The conversion from CNF to XOR+CNF is not observed to be computationally costly. As reported in Section 4.2 of the manuscript, the conversion time typically ranges from O(1e-3) to O(1e-2) seconds per instance.\nWe have added “Details of the preprocessing procedure and the per-instance preprocessing runtime are reported in Section 4.” Section 2.1 of the manuscript to direct readers where details can be found regarding the preprocessing steps.\n4. A major weakness of this work is the lack of comparison with the state-of-the-art works, making the improvement of this work less convincing. In addition to intrinsic comparison between XNF and CNF, the proposed architecture is only benchmarked with CPU implementations.\n* What is the improvement of the proposed in-memory computing architecture over existing in-memory computing works for SAT problems? Some references are listed below:\n[1] D. Kim, N. M. Rahman and S. Mukhopadhyay, \"29.1 A 32.5mW Mixed-Signal Processing-in-Memory-Based k-SAT Solver in 65nm CMOS with 74.0% Solvability for 30-Variable 126-Clause 3-SAT Problems,\" 2023 IEEE International Solid-State Circuits Conference (ISSCC), San Francisco, CA, USA, 2023, pp. 28-30.\n[2] C. Shim, J. Bae and B. Kim, \"30.3 VIP-Sat: A Boolean Satisfiability Solver Featuring 5×12 Variable In-Memory Processing Elements with 98% Solvability for 50-Variables 218-Clauses 3-SAT Problems,\" 2024 IEEE International Solid-State Circuits Conference (ISSCC), San Francisco, CA, USA, 2024, pp. 486-488.\n-> We agree with the referees that additional comparisons against other state-of-the-art SAT hardware accelerators are helpful to better understand the advantages of the system proposed in this work. We have added the comparison below to the Supplementary materials which include the references proposed by referees 1 and 2.\nAs we do not have access to the actual hardware, we are considering the common instances reported in literature, which are random 3-SAT problems with 20 and 50 variables. For these instances, we compare the performance of other accelerator systems to an SRAM-based experimental realization of our in-memory computing architecture reported in [11], as well as simulations of our RRAM architecture, which were previously reported in [10]. For the simulations of our RRAM architecture, we find that it is outperforming other accelerator systems. We want to stress that the advantages of the RRAM system partly arise due to the fact that we compare experimental systems to computer simulations, which can be more optimistic due to the lack of leakage power and other parasitic effects. Moreover, our architecture is using a different memory technology (RRAM) and a smaller technology node (28nm), both of which can result in faster operating speeds and lower energy consumption. For that reason, we believe that our experimental system reported in [8] is a fairer base of comparison. Here, we have reported either on-par or considerably better than other state-of-the-art systems.\nWhile we cannot test our benchmark problems on any of these hardware systems, we want to point out that all systems, except for Snap-SAT and our own architecture, can only support up to 3 literals per clause. This is insufficient to implement the considerably denser pre-processed SAT instances with up to 7 literals per clause. These accelerator systems would thus only be able to implement the sparser un-pre-processed instances and thereby suffer from the same performance penalties that we have observed in our detailed intrinsic comparison (around 30x more iterations and energy to find a solution). In addition, as none of the state-of-the-art systems can support XNF clauses, we expect that the advantages we observe from translating problems from CNF to XNF in our intrinsic comparison (around 4x fewer iterations and 11x less energy) would also exist compared to the SOTA systems in supplementary table 3.\nConsidering the data in the table above and the results of our intrinsic comparison, we are therefore confident that our proposed XNF accelerator architecture can attain a performance advantage over existing IMC accelerators reported in the literature.\nIn response, we have modified parts of the discussion section:\n“For SAT problems that can be natively expressed as hybrid XOR--CNF problems, we find that this can reduce the chip area and energy consumption, while also improving the computation speed compared to mapping them to a pure CNF representation. This presents an advantage over existing SAT hardware accelerators, which can only solve problems in pure CNF formulation. When tackling pure CNF problems, the IMC architecture in FIG. 2 has previously demonstrated that it can outperform comparable SAT accelerators (see Supplementary materials). As shown in our intrinsic comparison in FIG. 4, the ability to implement XOR clauses can provide an additional order-of-magnitude improvement in computation speed and energy efficiency.\nMoreover, the crossbar array embedding depicted in FIG. 2 can, in principle, support dense XOR and CNF clauses with as many literals as there are variables. Our experimental proof of concept successfully demonstrates this for a hybrid XOR--CNF problem with up to five literals per clause, which can be extended to even more complex clauses. This allows our architecture to additionally leverage the advantages of SAT pre-processing techniques, which tend to trade increased algorithmic efficiency with a higher density of literals per clause (see TABLE 2 in Section 4.2). By combining these advantages, we find that our proposed accelerator can outperform state-of-the-art SAT solvers running on digital computers in terms of computation speed and energy consumption.”\nWe have also added the above comparison to Section 4 in the Supplementary materials.\n* What is the improvement of the proposed WalkSAT-XNF algorithm over existing CNF and XNF solvers if both implemented on CPUs?\nWe thank the referee for the question. We would like to highlight that the key measures of improvement are the median TTS and ETS metrics reported in TABLE 1 in the manuscript, where the TTS used for WalkSAT-XNF is based on the hardware-level estimate, which is the product of ITS and time per iteration, where we assume a latency of 6 nanoseconds for our hardware. Here, we present the TTS estimated from the CPU runtime of WalkSAT-XNF; the ETS estimates are shown in FIG.6 in the manuscript.\nThe average ITS and TTS comparisons for the instances in the XNF-PP class, based on measurable metrics, are as follows.\nXNF-PP WalkSAT-XNF xnfSAT ITS improvement (xnfSAT/\nITS average WalkSAT-XNF)\nMcEliece 77,304 5,627,260,452 72,794\nMDP 51,730,543 164,732,553 3\nAES 22,943,569 522,249,283 23\nXNF-PP WalkSAT-XNF WalkSAT-XNF xnfSAT CryptoMiniSat\nTTS average (IMC) (CPU) (CPU) (CPU)\nMcEliece 0.0005 0.034 1354.026 0.005\nMDP 0.3104 84.983 13.442 0.008\nAES 0.1377 26.193 66.867 0.017\nThe ITS and TTS comparisons among the CNF solvers are as follows.\nCNF-PP WalkSAT-XNF WalkSAT-SKC ITS improvement (WalkSAT-\nITS average SKC/ WalkSAT-XNF)\nMcEliece 292,611 519,921 1.8\nMDP 47,131,444,460 735,008,980,813 15.6\nAES 36,293,586 808,645,266 22.3\nCNF-PP WalkSAT-XNF WalkSAT-XNF WalkSAT-SKC Kissat\nTTS average (IMC) (CPU) (CPU) (CPU)\nMcEliece 0.0018 0.148 0.074 0.008\nMDP 282.7887 352,646.54 382,688.82 0.038\nAES 0.2178 28.1 165.898 0.027\nAs shown in the tables above, the TTS performance of the CPU-based WalkSAT-XNF lies between that of SLS solvers and CDCL solvers, with CDCL-based solvers (CryptoMiniSat, Kissat) often demonstrating better performance. We would like to highlight that our key argument is not based on TTS metric based on CPU implementation, but more importantly, on energy efficiency, as measured by ITS combined with the energy consumed per iteration, that is reported in Fig.6 and TABLE 1 in the manuscript.\n5. The evaluation of the detailed improvement of in-memory architecture is also missing, which makes the necessity of using in-memory computing unclear. Please provide the improvement of the proposed architecture compared with implementing WalkSAT-XNF on CPUs.\n-> We thank the referee for raising this point. The table below reports the average TTS grouped by instance class and formulation class, along with their improvements measured on the CNF and XNF representations. The TTS metric (TTS(CPU)) is measured from a CPU-based implementation written in the Rust programming language. The TTS metric (TTS(IMC)) is measured by iterations-to-solution multiplied by a latency of 6 nanoseconds. As reported in the Speedup columns, TTS measured by IMC hardware demonstrates orders-of-magnitude improvement. We believe that reporting the following would help strengthen the necessity of introducing IMC hardware.\nCNF XNF\nInstance class TTS (CPU) TTS (IMC) Speedup TTS (CPU) TTS (IMC) Speedup\nMcEliece 0.15 0.0018 84 0.03 0.0005 73\nMDP 352,646.54 282.7887 1247 84.98 0.3104 274\nAES 28.10 0.2178 129 26.19 0.1377 190\nThe table above is included as Table 2 in the Supplementary Material.\n6. What is the maximum problem size (in terms of variables and clauses) that the proposed RRAM crossbar arrays can support considering device non-idealities?\nWe thank the referee for raising an important point and agree that it would help to be more specific in the manuscript about the dimensions and scalability of RRAM crossbar arrays.\nIndividual RRAM arrays demonstrated in the literature [e.g., An analog-AI chip for energy-efficient speech recognition and transcription | Nature] can potentially support up to 256 variables and 512 clauses. However, crossbar arrays can also support problems larger than this by utilizing tiling architectures, where problems are split across different arrays. State-of-the-art systems have demonstrated this for large-scale problems using up to 140 million RRAM memory cells. We have also recently proposed an architecture that can exploit the sparsity of SAT problems to map problems with up to 1000 variables onto a single chip with an area of ~50mm².\nIn order to address this comment, we have changed parts of our previous Discussion section, where the scalability of SAT hardware accelerators is discussed:\n“Another challenge relates to the scalability of the IMC hardware. Crossbar arrays are realistically limited in size by parasitic effects and signal drop-off to a few hundred rows and columns. Using our architecture, current IMC hardware could support SAT problems with up to ~250 variables and ~500 clauses within a single array.”\n7. What is the solvability performance of the proposed algorithm and architecture?\n-> We thank the referee for the question. The architecture maintains a 1-to-1 correspondence with the proposed algorithm, and the average solvability of the proposed algorithm (which therefore also reflects the architecture) is summarized in Supplementary table S.1; solvability for all benchmark instances containing both CNF and XOR is 100%, i.e., all problems were solved at every repeat.\nTo evaluate hardware-based solvability, we tested three representative instances, as shown in the table below.\nThe instance par8-1 (XNF-PP), detailed in Section 4.2 of the manuscript, is included among them.\nnumber of number of number of number of max number of\nvariables CNF clauses XOR clauses repeats iterations\npar8-1 (XNF-PP) 13 41 1 500 2000\npar8-2 (XNF) 31 30 23 50 3000\npar8-3 (XNF 31 30 23 50 3000\nEach instance was solved successfully in every repeated attempt, yielding a solvability rate of 100%; the first instance par8-1 was solved 500 out of 500 runs, and other two instances were solved 50 out of 50 runs. This result indicates reliable solvability performance across both the architecture and the hardware experiment, and we are confident that using in-memory computing hardware for solving XOR+CNF problems is feasible.\nReviewer #2 (Remarks to the Author):\nIn this paper, the authors introduced a WalkSAT-XNF, a stochastic local search (SLS) heuristic designed to natively handle hybrid XOR–CNF Boolean formulas. The key idea is to extend the classical WalkSAT framework to directly evaluate both CNF and XOR clauses without requiring conversion into pure CNF form. The authors further demonstrate how this algorithm can be efficiently implemented using analog crossbar arrays based on memristive devices, leveraging their parallelism for gradient computation in variable selection. However, my major concern is that the experimental evaluation lacks sufficient comparison with modern XOR-CNF SAT solvers (aaai.v33i01.33011592)(978-3-030-53288-8_22)(s11786-024-00594-x), especially those that already support native XOR clause handling. The lack of relevant comparisons also worries me about the innovation level of the algorithm. Secondly, there is also a lack of comparison with existing IMC-based solvers (ISSCC42615.2023.10067380) in terms of hardware; only comparing with CPU-based solvers is limited.\n-> We appreciate the reviewer’s careful assessment and thoughtful feedback. Below, we respond to each comment with clarifications and additional detail.\nBelow are the suggestions:\n1. The paper primarily compares WalkSAT-XNF with traditional CNF-only solvers (e.g., Kissat, WalkSAT-SKC), which is insufficient. A meaningful comparison should include Advanced XOR-SAT solvers (aaai.v33i01.33011592 / 978-3-030-53288-8_22 / s11786-024-00594-x), specifically designed to handle CNF-XOR formulas arising from hashing-based approximate model counting. Without such comparisons, it is unclear whether the observed performance improvements are due to the IMC architecture or simply because the problems are better suited to XOR-enhanced formulations.\n-> We thank the referee for the suggestion to compare WalkSAT-XNF against advanced XOR-SAT solvers. We agree that comparing our results within the context of recent work on CNF+XOR solving is important to properly assess the contribution of our approach.\nThe two referenced papers (aaai.v33i01.33011592 / 978-3-030-53288-8_22) focus on improving the efficiency of hashing-based algorithms for model counting. They build on the BIRD (with the second paper introducing BIRD2) architecture to efficiently inject XOR-constraints during the BLAST step that arises from the cell-forming routine in approximate model counting. The related architecture has now evolved to ApproxMC6 (https://github.com/meelgroup/approxmc). They both rely heavily on an XOR-aware CDCL solver, CryptoMiniSat, once the XOR+CNF formulation is reconstructed after in-processing. Our solver, WalkSAT-XNF, which operates in a stochastic local search regime, is able to natively operate on XOR constraints, without requiring reformulating the problems into purely CNF-based instances. We have benchmarked against CryptoMiniSat in our evaluation, as it serves as a strong representative of the XOR-aware CDCL solver class. We believe that comparing WalkSAT-XNF with CryptoMiniSat constitutes a fair comparison, as it constitutes the backend for the 3 referenced approximate model counting solvers.\nThe third work referenced (s11786-024-00594-x) explores a DPLL-style algorithm tailored for 2-XNF (XOR-OR-AND normal form), where each clause is a disjunction of at most two literals. This is an interesting theoretical direction that differs from our approach both in scope and solver architecture.\nWe attempted to translate XOR+CNF formulae into 2- XOR-OR-AND normal form in order to benchmark the instances used in our paper by using the solver introduced in `s11786-024-00594-x’. The translation proceeded as follows: a k-literal CNF clause is reduced to (k-2) 3-literal clauses with k-3 auxiliary variables. Each 3-literal clause is then converted to three 2-literal clauses with the addition of auxiliary variables. However, this transformation does not guarantee satisfiability of the resulting 2-literal clauses, since there is no known satisfiability-preserving reduction. Despite this limitation, we adopt the following conversion of the type (𝑥 ∨𝑦 ∨𝑧) → (𝑥 ∨𝑎)∧(𝑦∨−𝑎)∧(𝑧∨−𝑎), with 𝑎 being an auxiliary variable introduced. The XOR clauses do not require any conversions and hence are omitted from the plot. We have observed that this conversion is not suitable for certain problem families, such as the McEliece class, which admit a unique solution. We believe that this uniqueness poses a problem in the converted form. For instance, if (x,y,z)=(0,1,0) is the unique solution to the instance, the 2-literal clauses are unsatisfiable. In fact, we observed that all McEliece instances reduced to contain 2-literal CNF clauses become unsatisfiable.\nIn the reverse direction, we attempted to translate existing 2-XOR-OR-AND normal form instances accessible from the link https://github.com/j-danner/2-Xornado/tree/main/tests/2xnfs into XOR+CNF formulae. This collection of instances is translated into a set of CNF+XOR instances suggested by Remark 5.1 in (s11786-024-00594-x), and the resulting statistic is reported in the plot below.\nHere, we observe a significant increase in the size of the instances, with the total number of clauses often doubling the number obtained in the XOR+CNF formulation. In our case, the solver is deployed on specialized in-memory computing hardware, where the number of clauses are constrained by the physical capacity of the system. Reducing high-order CNF clauses to quadratic form significantly increases problem size, potentially beyond the hardware capacity. To clarify these limitations, we have added the following explanation in the Discussion section of the revised manuscript:\n“Another challenge relates to the scalability of the IMC hardware. Crossbar arrays are realistically limited in size by parasitic effects and signal drop-off to a few hundred rows and columns. Using our architecture, current IMC hardware could support SAT problems with up to ~250 variables and ~500 clauses within a single array.”\nFurthermore, our hardware can support clauses with multiple literals, applying this transformation undermines its architectural advantages. To reinforce this point, we have strengthened TABLE 2 in Section 4.2 to show the clause degrees that our hardware can support.\nWe revised Section 2 of the Supplementary material to include discussions of these related works and clarify the distinctions in methodology and applicability. We also highlighted that the observed performance improvements stem from both the IMC-inspired architecture and the SLS-based approach CNF+XOR solving using the TTS metric, based both on the IMC and CPU implementations (Section 1 of the Supplementary material).\n2. The paper claims that WalkSAT-XNF is uniquely suitable for IMC acceleration, but does not clearly explain why other algorithms (e.g., CDCL + Gauss-Jordan elimination) cannot be adapted to similar architectures.\n-> We thank the referee for the question; we think this is an important point to clarify. There appears to be a misunderstanding. We do not want to claim that WalkSAT-XNF is uniquely suitable for IMC acceleration. While the design of dedicated CDCL or GJE accelerators would be a large undertaking and thus outside the scope of this work, we agree with the referee that there is a large potential for these algorithms to be accelerated by IMC. In the Discussion section of our manuscript, we had thus previously mentioned CDCL and GJE as promising algorithms that should be investigated in the future. Given the remark by the referee, we feel that it is important to better stress that WalkSAT-XNF is not uniquely suitable for IMC and we see potential in exploiting IMC for other types of algorithms.\nIn response, we have changed the last paragraph of the Discussion section:\n“The WalkSAT-XNF heuristic is an evolution of the CNF-specific WalkSAT heuristic and does not differentiate between XOR and CNF clauses for the purposes of variable selection. Based on the insights from this work, it could be possible to use IMC hardware for accelerating algorithmically efficient heuristics that include more sophisticated clause differentiation (e.g., by pre-solving the XOR clauses using Gauss--Jordan elimination).”\n3. No discussion is provided regarding why certain problem classes benefit more from one approach over another, nor is there a breakdown of structural features (e.g., XOR clause density, clause length, variable dependencies) that influence solver performance.\n-> We thank the referee for raising the question; we agree that including such discussions may help strengthen the manuscript. We aim to compare our observations with the work ‘The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas (Dudek et al., IJCAI-17, 2017, pp. 600–606) as a baseline. This work provides empirical findings on the performance of CryptoMiniSat using random XOR+CNF formulae, particularly focusing on the structural properties of XOR clauses. We use instance size, XOR clause degree, and clause-variable interdependency as metrics to gauge solver performance, and analyze the consistency of our findings with those reported by Dudek et al.\nFirst, we observe how instance size impacts solver performance. Regardless of the problem classes, the instance sizes are the most dominant factor of the energy efficiency of our solver. The relationship between energy-per-iteration and instance size is evident in the top row of the plot below. In addition, there is a strong positive relation between instance size and ITS (and therefore ETS), as shown in the bottom row of the figure below.\nSecondly, we observe a positive relation between the degree of XOR clauses to ITS, shown in the plot below. Specifically, higher XOR clause degrees tend to increase problem hardness, leading to larger ITS values. This observation aligns with empirical findings by Dudek et al,. However, it is important to note that this is not an entirely direct comparison, as our benchmarks are based on structured problem instances, whereas the results in the work by Dudek, et al.’s work are based on random problem instances under controlled settings. Additionally, we observe that the XOR clause degrees of the XNF-PP class instances tend to be greater than those of the XNF class instances. The increase in degree with respect to CNF clauses is also observed with preprocessing, yet, the degree of CNF clauses appears to have a weaker correlation with ITS.\nFinally, variable dependency--measured by the average frequency of clauses where each variable appears in--is negatively correlated with ITS. Although the correlation signal is weaker than other cases, a generally decreasing trend is still observed. We believe the trend shown in the plot below does not significantly violate the findings made in the aforementioned work by Dudek, et al. particularly when the XOR variable-probability is less than 0.2. In this region, the hardness and variable-XOR interdependency exhibits a concave pattern.\nWe have revised the manuscript to include the observations related to the instance size and clause degrees in Section 1 of the Supplementary material. The discussion regarding the variable-clause interdependency is not included, since the variable-XOR clause interdependency in our benchmark set does not span beyond 0.2, rendering the comparison inconclusive.\n4. The paper emphasizes the acceleration and energy efficiency advantages of the IMC architecture over traditional CPUs, but does not compare with other IMC-based SAT accelerators such as Snap-SAT (ISSCC42615.2023.10067380).\n-> We agree with the referee that a comparison to other SAT hardware accelerators is needed to better highlight the benefits of our proposed accelerator architecture. We would like to point the referee to our answer to a similar question by referee #1, where we describe the results of a comparison of our system against other state-of-the-art SAT hardware accelerators. We have also included Snap-SAT in the comparison, as suggested by the referee.\n5. Figure 2 of the paper illustrates the hardware module partitioning of WalkSAT-XNF, including clause evaluation, make/break computation, WTA, and other components, but provides no detailed description of its control logic or synchronization mechanisms. How do these modules coordinate with each other? Is there any control bottleneck?\n->We agree with the referee that a more detailed description of the operation of our architecture would be helpful, e.g., in identifying potential bottlenecks. We have added additional details to the Methods section to better describe the dataflow and operation during a single iteration. The entire system is driven by a central clock signal, where the signal is distributed to the different circuit elements by a clock tree to achieve synchronization. A full iteration takes three clock cycles in total. During the first clock cycle, the signals are applied to the first crossbar array and the output signals are analyzed using the readout circuit. During the second clock cycle, the second crossbar array is operated in the same way. During the third clock cycle, the WTA operation is performed, and the register state is updated. Once the register has been set with an initial variable configuration, the circuit will continuously repeat this flow, until the register is read out again. With this continuous autonomous operation, there is no need for complex control logic. We cannot identify a significant control bottleneck.\nIn response, we have extended the Methods section, where we describe the modeling of the hardware:\n“The circuit is driven and synchronized by a central clock signal, where the signal sequentially progresses through the individual circuit blocks shown in Fig.2. A single iteration of WalkSAT-XNF is performed in three clock cycles. During the first clock cycle, the signals are applied to the first crossbar array and the output signals are analyzed using the readout circuit. During the second clock cycle, the second crossbar array is operated in the same way. During the third clock cycle, the WTA operation is performed, and the register state is updated. The combined latency of these components per iteration of WalkSAT-XNF was modelled as taking $t_{\\rm iter} = 6 \\,$ns. Once the register is initialized, the entire circuit will continuously repeat this flow until a predefined number of iterations is reached or until a satisfying solution has been identified.”\n6. WalkSAT-XNF utilizes analog signals to perform parallel evaluation of make/break values, but does not quantify the precision loss of analog components such as ADCs and comparators. What is the impact of different ADC resolutions on ITS (Iterations-to-Solution)?\n->We thank the referee for raising an important point. In general, our hardware simulations discretize the analog output signal coming from the crossbar array to mimic the operation of an ADC or a comparator as shown in Fig.3 (i.e., each ADC level is associated with a specific number of true literals computed by the crossbar array). The simulations therefore already include the effects of signal discretization. Within all simulations, we have chosen an ADC resolution of 4 bits, which corresponds to 16 discrete levels. Given that the maximal number of literals per XOR clause for our benchmark problems is 15, this resolution is sufficiently high to evaluate XOR clauses even under the worst-case scenario, i.e., when all literals are true. We therefore do not expect that the current ADC resolution will have an adverse effect on the performance. That said, we see optimization potential in reducing the ADC resolution. We have analyzed the simulated output signals from the first crossbar for XOR clauses for two exemplary MDP problems in the figure below. We find that the average number of true literals for XOR clauses is considerably below the maximum number of literals. The distribution also shows that it is unlikely to encounter the case where all literals are true. This would allow us to reduce the resolution of the ADC, which would improve the overall energy efficiency of the accelerator. We have tested the effect of reducing the bit resolution on the cumulative success rate by reducing the number of ADC levels. Depending on the instance, we find that the success rate is not significantly affected by as few as 4-5 ADC levels. For a lower number of ADC levels, we see that the success rate will diminish. Notably, for par8-2, we see that even a 2-level ADC (effectively a comparator) is still able to solve the example problem, albeit in a considerable number of trials.\nIn response, we have added an additional remark to the Discussion section:\n“As we show in the Supplementary materials, additional energy savings can also be achieved by reducing the resolution of the ADC.”\nWe have also added a remark to the Methods section, where we explain the choice of the bit resolution for the ADCs:\n“Based on the maximum number of literals for the benchmarks problems (see Table 2) we assume an ADC bit resolution of 4 bits, which can support clauses with up to 15 literals.”\nFinally, we have added a new section (Section 4) to the Supplementary materials, where we discuss the data shown above."}, {"round": 2, "reviewer_comments": {"reviewer_1": "The authors have addressed most of my questions, but a few concerns remain not well resolved.\n- The maximum problem size that the proposed analog CiM array can support is limited primarily by the variations and on/off ratios of RRAMs as well as the non-idealities of the ADCs, instead of by the RRAM array size. Therefore, the claim of supporting up to 250 variables and 500 clauses is not convincingly substantiated.\n- The comparisons with the state-of-the-art CiM-based SAT accelerators are not apple-to-apple. In Supplementary Table 3, as the authors have mentioned, the proposed work uses a more advanced technology node, and thus the results are not directly comparable. The source of the improvement on pure CNF problems against other baselines is also unclear. Besides, the authors claimed “our experimental system reported in [8] is a fairer base of comparison”, yet [8] is not compared. The use of [10] to cite the proposed work within the table is also very confusing.", "reviewer_2": "The authors have provided detailed responses to the initial reviews and have made substantial revisions to the manuscript.\nHowever, several points still require clarification or further analysis to strengthen the paper:\n1.Since CDCL+GJE could also be accelerated via IMC, please elaborate on why WalkSAT-XNF was chosen as the first target instead of other algorithms. Give a brief discussion of the relative feasibility and potential performance of IMC-accelerated CDCL+GJE.\n2.The comparison table shows that other accelerators do not natively support XNF. However, is it not possible to pre-process the XNF problems into a low-literal CNF formulation to run on these accelerators? If so, what would be the expected performance penalty, and how would it affect the overall advantage claimed for your architecture?\n3.For larger crossbar arrays, could the clock tree distribution and signal skew become a challenge for synchronization? Has this been analyzed or simulated?\n4.The simulation results are promising, but the reliance on idealistic models (28nm, no leakage) may overstate the advantages. Please provide a sensitivity analysis of key non-idealities (e.g., conductance variations, ADC noise) on the solver’s success rate and energy efficiency."}, "author_response": "REVIEWER COMMENTS\nReviewer #1 (Remarks to the Author):\n“The authors have addressed most of my questions, but a few concerns remain not well\nresolved.”\n“The maximum problem size that the proposed analog CiM array can support is limited\nprimarily by the variations and on/off ratios of RRAMs as well as the non-idealities of\nthe ADCs, instead of by the RRAM array size. Therefore, the claim of supporting up to\n250 variables and 500 clauses is not convincingly substantiated.”\nWe agree with the reviewer that we should clarify the feasibility of using large-scale in-memory computing systems in our architecture. As the reviewer correctly remarks, scaling of our architecture requires that we can perform large-scale matrix-vector multiplications (MVMs) using analog compute in memory (CiM) arrays. CiM-based SAT accelerators, such as the ones in [11,14], have demonstrated successful operation using arrays as large as 128 by 1024. Sensitivity studies of device non-idealities in RRAM-based CiM hardware have shown the feasibility of solving SAT problems with up to 200 variables and 860 clauses [36].\nCiM arrays based on emerging memories (such as RRAM or phase change materials) for performing MVM operations have also been reported in the literature for array sizes of up to 2048 by 512 [46] for AI inference, where the layer-to-layer connections are represented by dense matrices, i.e., a very high on/off ratio for the memory cells. Such systems achieve large-scale dense matrix-vector operations, despite programming variations of individual memory cells or non-idealities in the sensing circuits, e.g., in the ADCs. It must be noted that, compared to AI inference tasks, the requirements of our architecture for the CiM array are considerably more relaxed. Contrary to the dense MVM operations in AI workloads, our architecture maps SAT problems to matrices that are relatively sparse. As shown in Table 2, the average on/off ratio for each individual array row does not exceed 20%. Moreover, compared to AI workloads, our architecture does not require multi-bit precision for the input data or the memory cells. The requirements on memory cell variations and the dynamic range of the sensing circuits are thus considerably more lenient. We are therefore confident that large-scale state-of-the-art CiM systems, such as the ones reported in [46], can also be used in our architecture. This is also supported by a sensitivity analysis that we have added to the Supplementary Information.\nIn response to the reviewer’s comment, we have modified the discussions section to incorporate the reviewer’s remarks related to non-idealities and dense matrices:\n“One challenge in realizing performance enhancements for industrial applications pertains\nto the scalability of IMC hardware. Crossbar arrays are limited in size, for example, by\nparasitic effects, signal drop-off, and non-idealities, to a few hundred rows and columns.\nCurrent IMC hardware capable of dense matrix--vector operations could support the\ncomputations in our architecture for SAT problems with up to ~250 variables and ~500\nclauses within a single array [46].”\nWe have also added additional details to section 2.4, where we discuss the dominant types of non-idealities in CiM hardware:”\n“As with other mixed-signal computing systems, realizing WalkSAT-XNF in hardware\nrequires it to be sufficiently resilient against hardware non-idealities in the analog circuits.\nStudies have identified variations in the RRAM cells and noise in the crossbar array's analog\nreadout circuit as the dominant non-idealities that can result in a deterioration in\nperformance [36].”\nWe have also added a new section 5 to the Supplementary Information, where we discuss and evaluate the sensitivity of our proposed architecture to hardware non-idealities,\nincluding RRAM variations and ADC noise.\n“The comparisons with the state-of-the-art CiM-based SAT accelerators are not apple-to-apple. In Supplementary Table 3, as the authors have mentioned, the proposed work uses a more advanced technology node, and thus the results are not directly comparable. The source of the improvement on pure CNF problems against other baselines is also unclear. Besides, the authors claimed “our experimental system reported in [8] is a fairer base of comparison”, yet [8] is not compared. The use of [10] to cite the proposed work within the table is also very confusing.”\nWe thank the reviewer for raising this point. Clearly, we have not done a good enough job in explaining the comparison in Tab.S3, and we agree that we should clarify this further. As correctly noted by the reviewer, the SAT accelerators cited in Tab.S3 are experimental proof-of-concept systems, whereas our simulations aim to predict performance attainable by a hardware accelerator. Compared to our simulations, experimental proof-of-concept systems sacrifice some of their performance, e.g., by using larger technology nodes and potentially less energy-efficient but more readily available memory technology. Moreover, these chips are typically operated in testing environments, which can produce additional power losses, e.g., due to test circuit boards or external signal sources. In the comparison in Tab.S3, we have therefore included both simulations (based on the work reported in [8]) and a proof-of-concept system [14] for a CNF-only SAT solver using our IMC approach.\nComparing [8] and [14] shows that an optimized CiM SAT accelerator can potentially improve compute speed and energy efficiency by a factor of 5x and 10x, respectively, over the proof-of-concept system. When comparing [14] to the other hardware systems, we can also gain insights into how our CiM approach compares to other state-of-the-art systems.\n[12] is a system that is very similar in capability to [14], as it can solve k-SAT problems with arbitrary numbers of literals per clause using a WalkSAT-like heuristic. We find that our approach is ~15x faster and ~2x more energy efficient. Compared to [10] and [11], we find that [14] is up to 2.4x slower and up to 25x less energy efficient for 3SAT problems. It is important to note that [10,11] have been specifically optimized for solving 3SAT problems, i.e., problems with only 3 literals per clause. Because of this, whereas [12,14] could solve our benchmark problems using the more efficient pre-processed representation (‘CNF-PP’ in Fig.S1), [12] and [14] would have to use the non-pre-processed problem representation (‘CNF’ in Fig.S1). As our data in Fig.S1 shows, these problems are larger in size and more complex to solve with SLS solvers, which results in a ~30x increase in computation time and energy consumption. For our benchmark problems, the benefits of the more energy efficient 3SAT solvers in [10,11] would thus be offset by the overhead of mapping to 3SAT. From the comparison in Tab.S3, we therefore estimate that our CiM approach is either better, or on-par compared to other state-of-the-art SAT accelerators for our benchmark problems in CNF.\nGiven the reviewer’s comment, we have decided to rewrite large parts of section 3 in the supplementary materials using our explanation above.\nReviewer #2 (Remarks to the Author):\n“The authors have provided detailed responses to the initial reviews and have made\nsubstantial revisions to the manuscript. However, several points still require\nclarification or further analysis to strengthen the paper:”\n“1. Since CDCL+GJE could also be accelerated via IMC, please elaborate on why\nWalkSAT-XNF was chosen as the first target instead of other algorithms. Give a brief\ndiscussion of the relative feasibility and potential performance of IMC-accelerated\nCDCL+GJE.”\nWe thank the reviewer for the suggestion and gladly provide further clarification.\nWalkSAT-XNF was designed because its WalkSAT-type algorithm provides a natural embedding of the problem in a matrix representation, which can be directly utilized for gradient computation and for evaluating clauses with IMC hardware. Moreover, WalkSAT-XNF’s relatively low computational complexity enables us to translate all its computational steps directly into analog circuits, which can perform all the computations during an iteration within just three clock cycles. The continuous and autonomous operation of this circuit avoids the need for complex control circuits, and the time and energy overhead of frequent memory access or communication with a co-processor, resulting in fast and efficient computation. Moreover, the entire problem can be embedded into the crossbar array without requiring frequent reprogramming of the memory cells. Given the reviewer’s comment, we have added the following to section 2.3 to better explain our choice:\n“Crucially, the relative simplicity of WalkSAT-XNF enables us to map every computational step to an equivalent analog circuit, enabling rapid continuous computation. As with other IMC concepts [8,34], the crossbar arrays in Fig.2 enable parallel gradient computations for both the CNF and XOR clauses within a single clock cycle. Performing an entire operation of WalkSAT-XNF is achieved within just three clock cycles, without the need for a complex control system, while also circumventing frequent time-intensive communication with external co-processors or memory systems. Both XOR and CNF clauses can be evaluated using the same array, allowing for an area-efficient design. Moreover, the crossbar array can implement a number of literals per clause that is equal to the number of variables, hence supporting highly complex clauses common in industry workloads.”\nRegarding the comparison to CDCL+GJE, it appears as if our previous reply has created the impression that it is easy to accelerate these methods with IMC hardware. We want to clarify that there is currently no architecture reported in the literature that can implement CDCL solvers with native XNF support using IMC hardware. We believe that this is due to CDCL algorithms being more complex compared to WalkSAT-like algorithms, which creates some yet unsolved design challenges. For example, it is unclear whether the computational steps can be mapped to a continuously operating analog circuit that could provide rapid computation as with WalkSAT-XNF. Moreover, it is unclear whether such a CDCL IMC accelerator would avoid frequent time-intensive communication with co-processors and memory systems and whether it would circumvent the need for frequent reprogramming of the IMC hardware. A performance comparison with WalkSAT-XNF would thus require us to first conceive, design, model, and benchmark an architecture, which would be similar in scope to the design of WalkSAT-XNF. If it is possible to design such an accelerator, we think that this would be deserving of a separate publication, given the novelty and considerable design challenges.\nWe would also like to clarify that we did not want to imply that Gauss-Jordan elimination (GJE) is easily implementable on IMC hardware. GJE requires altering many components within the matrix due to the elementary row operations, such as row swapping, adding/subtracting a subset of rows to replace a row within the matrix. Implementing this on an IMC crossbar array would necessitate multiple reprogramming steps--even if polynomially bounded--which is not ideal. Hence, for the CDCL combined with GJE--as implemented in CryptoMiniSAT--we believe that GJE should be performed independently on systems that can alter computational components efficiently and perform complex logic, which will require data transfer between the accelerator and a co-processor.\nConsidering the origin of GJE, as discussed in \"Extending SAT Solvers to Cryptographic Problems. SAT 2009: 244-257 by Mate Soos, Karsten Nohl, Claude Castelluccia\", it is primarily used for unit propagation after constructing a system of linear equations derived from XOR clauses. By taking an assumption set (i.e., assuming a subset of variable assignments within a search tree), unit propagation can be attempted whenever a single equality (i.e., an XOR clause) contains exactly one unassigned variable. Meanwhile, ongoing work for CDCL algorithms using hardware accelerators for CNF clauses--such as \"SAT-Accel: A modern SAT solver on an FPGA. In Proceedings of the 2025 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA ’25), 234–246. ACM by Lo, M., Chang, M.-C. F., & Cong, J.\"--has demonstrated novel techniques for accelerating propagations, which is referred to as the main bottleneck in conventional CDCL solvers. In their approach, each variable is assigned a unique bit-wise identifier derived from binary representation of an integer. Each clause is compactly represented by a signature, computed as the bitwise XOR of all variable IDs in that clause, along with a counter tracking the number of unassigned variables. Whenever a variable is assigned (i.e., joins the assumption set), its identifier is XORed with the current clause signature, and the counter is decremented. When only one variable remains unassigned, the resulting signature directly identifies that variable, enabling efficient unit propagation. This method relies on fixed-width XOR and simple counter operations. Although representing variable indices as bit-wise identifiers introduces a logarithmic overhead of log(n) bits the overall scheme appears suitable for hardware implementation. Moreover, both forward propagation and backtracking introduced in this method can reuse the same clause signatures (i.e., allowing to reuse the same clause signature to perform both operations), further simplifying the logic. Given that our IMC hardware natively supports XOR operations, we believe that our IMC hardware could be used to accelerate part of the computational approach presented by Lo et al. That said, as explained above, an evaluation of the feasibility and performance of this concept would require the design of an entirely new accelerator architecture, which is beyond the scope of our current manuscript.\nIn response to the reviewer’s comment, we have added reference [51] to the work by Lo et al. mentioned in the explanation above.\n“2. The comparison table shows that other accelerators do not natively support XNF.\nHowever, is it not possible to pre-process the XNF problems into a low-literal CNF\nformulation to run on these accelerators? If so, what would be the expected\nperformance penalty, and how would it affect the overall advantage claimed for your\narchitecture?”\nWe thank the reviewer for raising this very important point. As the reviewer correctly points out, our benchmark problems can be represented both as XNF problems and as CNF problems. Moreover, the problems can be represented as low-degree and high-degree problems after applying pre-processing techniques. In our benchmarks, these 4 different problem representations are named ‘CNF’, CNF-PP’, XNF’, and ‘XNF-PP’, where ‘-PP’ variants tend to involve higher degree counts, as shown in Table 2 in the manuscript. We have compared the performance when solving these different problem representations in Fig.S1 and in Tab.S1. We find that mapping to low-degree CNF problems increases iterations-to-solutions by a factor of ~100 compared to XNF-PP, while also increasing the number of variables and clauses by a factor of ~5. When solving the low-literal CNF problems with the SAT accelerators in Tab.S3, which are using local search heuristic similar to our work, this would result in considerably slower computation times compared to an XNF-native hardware accelerator. Moreover, we want to stress that due to the increase in the number of variables and clauses (see also Tab.2), the size of many of the low-degree SAT problems often becomes too large to fit into current SAT accelerators. Given the reviewer’s comment, we believe it is important to better emphasize these points in our manuscript. In section 3 of the Supplementary Information, we now specifically mention the scenario described by the reviewer:\n“Notably, while none of these accelerator devices support XOR clauses, it is still possible for them to solve hybrid XOR--CNF problems by mapping them to a CNF representation.”\nWe also added more details to explain the performance penalty of mapping to low-degree CNF problems and how that affects the overall performance of the SAT accelerators in Tab.S3.\n“It is important to note that these accelerator [12,14] have been specifically optimized for solving 3-SAT problems, that is, problems with only 3 literals per clause. Because of this, whereas the accelerator in Ref. [13] could solve the benchmarking problems in Fig.S1 using the preprocessed representation (i.e., ``CNF-PP'' in Fig.S1), the accelerators in Refs. [12,14] would have to use the un-preprocessed problem representation (i.e., ``CNF'' in Fig.S1). As our data in Fig.S1 shows, these problems are larger in size and more complex to solve with SLS solvers, which results in an ~30X increase in computation time and energy consumption. The benefits of the more energy-efficient 3-SAT solvers in Refs. [12,14] would thus likely be offset by the overhead of mapping to a 3-SAT formulation. Based on our comparison, we estimate that our accelerator is either better than, or on-par with, other state-of-the-art accelerators when solving our benchmarking problems in CNF representation. Projecting the performance of solving the benchmarking problems in XNF representation from Fig.S1, an XNF-capable SAT accelerator would attain an additional improvement by an order of magnitude in both runtime and energy consumption over pure CNF SAT accelerators due to the decrease in problem size and the higher algorithmic efficiency. We also note that the number of clauses for our benchmarking instances in CNF representation can be prohibitively large to implement with many of the CNF SAT accelerators listed in Table S3, whereas the XNF problems are sufficiently small to be implemented with existing crossbar arrays.”\n“3. For larger crossbar arrays, could the clock tree distribution and signal skew become a challenge for synchronization? Has this been analyzed or simulated?”\nThe reviewer raises a valid point. The distribution of clock signals can be a challenge and requires careful engineering by circuit designers. In our energy model, we consider energy consumption by clock trees in individual building blocks. We have not simulated and verified the clock distribution for the entire system. That said, there are various hardware systems that demonstrate the feasibility of achieving clock synchronization in accelerator devices using crossbar arrays, including accelerators for SAT problems [11,14] and AI workloads [45]. Some of these chips, e.g., in [45], achieve synchronous operation across multiple parallel crossbar arrays. Given that, we are confident that clock signal distribution is also feasible within our proposed architecture.\n“4. The simulation results are promising, but the reliance on idealistic models (28nm,\nno leakage) may overstate the advantages.”\nWe thank the reviewer for raising this point. Clearly, we haven’t done a good enough job in explaining the sources of the differences in performance in Table S3. In particular, our use of the term “leakage” appears to have caused a few misunderstandings about our energy model based on the 28nm TSMC foundry process. We’d like to clarify that our results are based on a commercial foundry process design kit (PDK). This PDK contains detailed models for leakage power in all building blocks, e.g., subthreshold leakage in transistors, which are also accounted for in our energy model. Our simulations are therefore a prediction of a chip fabricated in that foundry technology node. Within the discussion of Tab.S3, “leakage” was used to refer to the fact that many of the chips are proof-of-concept systems. Such systems are operated in testing environments, which can produce an additional energy overhead, e.g., due to additional losses from test PCBs, cables or external voltage/signal sources. The energy reported for the experimental systems in Tab.S3 can include these overhead losses, which would not be present in a fully integrated system. In contrast, our simulations aim to predict performance attainable by a fully integrated accelerator device and not that of a proof-of-concept system. Within our manuscript, we think it is important to explain this distinction to facilitate a fair comparison. Given the reviewer’s comment, we have decided to rewrite section 3 of the supplementary materials to better explain this point. We now explain the differences between experimental systems and our simulations in table S3 in the following way:\n“We note that the SAT accelerators reported in the literature [11-15] are experimental proof-of-concept systems, whereas the goal of our work is to project the performance attainable by a fully integrated accelerator device. Compared to our simulations, these proof-of-concept systems employ larger technology nodes and potentially less-efficient memory technology. Moreover, proof-of-concept systems are typically operated in test environments that can produce additional energy overhead, for example, due to energy losses incurred from test circuit boards, cables, or external signal sources. We have therefore included both simulations using our energy model (based on the work reported in Ref. [10]) and a proof-of-concept system of the SAT accelerator reported in Ref. [11] that uses our IMC architecture to solve CNF problems.”\n“Please provide a sensitivity analysis of key non-idealities (e.g., conductance\nvariations, ADC noise) on the solver’s success rate and energy efficiency.”\nWe thank the reviewer for the suggestion. We have added a sensitivity analysis to section 5 of the Supplementary Information. In this analysis, we investigate the influence of readout noise (e.g., noise from the TIAs, comparators, ADCs), as well as conductance variations of the RRAM cells (i.e., programming variations and thermal/telegraph noise) on the iterations-to-solution (ITS). As established in [18,36], we model the variations in the crossbar array’s bit line (BL) output voltage during each cycle 𝑡 as:\n𝑘\n𝑉 (𝑡 ) ∝ ∑(𝐺 +𝒩(0,𝜎 )+𝒩(0,𝜎 )(𝑡 ))𝑥 +𝒩(0,𝜎 )(𝑡 )\n𝐵𝐿,𝑖 𝑘 𝑖𝑗 𝑑2𝑑.𝑅𝑅𝐴𝑀 𝑐2𝑐,𝑅𝑅𝐴𝑀 𝑘 𝑗 𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡 𝑘\n𝑗\nHere, 𝐺 are the target conductance values of the RRAM cells and 𝑥 are Boolean input\n𝑖𝑗 𝑗\nvariables. Variations are approximated by Gaussian normal distributions 𝒩(η,σ) with zero mean and standard deviations 𝜎 (device-to-device RRAM conductance variations\n𝑑2𝑑,𝑅𝑅𝐴𝑀\nduring programming), 𝜎 (cycle-to-cycle RRAM conductance variations due to\n𝑐2𝑐,𝑅𝑅𝐴𝑀\nthermal/telegraph noise) and 𝜎 (cycle-to-cycle variations due to noise in the\n𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡\nreadout circuit, e.g., TIAs, comparators, ADCs). Cycle-to-cycle variations change every\ncycle 𝑡 , whereas device-to-device variations are set initially and remain constant over time.\n𝑘\nThe conductance-dependent RRAM variations 𝜎 and 𝜎 are based on the\n𝑑2𝑑,𝑅𝑅𝐴𝑀 𝑐2𝑐,𝑅𝑅𝐴𝑀\nmodel in Ref. [18], which is derived from device characterizations of TaO memristors in Ref.\n[19]. Here, we assume that the conductance of the low resistance state (LRS) is at 2uS and\nthat the high resistance state (HRS) is at 20nS. In our analysis, we then sweep the magnitude\nof the readout noise 𝜎 to investigate how much noise in the peripheral readout\n𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡\ncircuits can be tolerated before performance of WalkSAT-XNF degrades.\nIn figure (a) below, we show the cumulative success rate for the MDP benchmark instance\n‘par8-3’ for different readout noise levels 𝜎 and find that increasing the noise will\n𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡\neventually lead to a lower success rate. When analyzing ITS of three exemplary MDP\ninstances as a function of the readout noise in figure (b), we find that ITS remains close to\nthe ideal simulations (without RRAM variations and readout noise) until a noise standard\ndeviation of 𝜎 ~0.15 (i.e., fluctuations of up to 15% relative to the voltage steps in\n𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡\nthe ADC). For larger noise, ITS will begin to deteriorate. We have also performed the same\nanalysis for an LRS conductance of 4uS (figure (c)) and 6uS (figure (d)). When increasing the\nconductance, the relative amount of noise from the RRAM cells decreases, thereby\nenhancing the signal-to-noise ratio. We observe increased robustness to readout noise of\nup to 𝜎 = 0.25, which also increases energy per iteration by up to 10 percent due\n𝑐2𝑐,𝑟𝑒𝑎𝑑𝑜𝑢𝑡\nto the increase in current flowing through the RRAM cells. We want to stress that readout\ncycle-to-cycle fluctuations of over 10 percent are larger than what we observe in our IMC\nhardware. Based on circuit simulations, we expect fluctuations in the range of a few percent\nat most.\nThis is also in agreement with our data in Fig.3, where we wanted to experimentally verify\nwhether variability in the IMC hardware significantly affects the performance of WalkSAT-\nXNF. In our experiments, we performed the analog computations within WalkSAT-XNF\n(clause evaluation and make/break value computation) on an actual RRAM chip. The RRAM\ncells in our test chip were programmed with a relatively large variability of ~10%. Our results\nshow that, despite the RRAM variations and despite readout noise present in our test chip,\nwe can evaluate clauses with just ~1% error. When using the hardware to solve XNF\nproblems, the success rate and computation time agree well with our ideal noiseless\nsimulations, showing that errors due to device non-idealities do not accumulate\nsignificantly enough to affect the solver’s performance. To further verify this, we show\nadditional experiments on another IMC chip for the ‘par8-2’ and ‘par8-3’ benchmark\nproblems below. We can again see good agreement between ideal noiseless simulations\nand the hardware experiments. Our sensitivity analysis and our hardware experiments thus\nindicate that WalkSAT-XNF is sufficiently resilient to hardware non-idealities. We believe\nthis to be due to the binary RRAM weights and the binary input states. The results of the\ncrossbar array operation are thus integer values, whose discrete nature is significantly more\nrobust to noise compared to continuous floating-point operations.\nIn response to the reviewer’s remarks, we have added a new section 5 to the Supplementary\nInformation based on our reply above. We have also added additional details to section 2.4,\nwhere we discuss the dominant types of non-idealities in CiM hardware:\n“As with other mixed-signal computing systems, realizing WalkSAT-XNF in hardware\nrequires it to be sufficiently resilient against hardware non-idealities in the analog circuits.\nStudies have identified variations in the RRAM cells and noise in the crossbar array's analog\nreadout circuit as the dominant non-idealities that can result in a deterioration in\nperformance [36].”\n“This observation is also supported by a simulation-based sensitivity study, the results of\nwhich are presented in the Supplementary Information. We believe this robustness to be due\nto the fact that the weights and the input states in our architecture are binary. The results of\nthe crossbar array's operations are discrete integer values, thereby providing additional\nrobustness against noise, compared to, for example, floating point operations.”\nReferences (as numbered in the revised manuscript and the Supplementary Information):\n[8] G. Pedretti, F. Böhm, T. Bhattacharya, A. Heittman, X. Zhang, M. Hizzani, G. Hutchinson,\nD. Kwon, J. Moon, E. Valiante, I. Rozada, C. E. Graves, J. Ignowski, M. Mohseni, J. P. Strachan,\nD. Strukov, R. Beausoleil, and T. V. Vaerenbergh, Solving Boolean satisfiability problems\nwith resistive content addressable memories, npj Unconventional Computing 2, 7 (2025).\n[10] Q. Zhang, S. Su, Z. Liu, H.-C. Cheng, Z. Qiu, M. Palaria, J. Ye, D. Meng, B. Chen, S.\nHossain, W. Wu, and M. S.-W. Chen, A stochastic analog sat solver in 65nm CMOS achieving\n6.6μs average solution time with 100% solvability for hard 3-sat problems, in 2024 IEEE\nSymposium on VLSI Technology and Circuits (VLSI Technology and Circuits) (2024).\n[11] C. Shim, J. Bae, and B. Kim, 30.3 VIP-Sat: A Boolean Satisfiability Solver Featuring 5×12\nVariable In-Memory Processing Elements with 98% Solvability for 50-Variables 218-Clauses\n3-SAT Problems, in 2024 IEEE International Solid-State Circuits Conference (ISSCC) (IEEE,\n2024) pp. 486–488.\n[12] S. Xie, M. Yang, S. A. Lanham, Y. Wang, M. Wang, S. Oruganti, and J. P. Kulkarni, 29.2\nSnap-SAT: A One-Shot Energy-Performance-Aware All-Digital Compute-in-Memory Solver\nfor Large-Scale Hard Boolean Satisfiability Problems, in 2023 IEEE International Solid- State\nCircuits Conference (ISSCC) (IEEE, 2023) pp. 420–422.\n[14] T. Bhattacharya, D. Kwon, G. Hutchinson, X. Zhang, I. Rozada, and D. Strukov, A Fully\nIntegrated Mixed-Signal Compute-In-Memory Accelerator for Solving Arbitrary Order\nBoolean Satisfiability Problems, in 2024 IEEE Symposium on VLSI Technology and Circuits\n(VLSI Technology and Circuits) (2025).\n[18] L. Zhao, L. Buonanno, A. Natarajan, J. Ignowski, and G. Pedretti, Noise aware finetuning\nfor analog non-linear dot product engine, in NeurIPS 2024 Workshop Machine Learning with\nnew Compute Paradigms (2024).\n[19] X. Sheng, C. E. Graves, S. Kumar, X. Li, B. Buchanan, L. Zheng, S. Lam, C. Li, and J. P.\nStrachan, Low-conductance and multilevel CMOS-integrated nanoscale oxide memristors,\nAdvanced Electronic Materials 5, 1800876 (2019).\n[36] A. Heittmann, M. Hizzani, and J. P. Strachan, in 2025 IEEE International Symposium on\nCircuits and Systems (ISCAS) (2025) pp. 1–5.580\n[46] S. Ambrogio, P. Narayanan, A. Okazaki, A. Fasoli, C. Mackin, K. Hosokawa, A. Nomura,\nT. Yasuda, A. Chen, A. Friz, M. Ishii, J. Luquin, Y. Kohda, N. Saulnier, K. Brew, S. Choi, I. Ok,\nT. Philip, V. Chan, C. Silvestre, I. Ahsan, V. Narayanan, H. Tsai, and G. W. Burr, An analog-AI\nchip for energy-efficient speech recognition and transcription, Nature 620, 768-775 (2023)\n[51] M. Lo, M.-C. F. Chang, and J. Cong, SAT-Accel: A modern sat solver on a FPGA, in\nProceedings of the 2025 ACM/SIGDA International Symposium on Field Programmable Gate\nArrays, FPGA ’25 (Association for Computing Machinery, New York, NY, USA, 2025) p. 234–\n246.608"}, {"round": 3, "reviewer_comments": {"reviewer_1": "The authors have made substantial improvements in the discussion of hardware non-idealities as well as in the comparison with the state-of-the-art works, and have addressed my previous concerns. One remaining issue is the reference numbering. The authors note that the references in the response letter are as numbered in the revised manuscript and the Supplementary Information. However, I found that references [8] and [14] in the response letter correspond to [10] and [11] in the revised Supplementary Information. This inconsistency confuses me. Please make sure that the reference numbering is consistent and correct across the main manuscript and the Supplementary Information.", "reviewer_2": "The author provided detailed responses to the previous suggestions. After review, I believe that the authors have adequately addressed the issues raised and my previous concerns have been resolved. I suggest accepting the current form of the manuscript."}, "author_response": "Reviewer #1:\nThe authors have made substantial improvements in the discussion of hardware non-idealities as\nwell as in the comparison with the state-of-the-art works, and have addressed my previous\nconcerns. One remaining issue is the reference numbering. The authors note that the references in\nthe response letter are as numbered in the revised manuscript and the Supplementary Information.\nHowever, I found that references [8] and [14] in the response letter correspond to [10] and [11] in\nthe revised Supplementary Information. This inconsistency confuses me. Please make sure that\nthe reference numbering is consistent and correct across the main manuscript and the\nSupplementary Information.\n-> Response:\nWe thank the reviewer for the positive assessment of our revisions. We sincerely thank the reviewer\nfor the time and thoughtful feedback provided throughout the review process.\nWe appreciate the reviewer pointing out the confusion regarding the reference numbering in our\nprevious response. We apologize for the lack of clarity. To comply with the journal’s formatting\nguidelines, the Supplementary Information (SI) maintains a dedicated, independent reference list\nthat starts from [1]. Consequently, the numbering in the SI does not align with the numbering in the\nMain Manuscript. In our previous response letter, citations [8] and [14] referred to the Main\nManuscript’s bibliography, whereas citations [10] and [11] referred to the SI bibliography. We\nunderstand that using these numbers interchangeably without specifying the source was confusing.\nWe have ensured that the references are organized following the guidelines.\nReviewer #2 (Remarks to the Author):\nThe author provided detailed responses to the previous suggestions. After review, I believe that the\nauthors have adequately addressed the issues raised and my previous concerns have been\nresolved. I suggest accepting the current form of the manuscript.\n-> Response:\nWe sincerely thank the reviewer for the positive feedback and for recommending our manuscript for\npublication. We appreciate the time the reviewer dedicated to evaluating our work and the\nconstructive suggestions provided during the review process."}]

Decision letter