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

作者：赵海军^*; 陈华月; 崔梦天

来源：计算机应用研究, 2023, 1-7.

DOI：10.19734/j.issn.1001-3695.2023.04.0189

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

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

• 单位
  西南民族大学; 西华师范大学