🔥 News

• 2025.08:  🎉🎉 Fahiem Bacchus PhD Thesis Award, SAT Association (only one awarded globally each year, first recipient from Asia) 国际SAT协会最佳博士论文奖（每年全球一篇，亚洲首个）

• 2025.08:  🎉🎉 1 paper has been accepted by ASE (CCF-A) 1篇论文被ASE (CCF-A) 接收

• 2025.07:  🎉🎉 PhD thesis awarded “Outstanding PhD Thesis of the Chinese Academy of Sciences” 博士学位论文获得”中科院优秀博士论文”

• 2025.05:  🎉🎉 1 papers has been accepted by CP（CCF-B） 1篇论文被CP (CCF-B) 接收

• 2025.02:  🎉🎉 4 papers have been accepted by DAC（CCF-A） 4篇论文被DAC (CCF-A) 接收

• 2024.12:  🎉🎉 Second Prize + Enterprise Special Award, China Postgraduate IC Innovation Competition EDA Elite Challenge 中国研究生创”芯”大赛·EDA精英挑战赛 二等奖 + 企业特别奖

• 2024.08:  🎉🎉 Second Place in SAT Competition Cloud Track 国际SAT比赛云计算赛道亚军

• 2024.07:  🎉🎉 Graduate student representative, 2024 Commencement, University of Chinese Academy of Sciences 中国科学院大学2024年毕业典礼，研究生代表

• 2024.06:  🎉🎉 “President’s Special Award”, University of Chinese Academy of Sciences “中国科学院大学 院长奖-特别奖”

🎖 Honors

• 2025.08:   Fahiem Bacchus PhD Thesis Award, SAT Association (1 winner globally per year) 国际SAT协会“最佳博士论文奖”（每年全球遴选一位） 🔍

• 2025.07:   Outstanding PhD Thesis Award, Chinese Academy of Sciences (80/year in UCAS+USTC) 中国科学院“优秀博士论文”（国科大+中科大80人/年） 🔍

• 2024.07:   Graduate Student Representative, University of Chinese Academy of Sciences (1/13691) 中国科学院大学 硕博研究生毕业生代表 (1/13691) 🔍

• 2024.06:   Outstanding Graduates in Beijing 北京市优秀毕业生

• 2024.06:   The President Award of the Chinese Academy of Sciences - Special Award (80/year in UCAS+USTC) 院长奖学金-特别奖（国科大+中科大80人/年） 🔍

• 2023.11:   “Pollyanna Chu” Scholarship for Distinguished Doctorates (Top 1%) 朱李月华优秀博士奖学金 (Top 1%)

• 2023.11:   China Education Development Foundation Integrated Circuit Personnel Training Project (EDA no more than 10 in China) 中国教育发展基金会“奋进奖学金–集成电路人才培养”计划 (EDA方向全国不超10人) 🔍

• 2022.11:   National Scholarship for Doctoral Students (Top 1%) 博士国家奖学金 (Top 1%)

• 2020.11:   National Scholarship for Graduate Students (Top 1%) 硕士国家奖学金 (Top 1%)

🏆 Competitions

• The International SAT Competition & Race 🏠
  • 2025: PRS won 3rd Place of Parallel Track.
  • 2024: PRS won 🥈Cloud Track
  • 2023: PRS won 🥇🥇🥇Main-Parallel(SAT/UNSAT/ALL) Track and 🥈Cloud Track
  • 2022: ParKissat-RS won Chinese First 🥇🥇🥈Main-Parallel(SAT/ALL) Track; kissat-pre won 🏆NoLimits Track; kissat-inc won 🥈🥈Main-Sequential(SAT/ALL) Track
  • 2021: lstech_Maple won 🥈Main-Sequential(SAT) Track; kissat_bonus won 🥈Main-Sequential(UNSAT) Track;
  • 2020: Relaxed_LCMDCBDL_newTech won 🥇Main-Sequential-SAT Track
  • 2018: ReasonLS won 🏆NoLimits Track
  • Sparkle SAT Challenge 2018 🏠: ReasonLS won the 🥈second place.
• International Satisfiability Modulo Theories (SMT) Competition 🏠
  • 2023: z3++ won 🏆MV-Biggest Lead & MV-Largest Contribution & 🏆QF-LIA(;,‖,T,mv), QF_NLIA(;,‖,T,⊥,24), QF_NIA(;,‖,T), QF_IDL(⊥) 📽️Video
  • 2022: z3++ won 🏆MV-Biggest Lead & 🏆MV-Largest Contribution
  • 2021: YicesLS won 🏆QF-IDL Model Validation & Single Query
