可满足性问题作为软件漏洞挖掘领域的的基础性理论问题,对检测软件漏洞、保证软件安全性具有重大的意义。现代社会复杂的软件环境对可满足性问题的求解速度提出了更高的要求。本文基于高性能众核ARM平台,研究了面向可满足性问题的并行优化技术。对于SMT问题的Boolector求解器,我们采用粗粒度并行的方法,利用ARM平台单核计算能力较强且核心数较多的优势提高求解器的吞吐率,我们还针对数据的调度采用了静态调度、动态调度、以及我们提出的基于时间排序的动态调度策略,最终我们在ARM平台获得了优于主流通用X86平台3.63倍的加速比。对于SAT问题的Minisat求解器,我们同时采用了粗粒度与细粒度并行两种并行方法,其中粗粒度并行主要用于提高吞吐率,细粒度并行主要用于缩短长尾效应,平衡线程负载。此外,我们还利用时间预测模型提前预测求解实例的大致运行时间,从而能根据运行时间对输入数据集进行排序,进而充分发挥基于时间排序的动态调度策略的优化效果。在测试中,我们在ARM平台上获得了优于主流通用X86平台3.46倍的加速比。