在计算机科学中,布尔可满足性问题(有时称为命题满足性问题或SAT问题)是确定是否存在一个问题的解,其满足给定的布尔公式。换句话说,它判断给定的布尔公式的变量是否可以赋予真值TRUE或FALSE,使得给定的布尔公式最后的结果为TRUE。如果最后的结果是TRUE,那我们就称该公式被为可满足。另一方面,如果不存在这样的分配,即对于所有可能的变量分配,由该公式表示的结果为FALSE,那么就称该公式不可满足。SAT是第一个被证明是NP完全的问题。这意味着复杂等级NP中的所有问题(包括广泛的自然决策和优化问题)与SAT一样难以解决。没有已知的算法可以有效地解决每个SAT问题,并且通常认为不存在这样的算法,但是这种信念尚未在数学上证明。该技术是当代理论计算机科学研究的核心问题之一。GPU适用于大规模数据并行处理,具有很高的计算性价比,且在通用计算领域有广泛应用。本文面向大规模问题的求解需求,研究基于GPU的可满足性求解技术。由于已有求解器算法具有较强的控制依赖关系,是公认的难以被直接映射至的算法之一。本文分两步对问题进行求解。第一步:首先进行非精确求解过程,这一过程使用的是遗传算法和模拟退火算法相互结合的算法,通过使用这一混合算法,从解空间中找出十分靠近准确解的非准确的解;第二步:将得到的非精确解作为输入解,对此解进行精确求解,这一过程使用的算法是DPLL算法,通过DPLL算法得到满足问题的精确解,从而解决问题。在基于局部搜索的非精确求解技术中,为可满足性求解问题建立数学优化模型,我们将模拟退火算法和遗传算法结合起来,基于GPU实现了细粒度并行化,从而高效收敛到局部最优解。在基于DPLL的精确求解过程中,以非精确求解中局部搜索所得到的非精确解,作为所选择变量的赋值参考,再以传统精确求解方式进行求解,从而得到最终解。