知识表示和自动推理是人工智能领域的核心挑战,命题逻辑作为知识表示的一般方法,为定理证明提供了理论支撑,为计算机程序提供了验证、编译、可靠性分析。SAT求解器对提高命题逻辑问题可处理性做出了重要贡献,并在实际应用中取得显著成果。本文基于命题逻辑对SAT求解器中的相关策略展开研究,提出基于决策层的混合分支启发式策略和基于简化活性的学习子句集成管理策略,分别嵌入以CDCL(ConflictDriven Clause Learning)框架为核心的SAT求解器,具体成果如下:1、在变量的分支决策环节,变量赋值决策层和当前决策层被用于决策评估。一方面,对参与冲突分析的变量,提出了基于决策层的VSIDS＿dl(Variable State Independent Decaying Sum＿Decision Level)启发式策略;另一方面,对回溯过程中取消赋值的变量,根据强化学习,将回溯层次差作为学习率增量的一部分,提出了基于决策层的LRB＿dl(Learning Rate-based Branching＿Decision Level)启发式策略。并以分段式和交替式混合上述两种启发式策略,嵌入三个求解器中,形成对应的混合型分支启发式策略求解器,进行对比实验。结果表明,在求解图着色和平面色数问题时,基于决策层的交替式混合分支启发式策略在Maple COMSPS求解系统中显现出求解优势。2、在学习子句管理中,针对学习子句活跃值的计算复杂性和局限性,提出基于简化活性的学习子句评估标准。通过排序和标记的方法将其嵌入Maple LCMDist Chrono BT求解器中,实现了对全局学习子句参与冲突分析次数的简易评估和数据存储。实验结果表明:基于简化活性排序的集成管理策略能提高求解器的求解速率,基于简化活性标记的集成管理策略能解出部分原求解器无法求解的问题。