蔡少伟
中国科学院软件研究所 研究员 博导
中国科学院大学 教授
电子邮件: caisw@ios.ac.cn
通信地址: 北京市海淀区中关村南四街4号中国科学院软件园区5号楼210
邮政编码: 100190
研究方向 和 招生信息
本人主要研究方向为约束求解、组合优化以及EDA(电子设计自动化)验证。主要学术成果包括:
(1)(逻辑)约束求解:包括布尔可满足性问题(SAT),可满足性模理论问题(SMT),最大可满足性问题(MaxSAT)等,是软件和硬件验证、信息安全、工业调度等领域的核心技术。在SAT比赛和SMT比赛连续多年获得多个冠军,包括国内团队首次获得SAT比赛冠军(2012)和国内团队首次获得SMT比赛冠军(2021),在2013-2023年MaxSAT比赛连续获得多个赛道冠军,多年蝉联非完备赛道冠军。获得多个联合逻辑奥林匹克金牌。对SAT问题提出CDCL求解+局部搜索采样的混合求解方法,解决了命题逻辑推理与搜索方向十大挑战的第7个挑战,获得SAT会议最佳论文奖;对于SMT问题,设计了首个支持算术理论的局部搜索算法,与Z3结合研发了Z3++求解器,获得2022和2023年SMT比赛模型验证赛道的最大领先奖和最大贡献奖。在分布式约束求解器取得了突破,研发了并行和分布式的SAT求解器,SMT求解器,MaxSAT求解器。分布式求解器解决了多个之前未被解决的实例。
(2)组合优化和运筹优化:对于组合优化问题,最常见的启发式算法是局部搜索,对多个著名组合优化问题如最大团,图着色,顶点覆盖,集合覆盖等NP难问题设计了高效的局部搜索算法和化简算法,求解性能保持着前沿水平;提出了格局检测策略,有效解决局部搜索的重要缺陷—循环现象,被广泛用于各种NP难组合优化问题,相关论文曾被评为人工智能旗舰期刊Artificial Intelligence近五年最受欢迎论文之一;对大规模组合优化问题,设计了“搜索与推理”的半精确算法,在多个著名组合优化问题上,对稀疏实例上可秒级求解千万顶点规模的图优化问题。
(3)EDA形式化验证:设计了结合SAT求解与精确仿真的算法,研发了组合电路等价性验证工具,对数据通路电路的验证明显优于已有开源工具;研发了Model Checking工具,在标准测试集上优于ABC和IC3-ref等著名工具;研发了ATPG工具,在一些来自实际电路数据集上,优于开源工具性能。团队还对香山处理器等开源处理器进行了缓存协议验证,找到了多个死锁错误,并提出了修正方案。
相关论文发表在ACM Transactions on Computational Logic, Artificial Intelligence, IEEE Trans. on Computers, CAV,ICCAD,SAT,CP,AAAI等相关领域顶级期刊和会议。研发的SAT求解器提高了龙头企业芯片验证的SAT求解规模,提高了验证能力,已被多家EDA公司用于其EDA工具;提出的搜索技术成功应用于微软Azure云平台的故障检测;此外,相关技术还应用于多个产业,在EDA、软件验证、云计算、银行系统优化、运营排班、智慧园区等领域展开了系列项目。
招收研究生和实习生,希望学生有优秀的算法基础和编程能力, 较好的数学基础(尤其是离散数学)和英语能力。如有意愿保送研究生,请尽早联系。
工作经历
工作简历
2017-09~现在, 中国科学院软件研究所, 研究员
2014-07~2017-09,中国科学院软件研究所, 副研究员
讲授课程
离散数学
高级算法设计与分析
约束求解
社会兼职
- CCF学术工作委员会 执行委员,2024-2026
- EDA^2 开放合作机制,《EDA技术白皮书》形式化工具方向 主编
- 2022中国软件大会“约束求解与定理证明”论坛,联合主席,2022.11.25
- 中科院青年创新促进会 信息与管理分会 会长, 2019.10.16-2022.4.10;
- 程序委员会主席,the first international workshop of Heuristic Search in Industry (HSI 2020), conjunction with the 29th IJCAI Conference on Artificial Intelligence (IJCAI 2020);
- 发起人, Workshop on Hard Computational Problems: Representations, Algorithms and Applications (HCP会议) 2017起
- 程序委员会(高级)委员, IJCAI, AAAI, SAT, CP, FMCAD, ICAPS
- Yong Associate Editor,Frontinese of Computer Sciences, 2014.12-2019.12
- 客座编辑,"Constraints and Optimizations" special issue, Science China:Information Sciences, 2020.
荣誉与奖励
荣誉与奖励
- 中国计算机学会(CCF)杰出会员,2023
- 中国计算机学会(CCF)杰出演讲者,2022
- 中国科学院大学“领雁”奖,2022
- SAT会议最佳论文奖,2021
- 中国科学院优秀导师,2021,2024
- 中科院青年创新促进会 优秀会员,2021
- 长白山领军人才,2020
- 智源青年科学家,2020
- 北京市优秀毕业生, 2012
- 北京大学优秀博士论文奖,2012
- 北京大学学术创新奖, 2011
学术比赛获奖
- 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
- 全球运筹优化挑战赛-城市物流运输车辆智能调度 Excellence Award, 2018
- 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
出版信息
一些论文
Shaowei Cai, Bohan Li, Xindi Zhang:Local Search for SMT on Linear Integer Arithmetic. CAV (2) 2022: 227-248 [首个支持整数算术理论的SMT局部算术算法]
Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere: Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. 74: 1515-1563 (2022) [和Armin Biere团队一起总结了SAT混合求解的系统性论文]
- Shaowei Cai, Jinkun Lin, Yiyuan Wang, Darren Strash: A Semi-Exact lgorithm for Quickly Computing a Maximum Weight Clique in Large Sparse Graphs, J. Artif. Intell. Res. 72: 39-67 (2021) [求解算法和在线化简嵌套执行,“剥洋葱”方法快速求解最大加权团问题]
- Shaowei Cai*, Xindi Zhang: Deep Cooperation of CDCL and Local Search for SAT, SAT 2021 [最佳论文奖]
- Jinkun Lin, Shaowei Cai*, Bing He, Yingjie Fu, Chuan Luo, Qingwei Lin: FastCA: An Effective and Efficient Tool for Combinatorial Covering Array Generation. ICSE 2021 [组合测试覆盖产生工具 FastCA]
Shaowei Cai*, Zhendong Lei: Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability, Artificial Intelligence (AIJ), 287(2020)103354 [SATLike求解器, Partial MaxSAT]
- Yiyuan Wang#, Shaowei Cai#*, Jiejiang Chen, Minghao Yin: SCCWalk: An Efficient Local Search Algorithm and Its Improvements for Maximum Weight Clique Problem, Artificial Intelligence (AIJ), 280: 103230 (2020). Co-first author [最大加权团算法,在大量不同类型benchmark达到前沿水平]
Kenji Kanazawa, Shaowei Cai: FPGA Acceleration to Solve Maximum Clique Problems Encoded into Partial MaxSAT, 12th IEEE International Symposium on Embedded Multicore/Many-core Systems-on-Chip (MCSoC 2018), Hanoi, Vietnam, September 12-14, 2018 [FPGA加速MaxSAT求解器]
Shaowei Cai*, Jinkun Lin, Chuan Luo: Finding A Small Vertex Cover in Massive Sparse Graphs: Construct, Local Search, and Preprocess, Journal of Artificial Intelligence Research (JAIR) 59: 463-494 (2017). [大规模顶点覆盖问题:构造,局部搜索,预处理]
Shaowei Cai*, Chuan Luo, Haochen Zhang: From Decimation to Local Search and Back: A New Approach to MaxSAT, 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), Melbourne, Australia, August 19-25, 2017. [基于单元传播的消元法和局部搜索的混合算法]
Jinkun Lin, Shaowei Cai*, Chuan Luo, Kaile Su: A Reduction based Method for Coloring Very Large Graphs, 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), Melbourne, Australia, August 19-25, 2017. [基于归约技术求解大规模图着色问题]
Shaowei Cai*, Chuan Luo, Jinkun Lin, Kaile Su: New local search methods for partial MaxSAT, Artificial Intelligence (AIJ) 240: 1-18 (2016). [第一代在搜索过程区分硬子句和软子句的Partial MaxSAT算法]
Chuan Luo, Shaowei Cai*, Wei Wu, Zhong Jie, Kaile Su: CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability, IEEE Transactions on Computers (ToC) 64(7): 1830-1843 (2015). [加权MaxSAT局部搜索]
Shaowei Cai: Balance between Complexity and Quality: Local Search for Minimum Vertex Cover in Massive Graphs, 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), Buenos Aires, Argentina, July 25-31, 2015. [提出BMS概率采样]
Shaowei Cai*, Chuan Luo, Kaile Su: CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability, 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Austin, Texas, USA, September 24-27, 2015. [CCAnr求解器,该求解器仍然是SAT局部搜索代表性前沿求解器]
Shaowei Cai*, Chuan Luo, John Thornton, Kaile Su: Tailoring Local Search for Partial MaxSAT, Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI 2014), Québec Convention Center, Québec City, Québec, Canada, July 27–31, 2014. [首次在搜索过程区分硬子句和软子句的Partial MaxSAT算法]
Shaowei Cai*, Kaile Su: Local Search for Boolean Satisfiability with Configuration Checking and Subscore, Artificial Intelligence (AIJ) 204, pp.75-98 (2013). [SAT格局检测,二次评分函数,以及它们的理论分析]
Shaowei Cai, Kaile Su, Chuan Luo, Abdul Sattar: NuMVC: An Efficient Local Search Algorithm for Minimum Vertex Cover, Journal of Artificial Intelligence Research (JAIR) 46, pp. 687-716 (2013). [常常在文献中顶点覆盖的代表性局部搜索算法]
Shaowei Cai*, Kaile Su, Abdul Sattar: Local search with edge weighting and configuration checking heuristics for minimum vertex cover, Artificial Intelligence (AIJ) 175(9-10), pp. 1672–1696 (2011). [提出格局检测,该策略已经被广泛用于NP难问题的局部搜索算法]
科研活动
一些科研项目:
- “面向信息安全领域的约束求解器研究”,科技部重点研发计划,课题负责人,2023-11--2028-11
- “可满足性问题求解”,国家自然科学基金优秀青年科学基金项目, 主持, 2022-01--2024-12
- “生成式智慧视窗基于约束求解实现UI自适应布局技术”,HW研发项目,2024
- “布尔可满足性问题的并行算法研究”,CCF-华为胡杨林基金A类项目,主持,2022-2023
- “端到端合约广告最优分配机制的研究”,阿里巴巴研究项目,主持,2022-2023
- “总装调度约束求解算法设计工具开发”,中国航空制造技术研究院,主持,2022-2023
- “等价性验证SAT求解器”,HW研发项目,主持,2022
- “形式化约束方程组的增量求解”,HW研发项目,主持,2021
- “Resource Optimization in Cloud Computing”,微软亚洲研究院合作项目,主持,2022年
- “Intelligent Software Configuration Analysis and Optimization”, 微软亚洲研究院合作项目,主持,2020年
- “逻辑公式可满足性求解及其应用”,智源青年科学家项目,北京智源人工智能研究院,主持,2020-2022
- “最大可满足性问题的局部搜索算法”, 国家自然科学基金青年科学基金项目, 主持, 2016-01--2018-12
- “网络空间大数据的表示、度量与语义理解”, 科技部973项目课题, 参与, 2014-01--2018-12