布尔可满足性问题（Boolean Satisfiability Problem,SAT）是一个经典的判定问题,也是历史上首个被证实的NP问题。很多现实问题被证明可以转换为SAT问题去求解,例如人工智能中的轨迹规划和资源调度、集成电路中的模型检测和等价性验证等,因此,SAT问题一直是理论计算机科学领域中的研究重点。随着求解SAT问题的技术不断提高,软件求解器的发展已经趋于成熟,并具有非常优越的性能,但依然难以有效求解某些类型的SAT实例。而集成电路技术的不断发展也促进了硬件求解器的进步,基于硬件的求解方式虽然在复杂算法的实现上具有一定的局限性,但是它可以充分利用硬件平台的特点和资源,对算法的部分模块进行并行化的处理,以此设计可重构硬件SAT求解器。针对两种求解器的特点,本文结合应用型求解方式进行SAT硬件求解器的设计。首先,在传统DPLL算法的基础上加入随机排序和随机赋值策略,以此提高平均求解速度。采用异步控制机制,设计高性能可重构双链电路,用于控制DPLL算法的前进和回溯。使用布尔约束传播技术来加速变量的推导过程,通过分析蕴含推理的原理,编写解析器自动生成不同SAT问题的蕴含公式,提高求解效率。其次,针对目前软硬件协同处理机制中主-协处理器同步困难、通信时间较长等问题,采用将处理器系统与现场可编程门阵列相结合的ZYNQ平台进行设计,将与具体SAT问题无关的模块放在硬件上并行加速,与具体SAT问题相关的模块放在软件上便于修改配置,CPU与FPGA之间通过AXI总线进行通信,最后设计实现了一个基于软硬件运行时协同计算的SAT求解器。由于本文设计的硬件部分是一个最多可求解200个变量的可重构计算架构,求解具体SAT问题时只需要在软件部分进行配置即可,从而避免了为每个SAT实例进行耗时的FPGA综合、布局布线等步骤。通过测试大量的SAT实例,并与软件求解器的求解结果进行对比,证明了该求解器的正确性。