布尔可满足性(简称SAT)问题已被广泛运用于程序复杂度分析、程序验证和人工智能等各个方面以解决相关实际问题。模块可满足性理论(简称SMT)通过将SAT约束和模块理论约束相结合,在实际问题中,其表达能力比SAT理论更强。尽管SAT/SMT理论在实际中得到了较为广泛的应用,但当实际问题过于复杂时,SAT/SMT理论的求解效率将大幅降低,影响了SAT/SMT理论的可用性。为了解决上述问题,本文提出了一种基于求解器返回信息的SAT/SMT公式关键变量快速求解的新方法,该方法以公式的结构和求解器的返回结果为基础,对关键变量的特征进行分析,设计并实现了SAT/SMT公式关键变量的计算框架。通过理论分析和实验比较,说明所提出的计算方法和计算框架能够快速求解SAT公式的所有可行解和神经网络的对抗样本,提高了复杂情况下SAT/SMT的求解效率,增强了SAT/SMT理论的实用性。主要创新性如下:(1)研究并提出一个新的SAT公式关键变量求解框架。框架分析SAT公式关键变量的性质,并基于性质设计和实现了一个快速求解SAT公式关键变量的计算框架。框架能够迭代的得到更多的关键变量和非关键变量。实验表明,与已有的SAT公式求解关键变量的算法相比,本文所提出的新框架能够提高15%的求解效率。(2)基于SAT公式关键变量,研究并提出SMT公式关键变量的求解方法。对于一个SMT公式F,先计算其相应SAT公式的关键变量信息,根据所得到的SAT公式关键变量信息,计算得到部分SMT公式关键变量。本文将SMT公式拆解为SMT约束,并使用SMT求解器优化策略计算对于关键变量x的最大可行取值范围。与已有的方法相比,本文提出的方法需要的全称量词约束求解次数更少,提高了SMT求解器的求解效率。实验表明,由于本文提出的方法能够减少SMT求解次数,因此减少了SMT关键变量的求解时间,提高了SMT关键变量的求解效率,与已有的方法相比,本方法能够提高17%的求解效率。(3)基于SAT公式关键变量,研究并提出一种高效的SAT公式全解的求解方案。通过将已知的SAT公式可行解转换为屏蔽子句加入到SAT公式中,能够计算得到SAT公式的所有可行解。与已有的方法相比,本文使用SAT公式的关键变量,将SAT公式的多个可行解合并为一个更短的约束,并加入到原SAT公式中,以减少新加入的约束数量,缩小新的SAT公式的规模;并通过将关键变量作为单元子句加入到原公式的方式,加速SAT求解器的求解速度。实验表明,本文所提出的方法能够快速有效的计算SAT公式的全解,与已有的方法相比,本方法能够提高27%的求解效率。(4)基于SMT公式关键变量,研究并提出一个快速求解神经网络对抗样本的工具。神经网络的对抗样本能够提高神经网络的可靠性,本文使用SMT公式关键变量求解神经网络的对抗样本,是一种对神经网络进行验证的方法。本文首先将神经网络编码为SMT公式,找到与计算对抗样本相关的关键变量,并计算其最大可行取值范围r;然后使用区间分析法(Interval Analysis)计算该变量在给定的神经网络输入变换范围内的取值范围r~′,若r小于r~′,则当该关键变量的取值在r~′范围内但不在r范围内时,该神经网络一定存在一个对抗样本;最后根据关键变量的最大可行取值范围的计算结果设计梯度下降方法中的目标函数,并使用梯度下降法计算得到当前输入样本的一个对抗样本。实验表明,与已有的方法相比,本文所提出的方法能够找到更多的对抗样本。