基本信息

蔡少伟 

中国科学院软件研究所  研究员 博导

中国科学院大学 教授
电子邮件: 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


出版信息

一些论文

  1. Shaowei Cai, Bohan Li, Xindi Zhang:Local Search for SMT on Linear Integer Arithmetic. CAV (2) 2022: 227-248 [首个支持整数算术理论的SMT局部算术算法]

  2. 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混合求解的系统性论文]

  3. 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) [求解算法和在线化简嵌套执行,“剥洋葱”方法快速求解最大加权团问题]
  4. Shaowei Cai*, Xindi Zhang: Deep Cooperation of CDCL and Local Search for SAT, SAT 2021 [最佳论文奖]
  5. 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]
  6. 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]

  7. 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达到前沿水平]
  8. 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求解器]

  9. 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). [大规模顶点覆盖问题:构造,局部搜索,预处理]

  10. 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. [基于单元传播的消元法和局部搜索的混合算法]

  11. 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. [基于归约技术求解大规模图着色问题]

  12. Shaowei Cai*, Chuan Luo, Jinkun Lin, Kaile Su: New local search methods for partial MaxSAT, Artificial Intelligence (AIJ) 240: 1-18 (2016). [第一代在搜索过程区分硬子句和软子句的Partial MaxSAT算法]

  13. 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局部搜索]

  14. 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概率采样]

  15. 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局部搜索代表性前沿求解器]

  16. 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算法]

  17. Shaowei Cai*, Kaile Su: Local Search for Boolean Satisfiability with Configuration Checking and Subscore, Artificial Intelligence (AIJ) 204, pp.75-98 (2013). [SAT格局检测,二次评分函数,以及它们的理论分析]

  18. 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). [常常在文献中顶点覆盖的代表性局部搜索算法]

  19. 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. 16721696 (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