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

来源：计算机工程与科学杂志2021年第12期北京时间：

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

单位：（国防科技大学计算机学院，湖南 长沙 410073）

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

关键词：布尔可满足,FPGA,不完全算法,多线程,

基金资助：国家自然科学基金(62072464,U19A2062);并行与分布处理国家级重点实验室开放基金(WDZC20205500116)