基于不完全算法的并行FPGA SAT求解器

作者：黎铁军; 马柯帆; 张建民

来源：计算机工程与科学, 2021, 43(12): 2126-2130.

• 布尔可满足
• FPGA
• 不完全算法
• 多线程

可满足性问题是计算机理论与应用的核心问题。在FPGA上提出了一个基于不完全算法的并行求解器pprobSAT+。使用多线程的策略来减少相关组件的等待时间,提高了求解器效率。此外,不同线程采用共用地址和子句信息的数据存储结构,以减少片上存储器的资源开销。当所有数据均存储在FPGA的片上存储器时,pprobSAT+求解器可以达到最佳性能。实验结果表明,相比于单线程的求解器,所提出的pprobSAT+求解器可获得超过2倍的加速比。

• 单位
  国防科技大学