近日，中国计算机学会（CCF）形式化方法专业委员会公布了2025年度博士学位论文激励计划评选结果，中国科学院工业人工智能研究所可信智能软件团队助理研究员李博涵的博士论文《算术理论SMT问题的局部搜索算法与应用》入选。

《算术理论SMT问题的局部搜索算法与应用》围绕算术理论可满足性模理论（SMT）问题展开研究。SMT求解器作为软件可靠性保障的计算引擎，在软件验证和测试等领域有重要应用。论文提出了首个针对整数算术理论 SMT 问题的局部搜索算法LocalSMT，弥补了该领域的研究空白，并一步将局部搜索技术拓展至实数算术理论。LocalSMT 对可满足算术理论实例的性能达到了国际领先，尤其对非线性算术理论实例的求解性能大幅超过前沿求解器。基于 LocalSMT 算法的求解器在国际 SMT 比赛获得多次冠军，其中包括我国在该赛事的首个冠军。论文将 LocalSMT 应用于终端设备的页面自动布局，支持页面布局的“一次开发，多端部署”，并实现毫秒级响应。该项目获得华为“鸿蒙创新大赛” 冠军，并被华为确定为鸿蒙系统的新特性。

“博士学位论文激励计划”由CCF专业委员会设立，旨在进一步推动软件领域高水平创新人才培养工作。评选采用推荐-评审制，由单位推荐或CCF会员联名推荐候选博士学位论文，各专业委员会组建的该计划评审委员会组织评审，评选过程具体包括推荐、资格审查、初评、终评四个阶段。各专业委员会每年评选出不超过3篇，在相关领域做出杰出创新研究工作的博士学位论文，对论文完成人给予表彰和奖励。