Cılasun Hüsrev, Zeng Ziqing, S Ramprasath, Kumar Abhimanyu, Lo Hao, Cho William, Moy William, Kim Chris H, Karpuzcu Ulya R, Sapatnekar Sachin S
University of Minnesota, Minneapolis, USA.
Indian Institute of Technology Madras, Chennai, India.
Sci Rep. 2024 May 10;14(1):10757. doi: 10.1038/s41598-024-60316-y.
This work solves 3SAT, a classical NP-complete problem, on a CMOS-based Ising hardware chip with all-to-all connectivity. The paper addresses practical issues in going from algorithms to hardware. It considers several degrees of freedom in mapping the 3SAT problem to the chip-using multiple Ising formulations for 3SAT; exploring multiple strategies for decomposing large problems into subproblems that can be accommodated on the Ising chip; and executing a sequence of these subproblems on CMOS hardware to obtain the solution to the larger problem. These are evaluated within a software framework, and the results are used to identify the most promising formulations and decomposition techniques. These best approaches are then mapped to the all-to-all hardware, and the performance of 3SAT is evaluated on the chip. Experimental data shows that the deployed decomposition and mapping strategies impact SAT solution quality: without our methods, the CMOS hardware cannot achieve 3SAT solutions on SATLIB benchmarks. Under the assumption of some hardware improvements, our chip-based 3SAT solver demonstrates a remarkable 250 acceleration compared to Tabu search in dwave-hybrid on a CPU.
这项工作在具有全连接性的基于CMOS的伊辛硬件芯片上解决了3SAT这一经典的NP完全问题。本文探讨了从算法到硬件过程中的实际问题。它考虑了将3SAT问题映射到芯片时的几个自由度，即使用3SAT的多种伊辛公式；探索将大问题分解为可在伊辛芯片上处理的子问题的多种策略；以及在CMOS硬件上执行这些子问题的序列以获得更大问题的解决方案。这些在一个软件框架内进行评估，结果用于确定最有前景的公式和分解技术。然后将这些最佳方法映射到全连接硬件上，并在芯片上评估3SAT的性能。实验数据表明，所采用的分解和映射策略会影响SAT解决方案的质量：没有我们的方法，CMOS硬件无法在SATLIB基准测试中实现3SAT解决方案。在一些硬件改进的假设下，我们基于芯片的3SAT求解器与CPU上的dwave - hybrid中的禁忌搜索相比，实现了显著的250倍加速。
