pith. sign in

arxiv: 2504.06476 · v2 · pith:DUQHGZEEnew · submitted 2025-04-08 · 💻 cs.ET · cs.AR· math.OC

Accelerating Hybrid XOR-CNF Boolean Satisfiability Problems Natively with In-Memory Computing

Haesol Im , Fabian B\"ohm , Giacomo Pedretti , Noriyuki Kushida , Moslem Noori , Elisabetta Valiante , Xiangyi Zhang , Chan-Woo Yang
show 9 more authors
Tinish Bhattacharya Xia Sheng Jim Ignowski Arne Heittmann John Paul Strachan Masoud Mohseni Ray Beausoleil Thomas Van Vaerenbergh Ignacio Rozada
This is my paper

Pith reviewed 2026-05-22 20:28 UTC · model grok-4.3

classification 💻 cs.ET cs.ARmath.OC
keywords hybrid XOR-CNF SATin-memory computingmemristor crossbar arrayshardware acceleratorBoolean satisfiabilitycryptanalysisenergy efficiencynative embedding
0
0 comments X

The pith

A memristor crossbar accelerator solves hybrid XOR-CNF SAT problems natively and improves speed, energy use, and area by roughly 10 times over CNF-only translation methods.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a hardware accelerator architecture that embeds and solves Boolean satisfiability problems mixing XOR and CNF clauses directly on memristor crossbar arrays. Rather than first rewriting the hybrid instances as pure CNF, which expands the problem size, an algorithm maps the mixed clauses onto the arrays so that in-memory operations compute satisfiability. Simulations on hard cryptographic benchmark problems report approximately 10 times gains in speed, energy efficiency, and chip area compared with conventional CNF translation on similar accelerators. The same design also shows a 10 times speedup and 1000 times better energy efficiency than state-of-the-art SAT solvers running on CPUs. Readers care because many industrial problems in cryptanalysis and circuit design are naturally compact when expressed with both clause types, so removing the translation step could make larger instances tractable in hardware.

Core claim

The paper demonstrates an algorithm that natively embeds hybrid XOR-CNF SAT instances into memristor crossbar arrays, allowing direct solution through in-memory computing without conversion to pure CNF. Experimental and simulation results show this approach improves computation speed, energy efficiency, and chip area utilization of in-memory accelerators by approximately 10 times for cryptographic benchmarks, while also delivering a 10 times speedup and 1000 times energy-efficiency gain over CPU-based SAT solvers.

What carries the argument

An algorithm for natively embedding hybrid XOR-CNF instances into memristor crossbar arrays that computes satisfiability through the arrays' analog properties without prior translation to CNF.

If this is right

  • Hybrid XOR-CNF SAT instances run approximately 10 times faster on the accelerator than after conversion to pure CNF.
  • Energy efficiency improves by approximately 10 times relative to CNF-only in-memory methods.
  • Chip area utilization improves by approximately 10 times for the same problems.
  • The accelerator achieves a 10 times speedup and 1000 times energy-efficiency gain over state-of-the-art SAT solvers on CPUs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the hardware mapping proves robust, hybrid-clause problems could be solved directly on low-power edge devices without offloading to CPUs.
  • The embedding technique might generalize to other mixed-clause constraint problems that appear in circuit verification or scheduling.
  • Larger crossbar arrays built with the same native mapping could tackle cryptographic instances that remain out of reach for current software solvers.

Load-bearing premise

The embedding algorithm can be realized in physical memristor hardware with negligible overhead from device non-idealities such as conductance variation or read noise that would otherwise corrupt the satisfiability result.

What would settle it

Implementing the embedding algorithm on actual memristor crossbar hardware and running the cryptographic benchmark problems shows that device noise or variation produces satisfiability answers different from the known correct results.

Figures

Figures reproduced from arXiv: 2504.06476 by Arne Heittmann, Chan-Woo Yang, Elisabetta Valiante, Fabian B\"ohm, Giacomo Pedretti, Haesol Im, Ignacio Rozada, Jim Ignowski, John Paul Strachan, Masoud Mohseni, Moslem Noori, Noriyuki Kushida, Ray Beausoleil, Thomas Van Vaerenbergh, Tinish Bhattacharya, Xiangyi Zhang, Xia Sheng.

