研究方向

• 约束求解
• 运筹优化
• EDA（电子设计自动化）验证

主要学术成果

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

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

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

相关论文发表在ACM Transactions on Computational Logic, Artificial Intelligence, IEEE Trans. on Computers, CAV，DAC，ICCAD，SAT，CP，AAAI等相关领域顶级期刊和会议。研发的求解器和形式化工具提高了芯片验证和软件验证的能力，已被多家公司采用；相关技术还应用于多个产业，在EDA、软件验证、云计算、银行系统优化、运营排班、智慧园区等领域展开了系列项目。