3SAT on an all-to-all-connected CMOS Ising solver chip

Area of Science:

• Quantum Computing
• Computer Science
• Hardware Acceleration

Background:

• The 3-Satisfiability (3SAT) problem is a classical NP-complete problem with significant computational challenges.
• Solving large-scale NP-complete problems efficiently requires novel hardware and algorithmic approaches.

Purpose of the Study:

• To demonstrate the feasibility of solving the 3SAT problem on a CMOS-based Ising hardware chip.
• To develop and evaluate effective strategies for mapping 3SAT instances to the Ising hardware, including problem decomposition.

Main Methods:

• Utilized a CMOS-based Ising hardware chip with all-to-all connectivity.
• Developed and assessed multiple Ising formulations for 3SAT.
• Explored various strategies for decomposing large 3SAT problems into smaller subproblems manageable by the chip.
• Implemented a software framework to evaluate different mapping and decomposition techniques.
• Executed optimized approaches on the hardware to solve 3SAT instances.

Main Results:

• The developed decomposition and mapping strategies are crucial for achieving 3SAT solutions on the CMOS hardware; without them, solutions were not possible on SATLIB benchmarks.
• The chip-based 3SAT solver demonstrated a 250x acceleration compared to Tabu search in dwave-hybrid on a CPU, assuming certain hardware improvements.

Conclusions:

• Effective mapping and decomposition techniques are essential for leveraging Ising hardware for complex computational problems like 3SAT.
• CMOS-based Ising hardware shows promise for accelerating solutions to NP-complete problems, with potential for significant performance gains over classical algorithms.