黎铁军，马柯帆，张建民

(国防科技大学计算机学院，湖南 长沙 410073)

1 引言

可满足性问题SAT(SATisfiability problem)作为最著名的NP完全NPC(Non-deterministic Polynomial Complete)问题之一，被广泛应用于理论研究和实践领域。许多困难的组合问题，包括硬件与软件的形式化验证、人工智能、运筹学、计算生物学、密码学、数据挖掘和机器学习等方向出现的问题，都可以用基于SAT的技术来解决。自从关于在可重构硬件上实现SAT求解器的综述[1]发表以来，基于硬件的SAT求解器获得了飞速的发展。最坏情况下，SAT问题求解时间呈指数增加，因此，近年来针对如何利用FPGA固有的灵活性和并行性高效求解SAT问题成为业界研究的热点。

SAT问题求解的最终目的是获得高效正确的判定。SAT求解器在不断追求高效算法的同时，不可避免地会遇到一些问题[2]。对软件求解器来说，一些求解器尽管性能优异，但求解算法过于复杂，研究人员需要大量专业知识去理解概念的正确性和算法运行机制。一些已经解决的问题或许还存在更优的求解方法。此外，一些求解器一味地追求其性能而忽视了算法的完备性，甚至正确性。对硬件求解器来说，软件求解器中新的启发式和数据结构的应用对硬件SAT求解器的加速策略作出了显著贡献。然而，尚不清楚硬件SAT求解方案的总体进展是否跟上了日益复杂和高效的软件求解器的快速进步。基于硬件的SAT求解器仍面临诸多挑战[3]。

本文重点研究了基于随机局部搜索SAT求解器的算法与实现，提出了基于FPGA的并行多线程求解器pprobSAT+。……