Nothing Special   »   [go: up one dir, main page]
基本信息

蔡少伟 

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

中国科学院大学 教授

https://lcs.ios.ac.cn/~caisw/


电子邮件： 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 2021会议最佳论文奖；对于SMT问题，设计了首个支持算术理论的局部搜索算法，与Z3结合研发了Z3++求解器，获得2022和2023年SMT比赛模型验证赛道的最大领先奖和最大贡献奖。在分布式约束求解器取得了突破，带领团队研发了并行和分布式的SAT求解器，SMT求解器，MaxSAT求解器，解决了多个之前未被解决的实例。相关论文获得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，DAC，ICCAD，SAT，CP，AAAI等相关领域顶级期刊和会议。研发的求解器和形式化工具提高了芯片验证和软件验证的能力，已被多家公司采用；相关技术还应用于多个产业，在EDA、软件验证、云计算、银行系统优化、运营排班、智慧园区等领域展开了系列项目。


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

工作经历

工作简历
2017-09~现在, 中国科学院软件研究所, 研究员
2014-07~2017-09,中国科学院软件研究所, 副研究员


讲授课程

  • 离散数学 （本科课程）

  • 高级算法设计与分析 （研究生课程）

  • 约束求解 （研究生课程）


社会兼职

  • CCF学术工作委员会 执行委员，2024-2026
  • EDA^2 开放合作机制，《EDA技术白皮书》形式化工具方向 主编
  • EDA^2 开放合作机制，形式化验证标准起草组 组长
  • 2023年中国软件大会“形式化验证@EDA”论坛，联合主席，2023.12.1
  • 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
  • 中国科学院优秀导师，2021，2024
  • 中科院青年创新促进会 优秀会员，2021
  • 长白山领军人才，2020
  • 智源青年科学家，2020
  • 北京市优秀毕业生, 2012
  • 北京大学优秀博士论文奖，2012
  • 北京大学学术创新奖, 2011

论文获奖

  • CAV 2024 会议 杰出论文奖 （中国首次）
  • CP 2024 会议 最佳论文奖 （亚洲首次）
  • SAT 2011会议 最佳论文奖（亚洲首次）

比赛获奖

  • 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
  • 全球运筹优化挑战赛-城市物流运输车辆智能调度 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. Mengyu Zhao, Shaowei Cai*, Yuhang Qian: Distributed SMT Solving Based on Dynamic Variable-Level Partitioning. CAV 2024: 68-88 [SMT分布式方法] [杰出论文奖]

  2. Peng Lin, Mengchuan Zoo, Shaowei Cai*: An Efficient Local Search Solver for Mixed Integer Programming. CP 2024: 19:1-19:19 [整数贵哈问题快速启发式求解] [最佳论文奖]

  3. Xindi Zhang, Bohan Li, Shaowei Cai*: Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory. ICSE 2024: 125:1-125:13 [SMT问题的混合求解算法CDCL(T)+LS]

  4. Yiyuan Wang, Chenghou Jin,Shaowei Cai*: PathLAD+: Towards effective exact methods for subgraph isomorphism problem. Artificial Intelligence (AIJ) 337:104219 (2024) [子图同构问题的精确算法]

  5. Yan Li , Yundu Huang , Wuyang Mao , Furong Ye , Xiang He , Zhonglin Zu , Shaowei Cai*: Bi-Objective Contract Allocation for Guaranteed Delivery Advertising. KDD 2024: 1691-1700 [双目标二次规划算法解决合约广告问题]

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

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

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

  11. 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]

  12. 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达到前沿水平]

  13. 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求解器]

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

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

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

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

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

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

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

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

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

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

  24. 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