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

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