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

Area of Science:

• Computer Science
• Electrical Engineering
• Computational Complexity

Background:

• Boolean satisfiability (SAT) is a critical problem in many industries.
• Hybrid XOR-CNF representations offer efficient solutions for specific SAT instances.
• Existing methods often require complex translations, impacting performance.

Purpose of the Study:

• To propose a hardware accelerator architecture for native XOR-CNF SAT problem solving.
• To leverage in-memory computing with memristor crossbar arrays for efficient computation.
• To demonstrate performance improvements over conventional approaches.

Main Methods:

• Developed a novel algorithm for solving hybrid XOR-CNF problems.
• Implemented the algorithm using memristor crossbar arrays for in-memory computing.
• Validated the approach through experimental and simulation-based analysis.

Main Results:

• The proposed accelerator achieved approximately 10x improvement in speed, energy efficiency, and area utilization compared to pure CNF translation.
• Demonstrated a 10x speedup and 1000x energy efficiency gain over state-of-the-art CPU-based SAT solvers.
• Successfully solved hard cryptographic benchmarking problems.

Conclusions:

• Native in-memory computing of XOR-CNF SAT problems offers substantial performance benefits.
• Memristor-based accelerators are a promising solution for computationally intensive SAT problems.
• This approach significantly advances the efficiency of SAT solvers in critical applications.