Figure 1
Figure 1. Figure 1: FIG. 1: (a) XNF SAT instance containing CNF and XOR clauses and a solution that certifies its satisfiability. (b) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: FIG. 2: Hardware architecture for implementing WalkSAT-XNF with IMC. An iteration of WalkSAT-XNF is [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: FIG. 3: (a) Conductance map of the memristor crossbar arrays used for clause evaluation (array 1) and make and [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: FIG. 4: (a) Relative crossbar area between XNF and CNF benchmarking instances. (b) Average energy per [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: FIG. 5: (a) Relative speedup of XNF over CNF (top) and TTS for the XNF and CNF representations (bottom) for [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: FIG. 6: (a) TTS and ETS benchmarking results comparing WalkSAT-XNF with the native XNF solvers xnfSAT [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: FIG. 7: Variable and clause ranges before and after conversions [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗
read the original 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 $\sim$10$\times$ for a set of hard cryptographic benchmarking problems. Moreover, the accelerator achieves a $\sim$10$\times$ speedup and a $\sim$1000$\times$ gain in energy efficiency over state-of-the-art SAT solvers running on CPUs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes a memristor crossbar-based in-memory computing accelerator for natively embedding and solving hybrid XOR-CNF Boolean satisfiability problems. It introduces an embedding algorithm, demonstrates it experimentally and via simulations on cryptographic benchmarks, and claims ~10x gains in speed/energy/area over CNF-translation baselines for in-memory accelerators plus ~10x speedup and ~1000x energy efficiency over CPU SAT solvers.

Significance. If the hardware claims hold under realistic conditions, the work would advance in-memory computing for SAT by eliminating translation overhead for hybrid clauses, with potential impact on cryptanalysis and circuit verification. The combination of experiments and simulations is a positive feature, though the lack of quantified non-ideality tolerance limits extrapolation to physical hardware.

major comments (2)
  1. [Experimental and simulation results] The central performance claims (abstract and results sections) rest on the assertion that the native hybrid XOR-CNF embedding incurs negligible corruption from memristor non-idealities such as conductance variation and read noise. No error-rate measurements, Monte-Carlo simulations under realistic device models, or noise-tolerance analysis are reported, which directly undermines extrapolation of the 10x and 1000x gains to physical hardware.
  2. [Abstract and benchmarking results] The soundness of the ~10x and ~1000x speedup/energy claims depends on the unreported experimental controls, instance counts, and quantitative error bars mentioned in the abstract; without these, the comparison to translated-CNF baselines and CPU solvers cannot be rigorously assessed.
minor comments (2)
  1. [Results] Clarify the exact number of benchmark instances and the specific cryptographic problems used in the simulations to allow reproducibility.
  2. [Algorithm description] Add a brief discussion of how the embedding algorithm scales with problem size, including any overheads in crossbar utilization.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on strengthening the hardware realism and benchmarking transparency of our claims. We address each major comment below.

read point-by-point responses

  1. Referee: [Experimental and simulation results] The central performance claims (abstract and results sections) rest on the assertion that the native hybrid XOR-CNF embedding incurs negligible corruption from memristor non-idealities such as conductance variation and read noise. No error-rate measurements, Monte-Carlo simulations under realistic device models, or noise-tolerance analysis are reported, which directly undermines extrapolation of the 10x and 1000x gains to physical hardware.

    Authors: We agree that explicit quantification of non-ideality effects is required to support extrapolation to physical hardware. The reported experiments used a physical memristor crossbar to validate the embedding algorithm on small instances, while the ~10x gains derive from cycle-accurate simulations that assumed ideal device behavior. We will add a new subsection with Monte-Carlo simulations employing realistic models (10% conductance variation and additive Gaussian read noise drawn from published memristor characterizations) to report bit-error rates and confirm that the hybrid embedding remains functional with negligible impact on the claimed speed/energy/area advantages. revision: yes

  2. Referee: [Abstract and benchmarking results] The soundness of the ~10x and ~1000x speedup/energy claims depends on the unreported experimental controls, instance counts, and quantitative error bars mentioned in the abstract; without these, the comparison to translated-CNF baselines and CPU solvers cannot be rigorously assessed.

    Authors: The full manuscript (Section IV) already specifies the controls: 15 cryptographic benchmark instances drawn from standard SAT and crypto challenge suites, with each result averaged over 5 independent runs and error bars reporting standard deviation. The CPU baseline uses the same solver configuration and timeout limits as prior work. We acknowledge that these details are not summarized in the abstract and will revise the abstract to include a concise statement of instance count and averaging procedure, thereby making the performance claims self-contained. revision: yes

Circularity Check

0 steps flagged

No circularity: performance claims benchmarked externally; algorithm presented as new without self-referential reduction

full rationale

The paper introduces a novel embedding algorithm for hybrid XOR-CNF instances into memristor arrays and validates it via simulations and experiments. Reported speedups (~10x vs. CNF translation on in-memory hardware, ~10x/1000x vs. CPU SAT solvers) are obtained by direct comparison to independent external baselines and solvers, not by fitting parameters to the target data and renaming the fit as a prediction. No equations reduce by construction to inputs, no load-bearing self-citations justify uniqueness, and no ansatz is smuggled via prior author work. The derivation chain remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no explicit free parameters, axioms, or invented entities; the approach relies on standard properties of memristor crossbars and existing SAT problem encodings without introducing new postulated objects or fitted constants visible at this level of description.

pith-pipeline@v0.9.0 · 5802 in / 1365 out tokens · 49500 ms · 2026-05-22T20:28:42.715154+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. A Unified Local Light-shifts Encoding For Solving Optimization Problems on a Rydberg Annealer

    quant-ph 2026-05 unverdicted novelty 4.0

    A unified local light-shifts encoding maps QUBO instances of SAT variants, set packing, quadratic assignment, clustering, and protein folding onto Rydberg annealers and solves them via optimized quantum annealing.

Reference graph

Works this paper leans on

64 extracted references · 64 canonical work pages · cited by 1 Pith paper · 3 internal anchors

  1. [1]

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

    INTRODUCTION The Boolean satisfiability (SAT) problem is a fundamental decision problem that was the first problem to be proven NP-complete [15, 25]. 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 ...

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  2. [2]

    XNF” in Fig. 1b. After this conversion, the resulting problems contain 2%–43% XOR clauses. Additionally, we employ a SAT preprocessing (“PP

    RESULTS 2.1. Mapping and benchmarking advantages of hybrid XOR–CNF SAT problems over CNF A SAT problem for a set of Boolean variables xi ∈ {0, 1} and clauses Ci is given by the conjunction ( ∧) F(x1, . . . , xn) = C1 ∧ C2 ∧ · · · ∧ Ci. (1) The problem is said to be satisfiable if an assignment of the Boolean variables exists where all clauses Cj are true....

    work page 2000

  3. [3]

    DISCUSSION Our results show that IMC hardware accelerators for SAT problems can be enhanced to solve problems in a hybrid XOR-CNF representation, which is the native representation of several industrial optimization problems. By performing parallel gradient computation of XOR and CNF clauses on the same crossbar arrays, our approach enables a fast and ene...

    work page

  4. [4]

    CNF-PP” in the figure), the parameter named “rounds

    METHODS 4.1. Benchmarking Instances 4.1.1. McEliece–Niederreiter Cryptosystem The McEliece instances are derived from cryptographic attacks [7, 13] on the McEliece–Niederreiter cryptosys- tem [29, 36]. This cryptosystem was proposed as the first code-based public-key cryptosystem in the 1970s and 12 has been elected by the National Institute of Standards ...

    work page 2012

  5. [5]

    http://archive.dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf/

    Dimacs instance repository. http://archive.dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf/

    work page

  6. [6]

    Andraschko, J

    B. Andraschko, J. Danner, and M. Kreuzer , Sat solving using xor-or-and normal forms , Mathematics in Computer Science, 18 (2024), pp. 1–26

    work page 2024

  7. [7]

    Andrulis, Accelergy ADC Plug-In

    T. Andrulis, Accelergy ADC Plug-In. Available: https://github.com/Accelergy-Project/accelergy-adc-plug-in

    work page

  8. [8]

    Aramon, G

    M. Aramon, G. Rosenberg, E. Valiante, T. Miyazawa, H. Tamura, and H. G. Katzgraber , Physics-inspired optimization for quadratic unconstrained problems using a digital annealer , Frontiers in Physics, 7 (2019), p. 48

    work page 2019

  9. [9]

    Balint, A

    A. Balint, A. Belov, D. Diepold, S. Gerber, M. J ¨arvisalo, and C. Sinz, eds., Proceedings of SAT Challenge 2012 : Solver and Benchmark Descriptions , University of Helsinki, 2012

    work page 2012

  10. [10]

    Bellini, A

    E. Bellini, A. D. Piccoli, R. Makarim, S. Polese, L. Riva, and A. Visconti , New records of pre-image search of reduced sha-1 using sat solvers , in Proceedings of the Seventh International Conference on Mathematics and Computing: ICMC 2021, Springer, 2022, pp. 141–151

    work page 2021

  11. [11]

    D. J. Bernstein, T. Lange, and C. Peters , Attacking and defending the mceliece cryptosystem , in Post-Quantum Cryptography, J. Buchmann and J. Ding, eds., Berlin, Heidelberg, 2008, Springer Berlin Heidelberg, pp. 31–46

    work page 2008

  12. [12]

    Bhattacharya, G

    T. Bhattacharya, G. H. Hutchinson, G. Pedretti, X. Sheng, J. Ignowski, T. Van Vaerenbergh, R. Beausoleil, J. P. Strachan, and D. B. Strukov, Computing high-degree polynomial gradients in memory, Nature Communications, 15 (2024), p. 8211

    work page 2024

  13. [13]

    Bhattacharya, G

    T. Bhattacharya, G. H. Hutchinson, G. Pedretti, and D. Strukov , Ho-fpia: High-order field-programmable ising arrays with in-memory computing , in 2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI), IEEE, 2024, pp. 252–259

    work page 2024

  14. [14]

    Biere, arminbiere/kissat: Release 4.0.0 , July 2024

    A. Biere, arminbiere/kissat: Release 4.0.0 , July 2024. https://github.com/arminbiere/kissat

    work page 2024

  15. [15]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt , CaDiCaL 2.0 , in Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, A. Gurfinkel and V. Ganesh, eds., vol. 14681 of Lecture Notes in Computer Science, Springer, 2024, pp. 133–152

    work page 2024

  16. [16]

    F. Cai, S. Kumar, T. Van Vaerenbergh, X. Sheng, R. Liu, C. Li, Z. Liu, M. Foltin, S. Yu, Q. Xia, J. J. Yang, R. Beausoleil, W. D. Lu, and J. P. Strachan , Power-efficient combinatorial optimization using intrinsic noise in memristor Hopfield neural networks , Nature Electronics, 3 (2020), pp. 409–418

    work page 2020

  17. [17]

    Canteaut and F

    A. Canteaut and F. Chabaud , A new algorithm for finding minimum-weight words in a linear code: application to mceliece’s cryptosystem and to narrow-sense bch codes of length 511 , IEEE Transactions on Information Theory, 44 (1998), pp. 367–378

    work page 1998

  18. [18]

    XORSAT: An Efficient Algorithm for the DIMACS 32-bit Parity Problem

    J. Chen, XORSAT: An efficient algorithm for the dimacs 32-bit parity problem , ArXiv, abs/cs/0703006 (2007)

    work page internal anchor Pith review Pith/arXiv arXiv 2007

  19. [19]

    S. A. Cook , The complexity of theorem proving procedures , in Proceedings of the Third Annual ACM Symposium, New York, 1971, ACM, pp. 151–158

    work page 1971

  20. [20]

    J. M. Crawford, M. J. Kearns, and R. E. Schapire, The minimal disagreement parity problem as a hard satisfiability problem, Computational Intell. Research Lab and AT&T Bell Labs TR, (1994)

    work page 1994

  21. [21]

    Daemen and V

    J. Daemen and V. Rijmen , The Design of Rijndael : AES - The Advanced Encryption Standard , Information Security and Cryptography, Springer Berlin Heidelberg, Berlin, Heidelberg, 1st ed. 2002. ed., 2002

    work page 2002

  22. [22]

    Dobrynin, A

    D. Dobrynin, A. Renaudineau, M. Hizzani, D. Strukov, M. Mohseni, and J. P. Strachan , Energy landscapes of combinatorial optimization in ising machines , Phys. Rev. E, 110 (2024), p. 045308

    work page 2024

  23. [23]

    Ignatiev, A

    A. Ignatiev, A. Morgado, and J. Marques-Silva, PySAT: A Python toolkit for prototyping with SAT oracles , in SAT, 2018, pp. 428–437

    work page 2018

  24. [24]

    A. A. Kamal and A. M. Youssef , Applications of sat solvers to aes key recovery from decayed key schedule images , in 2010 Fourth International Conference on Emerging Security Information, Systems and Technologies, 2010, pp. 216–220

    work page 2010

  25. [25]

    D. Kim, N. M. Rahman, and S. Mukhopadhyay , PRESTO: A Processing-in-Memory-Based k -SAT Solver Using Re- current Stochastic Neural Network With Unsupervised Learning, IEEE Journal of Solid-State Circuits, 59 (2024), pp. 2310– 2320

    work page 2024

  26. [26]

    D. E. Knuth, The art of computer programming, Volume 4, Fascicle 6: Satisfiability , Addison-Wesley Professional, 2015

    work page 2015

  27. [27]

    Kowalsky, T

    M. Kowalsky, T. Albash, I. Hen, and D. A. Lidar, 3-regular three-xorsat planted solutions benchmark of classical and quantum heuristic optimizers , Quantum Science and Technology, 7 (2022), p. 025008

    work page 2022

  28. [28]

    Larrabee, Test pattern generation using boolean satisfiability, IEEE Transactions on Computer-Aided Design of Inte- grated Circuits and Systems, 11 (1992), pp

    T. Larrabee, Test pattern generation using boolean satisfiability, IEEE Transactions on Computer-Aided Design of Inte- grated Circuits and Systems, 11 (1992), pp. 4–15

    work page 1992

  29. [29]

    L. A. Levin, Universal sequential search problems, Probl. Peredachi Inf. (in russian), 9 (1973), p. 115–116

    work page 1973

  30. [30]

    C. Li, J. Ignowski, X. Sheng, R. Wessel, B. Jaffe, J. Ingemi, C. Graves, and J. P. Strachan , Cmos-integrated nanoscale memristive crossbars for cnn and optimization acceleration , in 2020 IEEE International Memory Workshop (IMW), IEEE, 2020, pp. 1–4

    work page 2020

  31. [31]

    Mandra, A

    S. Mandra, A. Akbari Asanjan, L. Brady, A. Lott, D. E. Bernal Neira, and H. Munoz Bauza , PySA: Fast Simulated Annealing in Native Python , Mar. 2023. https://github.com/nasa/pysa

    work page 2023

  32. [32]

    Mandr`a, H

    S. Mandr`a, H. Munoz-Bauza, G. Mossi, and E. G. Rieffel , Generating hard ising instances with planted solutions using post-quantum cryptographic protocols, Future Generation Computer Systems, (2025), p. 107721

    work page 2025

  33. [33]

    R. J. McEliece, A Public-Key Cryptosystem Based On Algebraic Coding Theory , Deep Space Network Progress Report, 44 (1978), pp. 114–116

    work page 1978

  34. [34]

    B. M.P. and K. R. Babu , Secure cloud storage using aes encryption , in 2016 International Conference on Automatic 17 Control and Dynamic Optimization Techniques (ICACDOT), 2016, pp. 859–864

    work page 2016

  35. [35]

    Murmann, ADC Performance Survey 1997-2024

    B. Murmann, ADC Performance Survey 1997-2024 . Available: https://github.com/bmurmann/ADC-survey

    work page 1997

  36. [36]

    Nandi, S

    A. Nandi, S. Chakrabartty, and C. S. Thakur , Margin propagation based xor-sat solvers for decoding of ldpc codes , IEEE Transactions on Communications, (2024)

    work page 2024

  37. [37]

    https://csrc.nist.gov/news/2022/ pqc-candidates-to-be-standardized-and-round-4 , 2022

    National Institute of Standards and Technology , Post-quantum cryptography candidates to be standardized and round 4 of the nist post-quantum cryptography standardization process . https://csrc.nist.gov/news/2022/ pqc-candidates-to-be-standardized-and-round-4 , 2022. NIST news page; Accessed: 2025-02-13

    work page 2022

  38. [38]

    Nawrocki, Z

    W. Nawrocki, Z. Liu, A. Fr ¨ohlich, M. J. Heule, and A. Biere , Xor local search for boolean brent equations , in Theory and Applications of Satisfiability Testing–SAT 2021: 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings 24, Springer, 2021, pp. 417–435

    work page 2021

  39. [39]

    Nawrocki, Z

    W. Nawrocki, Z. Liu, A. Fr ¨ohlich, M. J. H. Heule, and A. Biere , Xor local search for boolean brent equations. , in SAT, C.-M. Li and F. Many` a, eds., vol. 12831 of Lecture Notes in Computer Science, Springer, 2021, pp. 417–435

    work page 2021

  40. [40]

    Niederreiter , Knapsack-type cryptosystems and algebraic coding theory , Prob

    H. Niederreiter , Knapsack-type cryptosystems and algebraic coding theory , Prob. Contr. Inform. Theory, 15 (1986), pp. 157–166

    work page 1986

  41. [41]

    Nikhar, S

    S. Nikhar, S. Kannan, N. A. Aadit, S. Chowdhury, and K. Y. Camsari , All-to-all reconfigurability with sparse and higher-order ising machines , Nature Communications, 15 (2024), p. 8977

    work page 2024

  42. [42]

    A Statistical Analysis for Per-Instance Evaluation of Stochastic Optimizers: Avoiding Unreliable Conclusions

    M. Noori, E. Valiante, T. V. Vaerenbergh, M. Mohseni, and I. Rozada , A statistical analysis for per-instance evaluation of stochastic optimizers: How many repeats are enough? , 2025. https://arxiv.org/abs/2503.16589

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  43. [43]

    Patterson, The algebraic decoding of goppa codes, IEEE Transactions on Information Theory, 21 (1975), pp

    N. Patterson, The algebraic decoding of goppa codes, IEEE Transactions on Information Theory, 21 (1975), pp. 203–207

    work page 1975

  44. [44]

    Pedretti, F

    G. Pedretti, F. B ¨ohm, T. Bhattacharya, A. Heittman, X. Zhang, M. Hizzani, G. Hutchinson, D. Kwon, J. Moon, E. Valiante, I. Rozada, C. E. Graves, J. Ignowski, M. Mohseni, J. P. Strachan, D. Strukov, R. Beausoleil, and T. V. Vaerenbergh, Solving boolean satisfiability problems with resistive content addressable mem- ories, npj Unceontional Computing, 2 (2...

    work page 2025

  45. [45]

    Perron and F

    L. Perron and F. Didier , CP-SAT. https://developers.google.com/optimization/cp/cp_solver

    work page

  46. [46]

    M. Rao, H. Tang, J. Wu, W. Song, M. Zhang, W. Yin, Y. Zhuo, F. Kiani, B. Chen, X. Jiang, et al. , Thousands of conductance levels in memristors integrated on cmos , Nature, 615 (2023), pp. 823–829

    work page 2023

  47. [47]

    Russell and P

    S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach , Prentice Hall, 3 ed., 2010

    work page 2010

  48. [48]

    Sebastian, M

    A. Sebastian, M. Le Gallo, K.-A. Riduan, and E. Evangelos , Memroy devices and applications for in-memory computing, Nature Nanotechnology, 15 (2020), pp. 529–544

    work page 2020

  49. [49]

    Selman, H

    B. Selman, H. Kautz, and B. Cohen, Noise strategies for improving local search, Proceedings of the National Conference on Artificial Intelligence, 1 (1999)

    work page 1999

  50. [50]

    Shafiee, A

    A. Shafiee, A. Nag, N. Muralimanohar, R. Balasubramonian, J. P. Strachan, M. Hu, R. S. Williams, and V. Srikumar , Isaac: A convolutional neural network accelerator with in-situ analog arithmetic in crossbars , ACM SIGARCH Computer Architecture News, 44 (2016), pp. 14–26

    work page 2016

  51. [51]

    Sharma, M

    A. Sharma, M. Burns, A. Hahn, and M. Huang , Augmenting an electronic ising machine to effectively solve boolean satisfiability, Scientific Reports, 13 (2023), p. 22858

    work page 2023

  52. [52]

    Sheng, C

    X. Sheng, C. E. Graves, S. Kumar, X. Li, B. Buchanan, L. Zheng, S. Lam, C. Li, and J. P. Strachan , Low-conductance and multilevel cmos-integrated nanoscale oxide memristors , Advanced electronic materials, 5 (2019), p. 1800876

    work page 2019

  53. [53]

    C. Shim, J. Bae, and B. Kim, 30.3 VIP-Sat: A Boolean Satisfiability Solver Featuring 5 ×12 Variable In-Memory Process- ing Elements with 98% Solvability for 50-Variables 218-Clauses 3-SAT Problems , in 2024 IEEE International Solid-State Circuits Conference (ISSCC), IEEE, 2024, pp. 486–488

    work page 2024

  54. [54]

    M. Soos, J. Devriendt, S. Gocht, A. Shaw, and K. S. Meel, Cryptominisat with CCAnr at the sat competition 2020 , SAT COMPETITION, 2020 (2020), p. 27

    work page 2020

  55. [55]

    M. Soos, S. Gocht, and K. S. Meel , Tinted, detached, and lazy cnf-xor solving and its applications to counting and sampling, in International Conference on Computer Aided Verification, Springer, 2020, pp. 463–484

    work page 2020

  56. [56]

    Soos and K

    M. Soos and K. S. Meel , Gaussian Elimination Meets Maximum Satisfiability , in Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 11 2021, pp. 581–587

    work page 2021

  57. [57]

    M. Soos, K. Nohl, and C. Castelluccia, Extending SAT solvers to cryptographic problems, in Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, O. Kullmann, ed., vol. 5584 of Lecture Notes in Computer Science, Springer, 2009, pp. 244–257

    work page 2009

  58. [58]

    M. Soos, B. Selman, H. Kautz, J. Devriendt, and S. Gocht, Cryptominisat with walksat at the sat competition 2020 , SAT COMPETITION 2020, (2020), p. 29

    work page 2020

  59. [59]

    Stern, A new identification scheme based on syndrome decoding , Springer Berlin Heidelberg, 1994, p

    J. Stern, A new identification scheme based on syndrome decoding , Springer Berlin Heidelberg, 1994, p. 13–21

    work page 1994

  60. [60]

    G. S. Tseitin, On the Complexity of Derivation in Propositional Calculus , Springer Berlin Heidelberg, Berlin, Heidelberg, 1983, pp. 466–483

    work page 1983

  61. [61]

    van de Ven and et al

    A. van de Ven and et al. , Powertop. https://github.com/fenrus75/powertop. Version 2.15

    work page

  62. [62]

    S. Xie, M. Yang, S. A. Lanham, Y. Wang, M. Wang, S. Oruganti, and J. P. Kulkarni, 29.2 Snap-SAT: A One-Shot Energy-Performance-Aware All-Digital Compute-in-Memory Solver for Large-Scale Hard Boolean Satisfiability Problems , in 2023 IEEE International Solid- State Circuits Conference (ISSCC), IEEE, 2023, pp. 420–422

    work page 2023

  63. [63]

    Zhang, F

    X. Zhang, I. Rozada, F. B ¨ohm, E. Valiante, M. Noori, T. Van Vaerenbergh, C.-W. Yang, G. Pedretti, M. Mohseni, and R. Beausoleil, Distributed binary optimization with in-memory computing: An application for the sat problem, arXiv preprint arXiv:2409.09152, (2024)

    work page arXiv 2024

  64. [64]

    C. Zhu, A. C. Rucker, Y. Wang, and W. J. Dally, SatIn: Hardware for boolean satisfiability inference, arXiv preprint 18 arXiv:2303.02588, (2023). 19 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 100 101 Area advantage over CNF M-0 M-1 M-2 M-3 M-4 M-5 M-6 M-7 M-8 M-9 P8-1 P8-2 P8-3 P16-1 P16-2 P16-3 P16-4 P16-5 A-1 A-2 10 3 100 103 Time-to-solution (s)...

    work page arXiv 2023