I am now a Special Research Assistant (post-doctor) in 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

• 2024.08:  🎉🎉 国际SAT比赛Cloud赛道亚军
• 2024.07:  🎉🎉 中国科学院大学2024年毕业典礼，研究生代表
• 2024.06:  🎉🎉 “中国科学院大学 院长奖-特别奖”
• 2024.05:  🎉🎉 ISEDA talk: “Practical Boolean SAT Solving Techniques”.

📝 Publications

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 🥈

• COR [J] 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)

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

• ISCAS Hybrid Algorithms for SAT and SMT and Their Applications Xindi Zhang, 2024.05 (ISCAS phd thesis) 🎞️Slides

• 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

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

• 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

• 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

• ToCL [J] 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++

• JAIR [J] 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

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

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

• JAIR [J] 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

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

• 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

🎖 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

• 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 and Work Experience

• 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