EAGER: An Analog Hardware System for Solving Boolean Satisfiability

该提案探讨了一种低功耗和高性能的模拟硬件系统的设计，能够解决布尔可满足性（SAT）问题，这是许多决策，调度，纠错和网络安全应用的核心。由于SAT属于计算机科学中著名的难决策问题家族，因此有效的解决方案将对所有计算科学，工程和社会应用产生深远的影响。该项目建立在理论家和硬件设计师之间的密切合作的基础上，为传统上在这方面几乎没有交集的研究领域创造了交叉授粉的机会。该项目将允许PI将新的研究发现纳入相关课程，并为本科生和研究生提供研究机会，包括来自代表性不足群体的学生。这项拟议的努力将研究潜在的模拟硬件的基础上，一些相关的确定性连续时间动态系统（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.