实验室动态 / 实验室风采 / 实验室动态 / 新闻动态

张昕荻荣获国际SAT协会2025最佳博士学位论文奖

第28届国际可满足性测试理论与应用会议(SAT 2025)于今年8月在苏格兰举办,期间公布了Fahiem-Bacchus Award 2025(最佳博士学位论文奖)获选人,实验室2024届毕业生张昕荻博士(导师:蔡少伟研究员)的学位论文获选。据悉,国际SAT协会每年从全球范围内仅遴选出1篇博士学位论文,授予“Fahiem-Bacchus Award”。

张昕荻,2018年进入实验室学习,2020年转为博士生,毕业后留在实验室任特别研究助理,曾获中国科学院院长奖特别奖、中国科学院优秀博士学位论文,主持国家自然科学基金青年基金项目1项。

其博士学位论文《Hybrid Algorithms for SAT and SMT and Their Applications》聚焦于命题逻辑可满足性问题(SAT)、可满足性模理论问题(SMT)的混合求解算法,及其若干应用问题。相关工作获得过SAT会议“最佳论文奖”、国际SAT、SMT、FLoC(国际逻辑学联合会议)竞赛冠军十余次、“强网杯”密码数学挑战赛全国冠军等荣誉。

论文创新性提出了一个以系统搜索为主体,局部搜索为辅的深度混合求解框架,大幅提高了SAT求解器的性能,解决了困扰命题逻辑领域二十余年的混合算法设计难题。对整数算术SMT问题,论文进一步设计了一种结合系统搜索算法与两种局部搜索引擎的双层混合机制,显著提升了SMT基求解器的性能。此外,论文利用运行时间的重尾分布现象,设计了冷-热重启的混合重启技术,基于此技术研制的并行SAT求解器,计算速度比同期主流求解器快四分之一。

论文还将相关求解技术成功应用到电子设计自动化(EDA)和密码分析领域:通过将穷举仿真引入传统的组合等价性验证(CEC)框架SAT-sweeping,有效提高了工具在数据通路样例上的证明效率,与商用工具形成互补;通过结合密码分析技术,利用提出的轮增量SAT编码求解技术,高效求解了一类流密码分析问题。

 

国际SAT协会(SAT Association)旨在推动可满足性问题及其相关领域的发展,包括SAT、MaxSAT、QBF、SMT、BDD、Model Counting、Model Checking等。协会通过组织年度SAT会议、出版《可满足性、布尔建模与计算期刊》(JSAT)、组织年度学术求解器比赛等方法,来实现其科研促进和学术交流的目的。