计算机应用研究2024，Vol.41Issue(1)：200-205,6.DOI:10.19734/j.issn.1001-3695.2023.04.0189
基于改进连续时间动态系统的模拟SAT求解器
Analog SAT solver based on improved continuous-time dynamic systems
摘要
Abstract
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 dy-namics circuit,this paper designed a form of analog hardware to obtain higher performance,smaller area and lower power con-sumption.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 al-gorithm and other hardware SAT solvers.关键词
布尔可满足性问题/连续时间动态系统/模拟设计/辅助变量/数字验证/加速性能Key words
Boolean satisfiability problem/continuous-time dynamical system/analog design/auxiliary variables/digital verification/speedup performance分类
信息技术与安全科学引用本文复制引用
赵海军,陈华月,崔梦天..基于改进连续时间动态系统的模拟SAT求解器[J].计算机应用研究,2024,41(1):200-205,6.基金项目
四川省自然科学基金资助项目(2022NSFSC0536) （2022NSFSC0536）
国家自然科学基金资助项目(12050410248) （12050410248）
