判定布尔公式的可满足性（SAT）是计算机科学领域经典的NP完全问题之一,由于众多领域的实际问题都可以转换为布尔可满足问题来求解,例如VLSI设计与验证、软件的形式验证、人工智能规划与优化等领域,因此几十年来一直是计算机理论领域的研究热点。近年来,随着布尔可满足求解技术的不断发展,软件实现的SAT求解器也逐渐走向成熟与完善,但针对某些类型的SAT实例,例如复杂3-SAT实例,存在学习时间长、求解效率不高等问题。而基于局部搜索原理、通过硬件加速的SAT求解技术是提高3-SAT求解效率最有效的手段,因此,基于硬件加速的SAT求解技术也得到了飞速发展,成为验证领域的研究热点。近年来,致力于改进基于随机局部搜索原理的SAT求解技术得到了广泛、深入的研究。然而,随机局部搜索求解技术在总体上仍有很高的改进潜力,尤其是在结构化SAT问题的求解上存在不足。因此,本文主要目标是寻找新的基于可编程逻辑器件的实现方法,以便更高效、更全面的求解不同类型的3-SAT问题,特别是随机类的3-SAT实例。通过以下几个步骤实现该目标:研究对随机局部搜索求解器初始赋值行为的新分析方法,分析适合随机局部搜索求解器的预处理技术,设计新的单线程的随机局部搜索硬件求解器,以及设计一个并行多线程的随机局部搜索硬件求解器。首先分析了传统随机局部搜索求解器对问题所有变元的初始赋值方式,提出了在局部搜索方法中,使用一种计算变元初始指派取正的概率Pi的SAT预处理算法。通过对参数取值的约束,使得当变元为正的子句的个数大于为负的子句的个数时,其初始指派取正的概率更大,否则,则减小此概率。此外,算法对传统随机产生的变元初始赋值策略进行了改进,尽量使初始指派后产生的可满足子句更多,提前指导了最优真值指派搜索的趋势,大大提高问题的收敛速度,减少搜索陷入局部最优的现象发生。这种对问题变元初值赋值的计算策略结构简单,算法可移植性强,可以用于任何随机局部搜索求解器中。提出基于加强约束算法的现场可编程门阵列（FPGA）求解器ECWSAT,并将基于概率的变元赋值预处理技术应用于此求解器。ECWSAT求解器中软件预处理由主机在求解开始前完成,利用变元消除策略对原始的DIMACS格式的数据进行化简,在计算变元初始赋值为正的概率后给所有变元赋初值,并根据当前初值提取对应的数据文件,如不可满足子句、地址映射表、子句映射表等,最后将这些数据文件下载到硬件求解器中。在主程序部分,对算法的变元选择启发式进行了改进。此外,为了避免搜索陷入局部最优,算法引入一个噪声扰动机制,当搜索进入局部最优时,允许算法按照一定策略选择和当前候选解相同质量或者次质量的解,使其进入不同的优化方向,从而跳出局部最优。实验结果表明,与软件SAT求解器WalkSAT以及其他同类型的硬件SAT求解器相比,ECWSAT求解器可有效的求解规模相对较大的随机SAT问题,特别是在难的随机问题上表现出了良好的性能。提出了基于概率分布函数的probSAT+硬件求解器,用于求解ECWSAT在求解某些大规模的实例成功率不高的问题。probSAT+硬件求解器的核心是一个基于概率分布函数的决策启发式算法。提出的算法在以下三个方面做了改进:首先,在预处理阶段,使用纯文字的化简规则确定符合条件变元的初值;其次,对变元的初始赋值策略做了约束,通过提前指导最优真值指派搜索的趋势,使得赋值后可满足子句尽可能多,减少搜索过程中的翻转次数和搜索的解空间,进而减少陷入局部最优情况的发生,加快算法的收敛速度;最后,在计算变元的概率分布函数时,提出了一种适应于硬件平台实现的概率求解方案,避免了在FPGA中进行复杂的指数或者多项式计算,从而减少了因此带来的巨大时间和面积开销。实验结果表明,与业界高效的同类型软件SAT求解器WalkSAT与Sparrow相比,probSAT+取得了较大的加速比,求解效率得到了显著提升。提出了基于不完全算法的并行多线程求解器pprobSAT+,以提高求解器在搜索过程中的吞吐率,增强求解器的处理能力。求解器基于probSAT+的算法框架,着重分析了求解器的主要组件及其相互作用,并对求解器并行多线程处理过程以及系统流水线带来的性能增益做了详细说明。pprobSAT+求解器在每次搜索的过程中,算法并不判断所有的子句的最终结果,而是仅仅对可能改变的子句进行评估,换句话说,算法仅评估包含翻转变元的子句,从而很大程度上节省了硬件资源开销。此外,由于使用了流水线设计,多个独立的线程被同时执行,使得并行和流水线电路具有很高的求解性能。当实例规模较小,并且所有的数据都存储在FPGA片上存储器时,pprobSAT+求解器能获得更高的性能与加速比。若能将部分数据存于片外存储器,则能大大提高求解器处理问题的规模。实验结果表明,pprobSAT+能够正确地判定公式的可满足性;并且与单线程probSAT+求解器相比,3线程pprobSAT+求解器能够达到超过2倍的加速比。