本人主要研究方向为约束求解、运筹优化以及EDA（电子设计自动化）验证。主要学术成果包括：

（1）（逻辑）约束求解：包括布尔可满足性问题（SAT），可满足性模理论问题（SMT），最大可满足性问题（MaxSAT）等，是软件和硬件验证、信息安全等领域的核心技术。从独立研发到带领团队，在SAT比赛和SMT比赛连续多年获得多个冠军，包括国内团队首次获得SAT比赛冠军（2012）和国内团队首次获得SMT比赛冠军（2021），在2013-2023年MaxSAT比赛连续获得多个赛道冠军，多年蝉联非完备赛道冠军。获得多个联合逻辑奥林匹克金牌。对SAT问题提出CDCL求解+局部搜索采样的混合求解方法，解决了命题逻辑推理与搜索方向十大挑战的第7个挑战；对于SMT问题，设计了首个支持算术理论的局部搜索算法，与Z3结合研发了Z3++求解器，获得2022和2023年SMT比赛模型验证赛道的最大领先奖和最大贡献奖。在分布式约束求解器取得了突破，带领团队研发了并行和分布式的SAT求解器，SMT求解器，MaxSAT求解器，解决了多个之前未被解决的实例。相关论文获得SAT 2021最佳论文奖和CAV 2024杰出论文奖。

（2）运筹优化/组合优化：[早期]对多个著名组合优化问题如最大团，图着色，顶点覆盖，集合覆盖等NP难问题设计了高效的局部搜索算法和化简算法，求解性能保持着前沿水平；提出了格局检测策略，有效解决局部搜索的重要缺陷—循环现象，被广泛用于各种NP难组合优化问题，设计了“搜索与推理”的半精确算法，在多个著名组合优化问题上，对稀疏实例上可秒级求解千万顶点规模的图优化问题。[近期] 带来团队研发了混合整数（线性和非线形）规划求解器，在标准测试集的快速求解能力领先于商业求解器Gurobi，刷新了多个挑战实例的求解记录，应用于EDA布局布线和互联网广告业务等实际场景，论文发表在KDD，CP等顶级会议，获得CP 2024会议最佳论文奖。

（3）形式化验证：针对EDA和操作系统验证定制求解器，应用于多家企业。带领团队自研了硬件形式化验证工具，包括电路等价性验证工具，Model Checking工具，ATPG工具，在一些来自实际电路数据集上，优于开源工具性能。团队还对香山处理器等开源处理器进行了缓存协议验证，找到了多个死锁错误和互斥性错误，并提出了修正方案。研发了高效SMT求解算法，定制增量式SMT求解和轻量级SMT求解，提高操作系统验证工具的性能，且应用于操作系统的页面自动布局。

相关论文发表在ACM Transactions on Computational Logic, Artificial Intelligence, IEEE Trans. on Computers, CAV，FM，DAC，ICCAD，SAT，CP，AAAI等相关领域顶级期刊和会议。研发的求解器和形式化工具提高了芯片验证和软件验证的能力，被集成到包括英伟达、英特尔、微软、华为等公司的软件，应用于我国的工业软件（EDA和工业调度）和基础软件（操作系统），并促进产业转化。

指导的所有博士毕业生皆获得中科院院长奖（包括特别奖和优秀奖），其中一名博士毕业生作为中国科学院大学研究生唯一毕业生代表在毕业典礼发言。

持续招收研究生和实习生，希望学生有优秀的算法基础和编程能力， 较好的数学基础（尤其是离散数学）和英语能力。如有意愿保送研究生，请尽早联系，大二暑假可以开始。

工作简历

2017-09~现在, 中国科学院软件研究所, 研究员

2014-07~2017-09,中国科学院软件研究所, 副研究员

讲授课程

• 离散数学 （本科课程）
• 高级算法设计与分析 （研究生课程）
• 约束求解 （研究生课程）

社会兼职

• SAT 2027会议 程序委员会主席
• CCF学术工作委员会 执行委员，2024-2026，2026-2028
• 中关村国家实验室网络空间先进技术研究院 首席科学家成员
• EDA^2 开放合作机制，《EDA技术白皮书》形式化工具方向 主编
• EDA^2 开放合作机制，形式化验证标准起草组 组长
• 中国物流50人智库专家，中国物流与采购联合会，2024年起
• 中科院青年创新促进会 信息与管理分会 会长, 2019.10.16-2022.4.10；
• IJCAI Heuristic Search in Industries workshop 发起人、程序委员会主席
• Workshop on Hard Computational Problems: Theories, Algorithms and Applications （HCP会议），发起人， 2017起
• 程序委员会（高级）委员：FM，TACAS，SAT, CP, FMCAD, ICAPS
• Yong Associate Editor，Frontinese of Computer Sciences, 2014.12-2019.12