• FLoC (Federated Logic Conference) 2022 Olympic Games 🏠
  • SAT: ParKissat-RS won 🏆Parallel Track
  • SMT: z3++ won 🏆MV-Biggest Lead & 🏆MV-Largest Contribution
• China Postgraduate IC Innovation Competition EDA Elite Challenge
  • 2025, 🥉Third Prize
  • 2024, 🥈Second Prize, 🏢 Enterprise Special Award (S2C)
  • 2022, Integrated Circuit EDA Elite Challenge, 🥈Second award, 🏢 Enterprise Special Award (Hisilicon)

• 2023, The 6th “Qiangwang Cup” National Network Security Challenge, Cryptography Mathematics Special Competition, Group Name: “CMixSAT”, 🏆 Champion

• 2017, Interdisciplinary Contest In Modeling, Meritorious Winner

• 2016, Contemporary Undergraduate Mathematical Contest in Modeling (CUMCM), 🥈 Second prize

• 2016, International Genetically Engineered Machine competition (iGEM), 🥇 Gold Award

📝 Publications

† Co-First Author; * Corresponding Author;

Conference Papers

[C3] SAT 2021

[C3] Deep Cooperation of CDCL and Local Search for SAT

Shaowei Cai†*, Xindi Zhang† 2021.07, pp 64–81 💾code

(Best Paper Award)🏆

[Projects]

💾Relaxed-LCMDCBDL-newTech 🥇

💾LSTech-Maple 🥈

💾kissat-pre 🥇; 💾kissat-inc 🥈

• [C15] ASE 2025 SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization
  Chuan Luo, Shaoke Cui, Jianping Song, Xindi Zhang*, Wei Wu, Chanjuan Liu, Shaowei Cai, Chunming Hu.

• [C14] CP 2025 DynamicSAT: Dynamic Configuration Tuning for SAT Solving.
  Zhengyuan Shi, Wentao Jiang, Xindi Zhang*, Jin Luo, Yun Liang, Zhufei Chu, Qiang Xu*. 💾DynamicSAT

• [C13] DAC 2025 PastATPG: A Hybrid ATPG Framework for Better Test Compaction with Partial Assignment SAT.
  Zhiteng Chao†, Xindi Zhang†, Xinyu Zhang, Jianan Mu*, Zizhen Liu, Shaowei Cai*, Jing Ye, Xiaowei Li and Huawei Li*.
  💾PastATPG 💾PA-Minisat

• [C12] DAC 2025 Leveraging Critical Proof Obligations for Efficient IC3 Verification.
  Lingfeng Zhu, Xindi Zhang, Yongjian Li* and Shaowei Cai.
  💾MCer

• [C11] DAC 2025 X-SAT: An Efficient Circuit-Based SAT Solver.
  Yuhang Qian, Zhihan Chen, Xindi Zhang and Shaowei Cai*.
  💾X-SAT

• [C10] DAC 2025 Parallel Dynamic Partitioning for Datapath Combinational Equivalence Checking.
  Shuai Zhou, Weikang Zhang, Xindi Zhang, Zite Jiang, Haihang You* and Shaowei Cai*.

• [C9] ICSE 2024 Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory.
  Xindi Zhang, Bohan Li, Shaowei Cai*. 2024.03 (Article No.: 125, Pages 1–13)
  💾hybridSMT 💾z3++ 🎞️Slides

• [C8] ASP-DAC 2024 A Fast Test Compaction Method for Commercial DFT Flow Using Dedicated Pure-MaxSAT Solver.
  Zhiteng Chao, Xindi Zhang, Junying Huang, Jing Ye*, Shaowei Cai, Huawei Li, Xiaowei Li*. 2024.03 (pp. 503-508)

• [C7] ICCAD 2023 Integrating Exact Simulation into Sweeping for Datapath Combinational Equivalence Checking.
  Zhihan Chen, Xindi Zhang, Yuhang Qian, Qiang Xu, Shaowei Cai*. 2023.10 (pp. 1-9)
  💾hybridCEC 🎞️Slides

• [C6] CP 2023 Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper).
  Shaowei Cai, Chuan Luo, Xindi Zhang and Jian Zhang. 2023.07 (pp. 5:1-5:10)
  💾CNC

• [C5] CAV 2022 Local Search For SMT on Linear Integer Arithmetic.
  †Shaowei Cai*, Bohan Li, Xindi Zhang. 2022.08, (pp. 227-248)
  💾z3++

• [C4] IJCAI 2022 Deep Cooperation of CDCL and Local Search for SAT (Extended Abstract).
  Shaowei Cai, Xindi Zhang. 2022 (pp. 5274-5278)
  💾code

• [C2] CP 2020 Pure MaxSAT and Its Applications to Combinatorial Optimization via Linear Local Search.
  Shaowei Cai*, Xindi Zhang. 2020.09 (pp. 90-106)
  💾LinearLS

