EAGER: An Analog Hardware System for Solving Boolean Satisfiability

本提案探讨了一种低功耗和高性能模拟硬件系统的设计，能够解决布尔可满足性（SAT）问题，这是许多决策，调度，纠错和网络安全应用的核心。由于SAT属于计算机科学中众所周知的困难决策问题，因此有效的解决方案将对所有计算科学，工程和社会应用产生深远的影响。该项目建立在理论家和硬件设计师之间的密切合作基础上，为传统上在此背景下几乎没有交集的研究领域创造了交叉授粉的机会。该项目将允许pi将新的研究发现纳入相关课程，并为本科生和研究生提供研究机会，包括那些来自代表性不足群体的学生。这项工作将研究基于耦合常微分方程形式的一些相关的确定性连续时间动力系统（CTDS）的模拟硬件的潜力，这些系统最近被引入到SAT问题的研究中。CTDS对能量函数进行梯度下降，能量函数本身随时间变化，通过指数驱动的辅助变量与动力学性能相耦合。该项目将系统地研究基于CTDS的模拟硬件SAT求解器在性能和能效方面是否优于数字SAT求解器，以及在多大程度上优于数字SAT求解器。它也将促进对硬件诱发噪声对模拟SAT求解器影响的理解。综上所述，本项目试图深入了解模拟求解器的非线性动力系统特性与约束满足问题的计算硬度之间的关系，从而为CTDS求解器和SAT求解器的模拟硬件设计奠定基础。

This proposal explores the design of a low-power and high-performance analog hardware system capable of solving Boolean Satisfiability (SAT) problem which is at the heart of many decision, scheduling, error-correction and cyber security applications. Since SAT belongs to a well-known family of hard decision problems in computer science, an efficient solution would have a profound impact in all of computational sciences, engineering, and societal applications. The project builds on close collaborations among theoreticians and hardware designers to create opportunities to cross-pollinate research areas that traditionally have had little intersection in this context. The project will allow the PIs to incorporate new research discoveries into relevant coursework, and offer research opportunities for undergraduate and graduate students, including those from underrepresented groups. This proposed effort will study the potential of analog hardware based on some related deterministic Continuous Time Dynamical System (CTDS) in the form of coupled ordinary differential equations, which have been recently introduced for the study of the SAT problem. The CTDS performs gradient descent on an energy function, which itself changes in time, coupled to the performance of the dynamics through exponentially driven auxiliary variables. The project will study systematically the question of whether and by how much a CTDS based analog hardware SAT solver can outperform digital SAT solvers in terms of performance and energy efficiency. It will also advance the understanding of the impact of hardware induced noises on analog SAT solvers. In summary, the project attempts to provide insights into the relationship between the nonlinear dynamical system properties of the analog solver and the computational hardness of constraint satisfaction problems, and thus lay the foundation for analog hardware designs for CTDS solvers, as well as that for SAT solvers.