荣誉

• 中国计算机学会（CCF）杰出会员，2023
• 中国计算机学会（CCF）杰出演讲者，2022
• 中国科学院大学“领雁”奖，2022
• 中国科学院优秀导师，2021，2024，2025
• 中科院青年创新促进会 优秀会员，2021
• 长白山领军人才，2020
• 智源青年科学家，2020
• 北京市优秀毕业生, 2012
• 北京大学优秀博士论文奖，2012
• 北京大学学术创新奖, 2011

论文获奖

• ICLR 2026 Logical Reasoning of Large Language Models Workshop 杰出论文奖
• CAV 2024 会议 杰出论文奖 （CCF A，形式化方法顶级会议，中国首次）
• CP 2024 会议 最佳论文奖 （CCF B，约束规划领域旗舰会议，中国团队首次）
• SAT 2021会议 最佳论文奖（CCF B，SAT领域旗舰会议，亚洲首次）

比赛获奖

• 2026年国际混合整数规划比赛MIPcc，提名奖（比赛共设一个冠军和两个提名奖），中国首次获奖
• 2025年，华为鸿蒙创新大赛，一等奖
• 2025年SMT比赛，并行赛道“最大领先奖”和“最大贡献奖”
• 2025年SMT比赛，位向量分组多个冠军
• 2025年SMT比赛，非线性算术理论增量求解冠军
• 2024年工信部求解器技术专题比赛，二等奖
• 2024年EDA精英挑战赛总决赛“超图分割算法设计”赛道二等奖和思尔芯企业特别奖，指导教师
• 2024年国际SMT比赛，云赛道“最大领先奖”和“最大贡献奖”
• 2024年国际SAT比赛，云赛道 亚军
• 2023年国际SAT比赛Main track并行组所有冠军，云赛道亚军
• 2023年国际SMT-COMP比赛多个赛道冠军，囊括整数算术理论（包括线形和非线形）所有冠军，总分获得“最大领先奖”和“最大贡献奖”
• 2023年MaxSAT比赛非完备赛道所有组冠军
• 第六届“强网杯”全国网络安全挑战赛密码数学专项赛，冠军，2023
• 2022年国际SMT-COMP比赛多个赛道冠军，总分获得两枚金牌“最大领先奖”和“最大贡献奖”（大赛共设有6枚金牌），2022
• 2022年国际SAT比赛Main track并行组冠军，Non-Limits组冠军，2022
• 2022年国际MaxSAT比赛获得5个冠军1个亚军（总共6个赛道），2022
• 2021年国际SMT-COMP比赛QF_IDL theory冠军（中国首次在SMT-COMP获冠军），2021
• 2021年国际EDA Challenge比赛亚军，2021
• 2021年国际SAT比赛Main track SAT,UNSAT 亚军，2021
• 2021年国际MaxSAT比赛完备组（加权）冠军， 非完备组（不加权和加权）冠军，2021
• 2020年国际SAT比赛Main track SAT 冠军，2020
• 2020年国际SAT比赛Planning track 亚军，2020
• 2018年Sparkle SAT Challenge, 亚军, 2018
• 2018年国际SAT比赛No-Limits track 冠军, 2018
• 2018年联合逻辑大会奥林匹克 金牌, 2018
• 2016年国际SAT比赛Random track 亚军, 2016
• 2014国际SAT比赛Hard-combinatorial组 亚军, 2014
• 2012国际SAT比赛,Best Solver Award （中国首次在SAT-COMP系列比赛获冠军）, 2012
• 中国机器人暨RoboCup公开赛:足球机器人比赛中型组，一等奖，2007

主持的一些科研项目：

• “SAT求解算法的理论分析与新型求解器”，国家自然科学基金重点项目，主持，2026.1-2030.12
• “可满足性问题求解”，国家自然科学基金优秀青年科学基金项目, 主持, 2022-01--2024-12
• “面向信息安全领域的约束求解器研究”，科技部重点研发计划，课题负责人，2023-11--2028-11
• “不确定场景下的模型数据混合驱动电力优化决策关键技术研究”，国家电网总部管理科技项目，2025
• “数字仿真工具中的约束随机过程优化算法”，华大九天公司研发项目，2025
• “SMT(BV)高效并行求解器研发项目”，HW研发项目，2024
• “生成式智慧视窗基于约束求解实现UI自适应布局技术”，HW研发项目，2024
• “总装调度约束求解算法设计工具开发”，中国航空制造技术研究院，主持，2022-2023
• “等价性验证SAT求解器”，HW研发项目，主持，2022 
• “逻辑公式可满足性求解及其应用”，智源青年科学家项目，北京智源人工智能研究院，主持，2020-2022
• “最大可满足性问题的局部搜索算法”, 国家自然科学基金青年科学基金项目, 主持, 2016-01--2018-12