• [C1] IJCAI 2020 NuCDS: An Efficient Local Search Algorithm for Minimum Connected Dominating Set.
  Bohan Li, Xindi Zhang, Shaowei Cai*, Jinkun Lin, Yiyuan Wang, Cristain Blum. 2020, (pp. 1503-1510)
  💾NuCDS

Journal Papers

• [J7] TODAES Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization.
  Zhihan Chen, Xindi Zhang, Yuhang Qian, Shaowei Cai*.
  💾ParaHCEC

• [J6] JOS Cold Restart for CDCL Algorithms.
  Xindi Zhang, Zhihan Chen, Shaowei Cai*.

• [J5] COR A fast local search algorithm for minimum sum coloring problem on massive graphs
  Yan Li, Mengyu Zhao, Xindi Zhang, Yiyuan Wang*. 2024.09 (Vol. 172 (2024), 106794)

• [J4] Integration A fast test compaction method using dedicated Pure MaxSAT solver embedded in DFT flow
  Zhiteng Chao, Xindi Zhang, Junying Huang, Zizhen Liu, Yixuan Zhao, Jing Ye, Shaowei Cai*, Huawei Li*, Xiaowei Li. 2024.08 (Vol. 100 (2024): 102265.)

• [J3] ToCL Local Search For Satisfiability Modulo Integer Arithmetic Theories.
  †Shaowei Cai*, Bohan Li, Xindi Zhang. 2023.07 (Vol 24(4): No.32, pp. 1-26)
  💾z3++

• [J2] JAIR Better Decision Heuristics in CDCL through Local Search and Target Phases.
  Shaowei Cai*, Xindi Zhang, Mathias Fleury, Armin Biere. 2022.08 (Vol. 74 (2022):1515-1563.)
  💾code

• [J1] JAIR Efficient Local Search based on Dynamic Connectivity Maintenance for Minimum Connected Dominating Set.
  Xindi Zhang, Bohan Li, Shaowei Cai*, Yiyuan Wang*. 2021.05 (Vol. 71 (2021), pp. 81-119)
  💾FastCDS 💾NuCDS

Thesis

• [D] ISCAS Hybrid Algorithms for SAT and SMT and Their Applications
  Xindi Zhang. 2024.05 (ISCAS PHD Thesis)
  🎞️Slides

📖 Educations

• Jul. 2024 - Now:2024年7月 - 至今： Special Research Assistant (Post-Doctor), Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China. 特别研究助理，重点实验室党支部副书记，博士后，基础软件与系统重点实验室（中国科学院）与计算机科学国家重点实验室，中科院软件所，北京，中国。

• Aug. 2018 - Jun. 2024:2018年8月 - 2024年6月： M.S. & Ph.D. student, (Supervisor: Prof. Shaowei Cai), State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China. 硕博连读（导师：蔡少伟研究员），中科院软件所计算机科学国家重点实验室，北京，中国。

• Aug. 2014 - Jul. 2018:2014年8月 - 2018年7月： B.Eng. in Software Engineering, College of Software; B.A. in Finance, School of Economics. Jilin University, Changchun, China. 软件工程（卓越工程师培养计划）学士，软件学院；金融学学士，经济学院。吉林大学，长春，中国。

💬 Talks

• 2025.11–2025.12, “SAT求解及EDA形式化技术简述”, 东北师范大学, 吉林大学, 西南交通大学, 西华大学, 等 🎞️Slides

• 2025.11, “异构并行SAT求解及组合等价性验证”, ChinaSoft 2025, 🎞️Slides

• 2025.11, “EDA形式化验证的并行算法”, ChinaSoft 2025, 🎞️Slides

• 2025.08 “CCF形式化方法专委会青年学术论坛–形式化方法在基础软件中的应用”. 🎥Video

• 2025.05, “Advances on SAT and Equivalence Checking”, ISEDA 25 🎞️Slides

• 2024.08, “SAT求解及其EDA应用简述”, Institute of Computing Technology, Chinese Academy of Sciences, 🎞️Slides

• 2024.06, “坐稳“冷”板凳，在不变中拥抱变化”, Institute of Computing Technology, Chinese Academy of Sciences, 🎞️Slides

• 2024.05, “SAT求解及其EDA应用简述”, Huawei, 🎞️Slides

• 2024.05, “Practical Boolean SAT Solving Techniques”, ISEDA 24, 🎞️Slides

• 2023.12, “Hybrid Solvers, Preprocessing, and Parallel Solvers for SAT/SMT”, KouShare, 🎞️Slides 📽️Video

• 2023.07, “SAT并行求解与密码学求解应用”, 🎞️Slides