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

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

A parallel FPGA SAT solver based on incomplete algorithm

The Boolean satisfiability (SAT) problem is the key problem in computer theory and application. his paper proposes a parallel SAT solver based on incomplete algorithm on FPGA. The algorithm uses a multi-threaded strategy to reduce the waiting time of related components and improve the efficiency of the solver. In addition, different threads use data storage structures that share addresses and clause information to reduce the resource overhead of on-chip memory. When all data is stored in the FPGA’s on-chip memory, the solver can achieve the best performance. The experimental results show that, compared with the single-threaded solver, the solver proposed in this paper can achieve a speedup of more than 2 times.