I am now a Special Research Assistant (post-doctor) in Constraint Solving Lab, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China.

My cooperating mentor is is Prof. Shaowei Cai (蔡少伟).

My research interests are SAT, SMT, EDA and etc.

🔥 News

• 2025.02:  🎉🎉 四篇论文被DAC（CCF-A）接收
• 2024.12:  🎉🎉 中国研究生创“芯”大赛·EDA精英挑战赛 二等奖 + 企业特别奖
• 2024.08:  🎉🎉 国际SAT比赛Cloud赛道亚军
• 2024.07:  🎉🎉 中国科学院大学2024年毕业典礼，研究生代表
• 2024.06:  🎉🎉 “中国科学院大学 院长奖-特别奖”
• 2024.05:  🎉🎉 ISEDA talk: “Practical Boolean SAT Solving Techniques”.

📝 Publications

[C3] SAT 2021

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 🥈

• [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*.

• [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*.

• [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.)

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

• [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

• [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

• [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

• [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

• [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

‡ Sorted by the Last Name; † Co-First Author; * Corresponding Author;

🎖 Honors and Awards

• 2024.07, Graduate Student Representative, University of Chinese Academy of Sciences (1/13691)🔍
• 2024.06, Outstanding Graduates in Beijing
• 2024.06, The President Award of the Chinese Academy of Sciences - Special Award (58 students in CAS) 🔍
• 2023.12, CCF Chinasoft, Outstanding Doctoral Representative (14 students in China)
• 2023.11, “Pollyanna Chu” Scholarship for Distinguished Doctorates (Top 1%)
• 2023.11, “FenJin” Scholarship – Integrated Circuit Personnel Training Project (95 students in China, EDA no more than 10%)🔍
• 2022.11, National Scholarship for Doctoral Students (Top 1%)
• 2020.11, National Scholarship for Graduate Students (Top 1%)

Competitions Awards

• The International SAT Competition & Race 🏠Homepage
  • 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 🏠Homepage
  • 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 🏠Homepage
  • SAT: ParKissat-RS won 🏆Parallel Track
  • SMT: z3++ won 🏆MV-Biggest Lead & 🏆MV-Largest Contribution

• 2024, China Postgraduate IC Innovation Competition EDA Elite Challenge, 🥈Second award, 🏢 Enterprise Special Award (S2C)

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

• 2022, Integrated Circuit EDA Elite Challenge, 🥈Second award, 🏢 Enterprise Special Award (Hisilicon)

• 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

📖 Educations

• Jul. 2024 - Now, 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, M.D & 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, B.Eng. in Software Engineering, College of Software; B.A. in Finace, School of Economics. Jilin University, Changchun, China.

💬 Talks

• 2024.08, “Introduction of SAT and its Applications in EDA”, Institute of Computing Technology, Chinese Academy of Sciences, 🎞️Slides

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

• 2024.05, “SAT Solving and its Applications in 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.12 “Intriduction of SAT Studies & PhD Thinking” CCF-ChinaSoft, 🎞️Slides

• 2023.09 “Integrating Exact Simulation into Sweeping for Datapath Combinational Equivalence Checking” ICCAD 2023, 🎞️Slides