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

Nature Communications, vol. 17

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.

Authors 15

1. Haesol Im

   1QBit

   Affiliation as printed

   1QB Information Technologies (1QBit), Vancouver, BC, Canada

2. Fabian Böhm
   Affiliation as printed

   HPE Labs, Hewlett Packard Enterprise, Brussels, Belgium

3. Giacomo Pedretti

   Hewlett Packard Enterprise (United States)

   Affiliation as printed

   HPE Labs, Hewlett Packard Enterprise, Milpitas, CA, USA

4. Noriyuki Kushida

   1QBit

   Affiliation as printed

   1QB Information Technologies (1QBit), Vancouver, BC, Canada

5. Moslem Noori

   1QBit

   Affiliation as printed

   1QB Information Technologies (1QBit), Vancouver, BC, Canada

6. Xiangyi Zhang

   1QBit

   Affiliation as printed

   1QB Information Technologies (1QBit), Vancouver, BC, Canada

7. Chuhong Yang

   1QBit

   Affiliation as printed

   1QB Information Technologies (1QBit), Vancouver, BC, Canada

8. Tinish Bhattacharya

   University of California, Santa Barbara

   Affiliation as printed

   University of California, Santa Barbara, CA, USA

9. Jim Ignowski

   Hewlett Packard Enterprise (United States)

   Affiliation as printed

   HPE Labs, Hewlett Packard Enterprise, Milpitas, CA, USA

10. Arne Heittmann

    Forschungszentrum Jülich

    Affiliation as printed

    Peter Grünberg Institute (PGI-14), Forschungszentrum Jülich GmbH, Jülich, Germany

11. John Paul Strachan Aachen

    Forschungszentrum Jülich · RWTH Aachen University

    Affiliation as printed

    Peter Grünberg Institute (PGI-14), Forschungszentrum Jülich GmbH, Jülich, Germany

    RWTH Aachen University, Aachen, Germany

12. Masoud Mohseni

    Hewlett Packard Enterprise (United States)

    Affiliation as printed

    HPE Labs, Hewlett Packard Enterprise, Milpitas, CA, USA

13. Raymond G. Beausoleil

    Hewlett Packard Enterprise (United States)

    Affiliation as printed

    HPE Labs, Hewlett Packard Enterprise, Milpitas, CA, USA

14. Thomas Van Vaerenbergh
    Affiliation as printed

    HPE Labs, Hewlett Packard Enterprise, Brussels, Belgium

15. Ignacio Rozada corresponding

    1QBit

    Affiliation as printed

    1QB Information Technologies (1QBit), Vancouver, BC, Canada. ignacio.rozada@1qbit.com