基于改进连续时间动态系统的模拟SAT求解器

Analog SAT solver based on improved continuous-time dynamic systems

针对布尔可满足性问题的高效求解进行了研究。首先,通过对k-SAT问题和基于耦合常微分方程形式的确定性连续时间动态系统的分析,提出了一种基于时延信息形式的改进连续时间动态系统方程,以保持集中搜索特性;然后,提出了实现该系统方程的三个主要组件即信号动态电路、辅助变量电路和数字验证电路的模拟设计。在信号动态电路的设计中,设计了一种获得更高性能、更小面积和更低功耗的模拟硬件形式;在提出的辅助变量电路和数字验证电路的模拟硬件设计中,实现了避免梯度下降搜索陷入无解和确定给定问题的解是否已经找到的目标;同时提出了降低面积和功耗的可替代辅助变量电路的两种设计方案。仿真实验结果表明,提出的新的模拟SAT求解器不仅是有效的,而且相比于单一软件算法实现的SAT求解器和其他硬件类SAT求解器具有更高的加速性能和更低的功耗。

This paper studied efficient solving of the Boolean satisfiability problem.Firstly,by analyzing the k-SAT problem and the deterministic continuous-time dynamical system based on the coupled ordinary differential equation form,this paper proposed an improved continuous-time dynamical system equation based on the time-delay information form to maintain the centralized search property.Then,it presented the analog design of three main components,namely,the signal dynamics circuit,the auxiliary variable circuit and the digital verification circuit,to implement the system equation.In the design of signal dynamics circuit,this paper designed a form of analog hardware to obtain higher performance,smaller area and lower power consumption.In the analog hardware design of the proposed auxiliary variable circuit and digital verification circuit,it achieved the goal of avoiding the gradient descent search falling into no solution and determining whether the solution of a given problem has been found.At the same time,it proposed two design schemes of alternative auxiliary variable circuit with reduced area and power consumption.The simulation results show that the proposed new analog hardware SAT solver is not only effective,but also has higher speedup performance and lower power consumption compared with the SAT solver implemented by only software algorithm and other hardware SAT solvers.