I am now a Special Research Assistant (post-doctor) in Constraint Solving Lab, Key Laboratory of Systems Software, 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:  🎉🎉 4 papers have been accepted by DAC（CCF-A）
• 2024.12:  🎉🎉 中国研究生创“芯”大赛·EDA精英挑战赛 二等奖 + 企业特别奖
• 2024.08:  🎉🎉 Second Place in SAT Competition Cloud Track
• 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*. 💾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*.

• [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 (59 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 (EDA no more than 10 in China)(“奋进奖学金–集成电路人才培养”)🔍
• 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 (中国研究生创“芯”大赛 EDA精英挑战赛), 🥈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

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

• 2024.08, “Introduction of SAT and its Applications in EDA”, 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