软件所形式化 蔡少伟 研究员
报告生成时间：2026年8月20日
个人主页：蔡少伟
所属团队：中国科学院软件研究所 / 计算机科学国家重点实验室
一、学者基本信息
| 项目 | 内容 |
|---|---|
| 姓名 | 蔡少伟（Shaowei Cai） |
| 职称 | 研究员、博士生导师 |
| 所属单位 | 中国科学院软件研究所 |
| 所属实验室 | 基础软件与系统重点实验室（计算机科学国家重点实验室） |
| 实验室职务 | 约束求解研究室 主任 |
| 兼任职务 | 中国科学院大学 教授 |
| 研究方向 | 约束求解（SAT/SMT/MaxSAT）、运筹优化、形式化验证、EDA验证 |
| 学术兼职 | CCF形式化方法专业委员会委员、CCF杰出会员、CCF学术工委执行委员 |
| 邮箱 | caisw@ios.ac.cn |
| 个人主页 | https://lcs.ios.ac.cn/~caisw/ |
| 团队主页 | http://solver.ios.ac.cn/ |
| GitHub | https://github.com/shaowei-cai-group |
二、教育背景与职业履历
教育背景
蔡少伟的求学经历横跨中国与澳大利亚，兼具数学与计算机科学的学术底蕴。2004年至2008年，他在华南理工大学攻读学士学位。随后进入北京大学深造，于2008年至2012年间完成博士学位研究生阶段学习，研究方向聚焦于布尔可满足性问题（SAT）的局部搜索算法。在北京大学博士期间，他于2012年参加SAT国际竞赛，代表中国团队首次获得SAT比赛冠军，且将第二名远远甩在身后，这一成果为其学术生涯奠定了重要基础。凭借卓越的博士研究工作，他获得2012年北京大学优秀博士论文奖和北京市优秀毕业生荣誉。此后，他于2012年至2014年在澳大利亚格里菲斯大学（Griffith University）联合澳大利亚国家信息通信技术中心（NICTA）攻读应用数学博士学位，进一步深化了在组合优化和算法设计方面的研究积累。
职业履历
- 2014年7月至2017年9月：中国科学院软件研究所，副研究员
- 2017年9月至今：中国科学院软件研究所，研究员（破格晋升）
蔡少伟在副研究员阶段即开始独立组建约束求解研究团队，2017年破格晋升为研究员后正式担任约束求解研究室主任。他从最初独立研发SAT求解器，逐步发展为带领十余人的研究团队，研究领域从SAT求解扩展到SMT求解、MaxSAT求解、混合整数规划求解以及EDA形式化验证工具等方向。他曾主持国家自然科学基金委青年B项目和重点项目，并获得中国科学院优秀导师（2021年）、智源青年科学家（2020年）、中科院软件所杰出青年（2018年）、中科院青促会会员（2017年）等多项荣誉。
三、学生培养情况
蔡少伟作为博士生导师，培养了一批在约束求解领域具有国际影响力的青年学者。他于2021年获得中国科学院优秀导师称号，其指导的学生在SAT、SMT、MaxSAT等国际竞赛中屡获冠军，多名学生的博士论文入选CCF专业委员会博士学位论文激励计划。
主要指导学生
| 姓名 | 身份 | 主要方向 | 代表性成果 |
|---|---|---|---|
| 李博涵 | 博士毕业生（2024届） | 算术理论SMT局部搜索 | 博士论文入选CCF形式化方法专委会2025年度博士学位论文激励计划；基于LocalSMT算法的求解器在SMT比赛获"最大领先奖"和"最大贡献奖"；获华为鸿蒙创新大赛冠军 |
| 张昕荻 | 博士生/特别研究助理 | SAT/SMT求解器 | SAT比赛主赛道并行组冠军主要参与者；X-SAT电路SAT求解器（DAC 2025）共同一作；基于部分解SAT求解器的ATPG工具论文共同一作 |
| 赵梦宇 | 博士生 | 分布式SMT求解 | CAV 2024杰出论文奖第一作者，提出基于变量级划分的动态并行SMT求解框架 |
| 钱宇航 | 硕士生 | 电路SAT求解 | DAC 2025论文X-SAT第一作者，提出高效电路SAT求解器 |
| 陈志翰 | 硕士生 | SAT求解 | SAT比赛主赛道并行组冠军主要参与者 |
| 初一 | 博士后 | MaxSAT求解 | MaxSAT比赛5个冠军和1个亚军主要参与者 |
| 陶悦 | 研究生 | SAT求解器硬件化 | VeriSAT：基于FPGA的SAT求解器硬件实现 |
蔡少伟指导的学生不仅在学术竞赛和论文发表方面成果丰硕，更有多人将研究成果应用于华为鸿蒙系统、香山处理器验证等实际工程项目，体现了团队"理论研究与工程应用并重"的培养理念。团队代码开源在GitHub上（shaowei-cai-group），促进了学术界的知识共享和技术传播。
四、学术合作网络
4.1 软件所内部合作
蔡少伟所在的中国科学院软件研究所计算机科学国家重点实验室（现基础软件与系统重点实验室）汇聚了形式化方法领域的多位顶尖学者，形成了以院士领衔、中青年骨干为主体的研究团队。蔡少伟作为约束求解研究室的主任，与实验室内的形式化方法团队保持紧密合作关系。
核心团队成员及合作关系：
- 周巢尘（中科院院士）：软件所形式化方法的奠基人之一，在时序逻辑程序验证等方面做出开创性贡献。蔡少伟的约束求解工作为周巢尘院士团队的形式化验证研究提供了底层求解技术支撑。
- 林惠民（中科院院士）：著名并发理论专家，其研究成果为软件所形式化方法方向的学术地位奠定了基础。
- 詹乃军（研究员）：CCF形式化方法专委会主任，研究方向涵盖实时系统形式化验证、混成系统验证等。詹乃军与蔡少伟同属软件所形式化方法团队，在CCF形式化方法专委会中有密切协作。詹乃军近期工作聚焦于国产多核实时操作系统微内核的全流程形式化验证（2.5万行源码验证、45万行Coq验证代码），蔡少伟的求解器技术为其验证工作提供了核心计算引擎。
- 吴志林（研究员）：基础软件与系统重点实验室常务副主任、CCF形式化方法专委会秘书长。吴志林的研究方向涵盖模型检测、程序验证等，与蔡少伟在硬件形式化验证（如BMCFuzz：BMC与模糊测试结合的RISC-V处理器验证方法）方面有直接合作。
- 张立军（研究员）：在概率系统验证、定量模型检测等方面有深入研究，与蔡少伟在CAV等顶级会议发文方面有学术交集。
- 宋富（研究员）：形式化方法领域专家，参与RISC-V处理器验证工作，与蔡少伟团队在BMCFuzz等项目上有合作。
- 薛白（研究员）：量子系统形式化验证方向，与蔡少伟的CAV 2024论文同期被录用，属于同一实验室的平行研究团队。
- 李勇坚（副研究员）：模型检查工具方向，DAC 2025论文通讯作者，与蔡少伟同属约束求解研究室，在EDA验证工具有密切合作。
4.2 跨机构学术合作
蔡少伟的学术合作网络覆盖国内多所高校和研究机构，主要体现在以下几个方面：
国内高校合作：
- 北京大学：蔡少伟的母校，他与北京大学数学科学学院孙猛教授（CCF形式化方法专委执行委员）在CCF形式化方法专委会学术活动中有密切协作。北京大学也是他从博士阶段开始SAT研究的起点。
- 东北师范大学：与王艺源等人在MaxSAT求解方向有合作研究，共同获得MaxSAT比赛冠军。
- 华南理工大学：蔡少伟的本科母校，是其学术生涯的起点。
- 浙江大学：陈明帅（Mingshuai Chen）为软件所博士毕业生（2019届），现赴浙江大学组建形式化验证团队，与蔡少伟在形式化方法领域保持学术联系。
- 北京航空航天大学：根据讲座信息，蔡少伟被介绍为"北京航空航天大学教授"，表明其可能与北航有兼职或合作关系。
工业界研究机构合作：
- 华为理论实验室：与雷震东等人在MaxSAT求解方向有合作研究，共同获得MaxSAT比赛冠军。华为鸿蒙创新大赛冠军项目也体现了深度的产学研合作。
- 中国科学院先导A专项"RISC-V基础软件"：蔡少伟团队的X-SAT求解器等工作获得该专项支持，体现了与中科院内部RISC-V研究团队的合作。
4.3 国际合作
蔡少伟在国际约束求解学术界建立了广泛的合作网络，与多位国际顶尖学者保持长期合作关系。
核心国际合作伙伴：
- Armin Biere（奥地利林茨大学，SAT协会主席）：蔡少伟最重要的国际合作伙伴。两人作为SAT混合求解方向的两个主要团队负责人，在2021年SAT线上会议中深入讨论彼此的技术路线后，决定合作撰写系统性介绍SAT混合求解前沿技术的长文。合作成果"Better Decision Heuristics in CDCL through Local Search and Target Phases"发表在人工智能顶级期刊Journal of Artificial Intelligence Research（JAIR），为SAT混合求解方向提供了系统性的理论参考。此外，Mathias Fleury也参与了该合作。
- Holger H. Hoos（荷兰莱顿大学/加拿大UBC，欧洲科学院院士）：在伪布尔优化（Pseudo Boolean Optimization）的局部搜索算法研究上有合作，成果发表在SAT 2021。
- Griffith University / NICTA（澳大利亚）：蔡少伟的应用数学博士阶段联合培养机构，为其在组合优化和算法设计方面奠定了数学基础。
国际竞赛中的对手与合作伙伴：
蔡少伟团队在国际SAT竞赛、SMT竞赛和MaxSAT竞赛中与以下国际团队既是竞争对手也是交流伙伴：微软研究院（Z3求解器团队）、斯坦福大学（CVC5求解器团队）、意大利特伦托大学（MathSAT5求解器团队）、美国爱荷华大学（Yices2求解器团队）等。其研发的Z3++求解器基于微软Z3求解器的衍生开发，体现了与微软研究院的技术交流关系。
五、业界合作关系深度分析
蔡少伟团队的研究成果具有极强的工程实用价值，其研发的约束求解器被集成到多家国内外头部企业的核心软件中，应用场景涵盖芯片设计验证、操作系统验证、云计算调度、航空制造调度等多个关键领域。
主要企业合作：
| 企业/机构 | 合作内容 | 应用场景 |
|---|---|---|
| 华为 | EDA形式化验证工具、鸿蒙操作系统验证 | 求解器被确定为鸿蒙系统新特性；华为鸿蒙创新大赛冠军 |
| 英伟达（NVIDIA） | SAT求解器技术引用 | 求解器被英伟达重点引用，用于芯片设计验证 |
| 微软 | 云平台故障检测 | Z3++求解器基于微软Z3的衍生开发 |
| 英特尔（Intel） | 芯片设计验证 | 求解器应用于集成电路验证 |
| 华大九天 | EDA工具集成 | 求解器应用于EDA布局布线 |
| 中国航空集团 | 工业调度 | 航空制造调度优化 |
| 国家电网 | 优化调度 | 电力系统调度优化 |
| 阿里巴巴 | 云计算调度 | 云平台资源调度 |
| 香山处理器团队 | 处理器缓存协议验证 | 找到多个死锁错误和互斥性错误并提出修正方案 |
蔡少伟团队的业界合作模式具有以下特点：一是从基础研究到工程落地的完整链条，团队不仅研发求解器算法，还针对具体企业需求定制化开发硬件形式化验证工具（如电路等价性验证工具、Model Checking工具、ATPG工具）；二是覆盖面广，从国产EDA企业到国际芯片巨头，从操作系统厂商到云服务提供商，体现了约束求解作为"工业软件之魂"的基础性地位；三是持续深化，近年来团队将约束求解技术与大模型技术结合，研发了首个基于大模型技术的SAT求解器，英伟达对此成果进行了重点引用，标志着团队在前沿技术探索方面持续保持国际领先。
此外，蔡少伟还担任EDA²形式化验证标准组组长和《EDA技术白皮书》形式化验证方向主编，在行业标准制定方面发挥着重要的引领作用。他翻译的国际经典教材《Decision Procedures: An Algorithmic Point of View》中文版，进一步推动了约束求解领域知识在国内的传播普及。
六、重要奖项与学术兼职
重要奖项
| 年份 | 奖项 | 级别 |
|---|---|---|
| 2024 | CAV杰出论文奖（Distributed SMT Solving Based on Dynamic Variable-level Partitioning） | 国际顶级会议 |
| 2024 | CP最佳论文奖（An Efficient Local Search Solver for Mixed Integer Programming） | 国际顶级会议 |
| 2022-2023 | SMT比赛Model Validation赛道"最大领先奖"和"最大贡献奖" | 国际竞赛 |
| 2022 | FLoC奥林匹克竞赛2块金牌（SMT比赛，国内首次） | 国际奥林匹克竞赛 |
| 2021 | SAT最佳论文奖（Deep Cooperation of CDCL and Local Search for SAT） | 国际顶级会议 |
| 2012-2023 | SAT比赛10余枚金牌（主赛道和并行主赛道） | 国际竞赛 |
| 2013-2023 | MaxSAT比赛多个赛道冠军，多年蝉联非完备赛道冠军 | 国际竞赛 |
| 2021 | 华为鸿蒙创新大赛冠军 | 产业竞赛 |
| — | EDA精英挑战赛冠军及特别奖 | 产业竞赛 |
| 2021 | 中国科学院优秀导师 | 院级荣誉 |
| 2020 | 智源青年科学家 | 市级/机构荣誉 |
| 2018 | 中科院软件所杰出青年 | 所级荣誉 |
| 2017 | 中科院青促会会员 | 院级荣誉 |
| 2012 | 北京大学优秀博士论文奖、北京市优秀毕业生 | 校/市级荣誉 |
学术兼职
- CCF形式化方法专业委员会委员
- CCF杰出会员、CCF杰出演讲者
- CCF学术工委执行委员
- SAT 2027会议程序委员会主席
- EDA²形式化验证标准组组长
- 《EDA技术白皮书》形式化验证方向主编
- FMCAD、CP、SOCS等国际会议特邀报告人
- 国家自然科学基金委重点项目主持人
七、Connection圈层总结
蔡少伟是中国约束求解领域的领军人物，其学术关系网络呈现出以技术为核心、产学研深度融合的鲜明特征。
核心圈层（约束求解研究室团队）： 以蔡少伟为学术领袖，围绕博士生李博涵、张昕荻、赵梦宇及硕士生钱宇航等核心成员构建的紧密研究团队，是其在SAT/SMT/MaxSAT竞赛和顶级会议论文产出方面的主力。该团队是国内唯一在SAT、SMT、MaxSAT三大约束求解竞赛中均获得冠军的团队。
院所圈层（软件所形式化方法团队）： 与詹乃军（CCF形式化方法专委会主任）、吴志林（专委会秘书长）等同事构成软件所形式化方法的中坚力量。周巢尘院士和林惠民院士作为学术前辈奠定了团队的学术地位。约束求解为形式化验证提供底层计算引擎，蔡少伟的求解器技术直接支撑了詹乃军的操作系统微内核验证和吴志林的处理器验证工作，形成了"求解器-验证工具-应用场景"的完整技术链条。
学术圈层（国际约束求解社区）： 与Armin Biere（SAT协会主席）和Holger H. Hoos（欧洲科学院院士）等的深度合作，使蔡少伟在国际SAT/SMT学术界占据重要话语权。他担任SAT 2027程序委员会主席，标志着其国际学术地位得到广泛认可。
产业圈层（工业应用网络）： 求解器被华为、英伟达、微软、英特尔、华大九天等头部企业采用，应用于芯片验证、操作系统验证、云平台故障检测等关键场景，体现了其研究成果从基础理论到工程落地的完整转化能力。
蔡少伟的独特价值在于：他不仅是中国约束求解领域的学术领军者，更是连接基础理论研究和工业关键应用的桥梁。在形式化验证领域，SAT/SMT求解器被称为"工业软件之魂"，蔡少伟团队的工作直接支撑了国产EDA工具链、国产处理器验证和国家信息安全基础设施的建设，具有不可替代的战略意义。