EAGER: An Analog Hardware System for Solving Boolean Satisfiability

该方案探索了一种能够解决布尔可满足性(SAT)问题的低功耗和高性能模拟硬件系统的设计，该问题是许多决策、调度、纠错和网络安全应用的核心。由于SAT属于计算机科学中众所周知的一类困难决策问题，因此一个有效的解决方案将对所有计算科学、工程和社会应用产生深远的影响。该项目建立在理论家和硬件设计师之间密切合作的基础上，以创造机会对传统上在这一背景下几乎没有交叉的研究领域进行交叉授粉。该项目将允许私人投资机构将新的研究发现纳入相关课程，并为本科生和研究生提供研究机会，包括那些来自代表性不足群体的学生。这项拟议的工作将基于一些相关的确定性连续时间动态系统(CTDS)来研究模拟硬件的潜力，这些系统以耦合常微分方程组的形式出现，最近被引入用于研究SAT问题。CTDS对能量函数执行梯度下降，该能量函数本身随时间变化，并通过指数驱动的辅助变量与动力学性能相结合。该项目将系统地研究基于CTDS的模拟硬件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.