计算机应用研究

作者：赵海军,陈华月,崔梦天,

单位：1.西华师范大学计算机学院,四川南充637009；2.西南民族大学计算机科学与工程学院,成都610041；

关键词：布尔可满足性问题,连续时间动态系统,模拟设计,辅助变量,数字验证,加速性能,

基金：四川省自然科学基金资助项目(2022NSFSC0536)；国家自然科学基金资助项目(12050410248)；；

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

来源：2024年第1期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2024年第1期