约束求解：软硬件系统可信保障之魂 | CCF数图焦点第67期

约束求解是计算机科学的一个核心技术，也是符号主义AI的代表性技术，主要研究布尔可满足性（SAT）、可满足性模理论（SMT）、约束规划（CP）以及数学规划等约束模型的判定和优化问题的建模与求解算法。

约束求解领域经过长期发展，形成了高效的求解器，是电子设计自动化（EDA）、软件测试与验证、密码分析、能源调度等领域的基础引擎，也是多种工业软件的核心部件，对国家经济和社会发展具有重要影响。近些年来，复杂需求对约束求解技术提出了更高的挑战，约束求解与强化学习和大模型技术的结合也引起了越来越多关注，而同时学术界也在期待约束求解器的理论分析有本质突破。

本次专题聚焦约束求解及其应用，将CCF数字图书馆相关资源以及其他平台与选题相关的资源进行聚合，方便会员集中观看学习，也为读者探索约束求解与计算机其他领域的交叉融合抛砖引玉。

点击“阅读原文”浏览《CCF数图焦点》第67期详细内容。