Medusa: A Quantum-Inspired 200-Variable 1016-Clause Analog k-SAT Solver

📋 论文概要

提出了一种量子启发式模拟变量k-SAT求解器Medusa，支持最多200个变量和1016个子句，通过make/break反馈、分布式k-SAT逻辑等关键技术，在28nm CMOS工艺上实现了高能效和高速度的布尔可满足性求解，解决了传统数字求解器能耗高、速度慢的问题。

💡 主要创新点

• 采用量子启发的模拟计算范式，结合make/break反馈机制实现高效搜索空间遍历。
• 提出分布式k-SAT逻辑和数字宏耦合技术，大幅提升变量规模与子句处理能力。
• 通过反馈优化算法，在确保100%可解性和准确性的前提下，显著降低平均求解时间和能耗。

🏷 关键词

📄 原文摘要

Abstract A quantum-inspired analog variable k-SAT solver supporting up to 200 variables and 1016 clauses. Enabling techniques include make/break feedback, distributed k-SAT logic, digital macro coupling, and feedback optimization. The 28nm CMOS prototype achieves a 4.92µs mean solution time and a 19.1nJ mean energy consumption for 50-variable 3-SAT problems with 100% solvability and accuracy, representing 3.5× and 3× improvements in energy and solution time respectively, compared to the state-of-the-art. Boolean satisfiability (SAT or k-SAT, k 3) problems are essential combinatorial optimization problems (COPs) for artificial intelligence [1], drug discovery [2], scheduling, and automated design [3]. SAT problems solve for binary variables such that all clauses are true, with each clause comprising variables or their negations (e.g., x1 v ¬x2 v x3). However, SAT problems are NP-Complete, making them difficult for conventional computing.

👥 作者与机构

Luke D. Wormald, Ying-Tuan Hsu, Evangelos Dikopoulos, Wei Tang, Benjamin Datsko, Ali Hammoud, Zhengya Zhang, Michael P. Flynn

University of Michigan, Ann Arbor, MI