Accelerating Hybrid XOR$-$CNF Boolean Satisfiability Problems Natively with In-Memory Computing
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916014408597504 |
|---|---|
| author | Im, Haesol Böhm, Fabian Pedretti, Giacomo Kushida, Noriyuki Noori, Moslem Valiante, Elisabetta Zhang, Xiangyi Yang, Chan-Woo Bhattacharya, Tinish Sheng, Xia Ignowski, Jim Heittmann, Arne Strachan, John Paul Mohseni, Masoud Beausoleil, Ray Van Vaerenbergh, Thomas Rozada, Ignacio |
| author_facet | Im, Haesol Böhm, Fabian Pedretti, Giacomo Kushida, Noriyuki Noori, Moslem Valiante, Elisabetta Zhang, Xiangyi Yang, Chan-Woo Bhattacharya, Tinish Sheng, Xia Ignowski, Jim Heittmann, Arne Strachan, John Paul Mohseni, Masoud Beausoleil, Ray Van Vaerenbergh, Thomas Rozada, Ignacio |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_06476 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Accelerating Hybrid XOR$-$CNF Boolean Satisfiability Problems Natively with In-Memory Computing Im, Haesol Böhm, Fabian Pedretti, Giacomo Kushida, Noriyuki Noori, Moslem Valiante, Elisabetta Zhang, Xiangyi Yang, Chan-Woo Bhattacharya, Tinish Sheng, Xia Ignowski, Jim Heittmann, Arne Strachan, John Paul Mohseni, Masoud Beausoleil, Ray Van Vaerenbergh, Thomas Rozada, Ignacio Emerging Technologies Hardware Architecture Optimization and Control 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. |
| title | Accelerating Hybrid XOR$-$CNF Boolean Satisfiability Problems Natively with In-Memory Computing |
| topic | Emerging Technologies Hardware Architecture Optimization and Control |
| url | https://arxiv.org/abs/2504.06476 |