约束求解是计算机科学的一个核心技术，也是符号主义AI的代表性技术，主要研究布尔可满足性（SAT）、可满足性模理论（SMT）、约束规划（CP）以及数学规划等约束模型的判定和优化问题的建模与求解算法。
约束求解领域经过长期发展，形成了高效的求解器，是电子设计自动化（EDA）、软件测试与验证、密码分析、能源调度等领域的基础引擎，也是多种工业软件的核心部件，对国家经济和社会发展具有重要影响。近些年来，复杂需求对约束求解技术提出了更高的挑战，约束求解与强化学习和大模型技术的结合也引起了越来越多关注，而同时学术界也在期待约束求解器的理论分析有本质突破。
本次专题聚焦约束求解及其应用，将CCF188体育投注相关资源以及其他平台与选题相关的资源进行聚合，方便会员集中观看学习，也为读者探索约束求解与计算机其他领域的交叉融合抛砖引玉。
编委主任：苏金树 CCF会士 军事科学院教授
本期主编：蔡少伟 中国科学院软件研究所研究员
符号执行是一种有效的程序分析方法。符号执行方法将SMT求解器作为黑盒使用，调用一次SMT求解得到一个测试用例，并对应一条执行路径。本课题研究如何将SMT求解过程与路径空间的搜索过程结合起来，将SMT求解器求解的过程视为路径空间的搜索过程。将SMT求解器的求解过程中所产生的“半解”提取出来，作为有用的测试用例，达到“一次求解，生成多个测试用例”的效果。实验表明，本方法能够有效提高符号执行方法的效率。
基于SAT求解的模型检查技术是当前该领域的主流，其演变过程主要从早期的高度依赖SAT性能的BMC，K-induction和IMC算法到现今浅度依赖SAT的IC3/PDR和CAR等。然而，以上方法中并没有一个是完全占优的，甚至同一个算法使用不同的参数也会导致验证性能产生很大的差异。近年来研究者的工作主要聚焦于算法的性能提升上，但对导致性能差异的深层次原因关注较少。本报告从介绍模型检查的基本原理开始，分析现今主流技术的差异之处，再根据多年来在该领域的经验提出对模型检查性能的一些初步的可解释性分析，并展示一些最新的结果。
报告将以计算机科学领域经典的约束满足问题求解算法为切入点，首先介绍约束满足问题的背景知识以及经典问题实例；此基础上，结合实例介绍约束满足问题求解算法的核心思想，包括搜索策略与约束推理等方面；最后介绍我们近期在约束求解方向上取得的一些研究进展以及思考。
