布尔可满足性问题（SAT）是计算机科学的核心问题之一，SMT是特定背景下一阶逻辑公式可满足性问题，是对SAT的重要扩展，可以视为命题逻辑框架和背景理论如位向量理论和线性算术理论的结合，可以更方便的表达涉及数学理论和数据结构的约束问题。SAT和SMT是EDA和软件验证的核心引擎。本报告介绍SAT和SMT的主要方法和一些挑战。

报告将以计算机科学领域经典的约束满足问题求解算法为切入点，首先介绍约束满足问题的背景知识以及经典问题实例；此基础上，结合实例介绍约束满足问题求解算法的核心思想，包括搜索策略与约束推理等方面；最后介绍我们近期在约束求解方向上取得的一些研究进展以及思考。

基于SAT求解的模型检查技术是当前该领域的主流，其演变过程主要从早期的高度依赖SAT性能的BMC，K-induction和IMC算法到现今浅度依赖SAT的IC3/PDR和CAR等。然而，以上方法中并没有一个是完全占优的，甚至同一个算法使用不同的参数也会导致验证性能产生很大的差异。近年来研究者的工作主要聚焦于算法的性能提升上，但对导致性能差异的深层次原因关注较少。本报告从介绍模型检查的基本原理开始，分析现今主流技术的差异之处，再根据多年来在该领域的经验提出对模型检查性能的一些初步的可解释性分析，并展示一些最新的结果。

符号执行是一种有效的程序分析方法。符号执行方法将SMT求解器作为黑盒使用，调用一次SMT求解得到一个测试用例，并对应一条执行路径。本课题研究如何将SMT求解过程与路径空间的搜索过程结合起来，将SMT求解器求解的过程视为路径空间的搜索过程。将SMT求解器的求解过程中所产生的“半解”提取出来，作为有用的测试用例，达到“一次求解，生成多个测试用例”的效果。实验表明，本方法能够有效提高符号执行方法的效率。

逻辑是程序语义的基础，SMT求解器是许多程序分析与验证技术的推理引擎。目前，存在多种SMT理论，例如线性算术理论、数组理论、位向量理论、未解释函数理论等。这些理论已经能够很好的支持串行程序验证，但却缺乏直接面向并发程序验证的SMT理论。本报告介绍我们在并发程序SMT理论方面取得的最新研究成果，并介绍相应的求解算法。基于该理论开发的并发程序验证工具Deagle连续两年获得国际软件验证大赛并发安全赛道冠军。

自动化搜索方法在解放密码分析人员劳动力和提升密码算法设计水平方面功不可没，但随着研究的深入，其在诸多搜索任务中的效率问题和准确性问题逐渐成为现阶段制约自动化密码分析方法进一步应用的核心瓶颈。报告主要围绕基于布尔可满足性问题（Boolean Satisfiability Problem, SAT）的自动化搜索方法展开，首先介绍如何优化现有自动化搜索框架以提升搜索效率和精确度，其次介绍基于深度学习的密码分析进展。