近日，中国科学院公布了2025年度中国科学院优秀博士学位论文评审结果，中国科学院软件研究所2024届毕业生张昕荻博士的学位论文入选，其指导教师蔡少伟研究员荣获2025年度“中国科学院优秀导师”称号。

张昕荻，2018年进入软件所学习，2020年转为博士生，其博士学位论文《SAT和SMT问题的混合求解算法及应用》聚焦于命题逻辑可满足性问题（SAT）、可满足性模理论问题（SMT）的混合求解算法，及其若干应用问题。相关工作获SAT会议“最佳论文奖”、国际SAT、SMT、FLoC（国际逻辑学联合会议）竞赛冠军十余次、“强网杯”密码数学挑战赛全国冠军等。

论文创新性提出了一个以系统搜索为主体，局部搜索为辅的深度混合求解框架，大幅提高了SAT求解器的性能，解决了困扰命题逻辑领域二十余年的混合算法设计难题。对整数算术SMT问题，论文进一步设计了一种结合系统搜索算法与两种局部搜索引擎的双层混合机制，显著提升了SMT基求解器的性能。此外，论文利用运行时间的重尾分布现象，设计了冷-热重启的混合重启技术，基于此技术研制的SAT求解器，计算速度比同期主流求解器快四分之一。论文还将相关求解技术成功应用到电子设计自动化（EDA）和密码分析领域：通过将穷举仿真引入传统的组合等价性验证（CEC）框架SAT-sweeping，有效提高了工具在数据通路样例上的证明效率，与商用工具形成互补；通过结合密码分析技术，利用提出的轮增量SAT编码求解技术，高效求解了一类流密码分析问题。

中国科学院优秀博士学位论文评选始于2004年，每年评选一次。2025年，全院共有100篇论文入选。

张昕荻近照