Xindi Zhang(张昕荻)’s Homepage

I am now a Ph.D. student in State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China. My supervisor is Prof. Shaowei Cai.

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

Educations

  • Aug. 2018 - now. M.D & Ph.D. student, 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.

Awards and Hornors

  • 2023, CCF Chinasoft, Outstanding Doctoral Representative (A total of 14 people in China)

  • 2023, “FenJin” (Endeavor in English) Scholarship – Integrated Circuit Personnel Training Project (A total of 95 people in China)

  • 2023,”Pollyanna Chu” Scholarship for Distinguished Doctorates (A total of 300 people in CAS)

  • SAT Competition 2023. Presentation of Results, PRS-sc23.
    • Main-Parallel-Track (ALL, SAT, UNSAT) Gold Medal *3
    • Cloud-Track, Siver Medal
  • SMT Competition 2023. Presentation, Results, z3++
    • Biggest Lead Model Validation
    • Largest Contribution Model Validation
    • Winner of QF-LIA(;,‖,T,mv), QF_NLIA(;,‖,T,⊥,24), QF_NIA(;,‖,T), QF_IDL(⊥)
  • 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)

  • SAT Competition 2022 & Floc, Presentation of Results, kissat_inc, parkissat_rs
    • Floc: SAT Competition 2022 Parallel track, Gold Medal
    • Main-Parallel-Track, Main-Parallel-Track-SAT, Gold Medal
    • NoLimits Track, Winner
    • Main-Parallel-Track-UNSAT, Silver Medal
    • Main-Track, Main-Track-SAT, Silver Medal
  • SMT Competition 2022 & FLoC, Presentation of Results, z3++
    • Gold Biggest Lead Model Validation: Z3++, Gold Medal
    • Glod Largest Contribution Model Validation: Z3++, Gold Medal
    • Single Query Track: QF-NIA(UNSAT parallel), QF-NRA/QF-LIA(SAT parallel), QF-IDL(ALL); Model Validation Track: QF-LIA(ALL), QF-IDL(ALL), First Rank
  • SAT Competition 2021, Presentation of Results
    • Main-Track-SAT, Main-Track-UNSAT, Silver Medal
    • 2021, SAT Cometition 2021 Crypto (Cadical Hack), Honorable Mentions]
  • SMT Competition 2021, Presentation of Results
    • QF_IDL(ALL) Model Validation Track, Single Query Track, Winner
  • SAT Competition 2020, Presentation of Results, Relaxed_newTech
    • Main-Track-SAT, Gold Medal
    • Main-Track, Silver Medal
  • SAT Competition 2018 NoLimit-Track, Winner.
  • Sparkle SAT Challenge, 2018, Second Place.

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

  • National Scholarship for Doctoral Students, and National Scholarship for Master’s Students

Publications

  • [C9] *Shaowei Cai, Xindi Zhang. Deep Cooperation of CDCL and Local Search for SAT. In SAT 2021: 64-81. co-1st author, [Best Paper Award].

  • [C8] Xindi Zhang, Bohan Li, Shaowei Cai. Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory. In ICSE 2024.

  • [C7] Zhiteng Chao, Xindi Zhang, Junying Huang, Jing Ye, Shaowei Cai, Huawei Li, Xiaowei Li. A Fast Test Compaction Method for Commercial DFT Flow Using Dedicated Pure-MaxSAT Solver. In ASP-DAC 2024.

  • [C6] Zhihan Chen, Xindi Zhang, Yuhang Qian, Qiang Xu, Shaowei Cai. Integrating Exact Simulation into Sweeping for Datapath Combinational Equivalence Checking. In ICCAD 2023: 1-9.

  • [J3] *Shaowei Cai, Bohan Li, Xindi Zhang. Local Search For Satisfiability Modulo Integer Arithmetic Theories. TOCL, 2023, 24(4): 1-26. co-1st author

  • [J2] Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere. Better Decision Heuristics in CDCL through Local Search and Target Phases. JAIR.74 (2022):1515-1563. 1st student author

  • [C5] *Shaowei Cai, Bohan Li, Xindi Zhang. Local Search For SMT on Linear Integer Arithmetic. In CAV 2022:227-248. co-1st author

  • [C4] Shaowei Cai, Xindi Zhang. Deep Cooperation of CDCL and Local Search for SAT (Extended Abstract)*. In IJCAI 2022:5274-5278 . 1st student author

  • [J1] Xindi Zhang, Bohan Li, Shaowei Cai, Yiyuan Wang. Efficient Local Search based on Dynamic Connectivity Maintenance for Minimum Connected Dominating Set. JAIR.71(2021):89-11. 1st author

  • [C3] Shaowei Cai, Chuan Luo, Xindi Zhang and Jian Zhang. Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper). In CP 2021: 5:1-5:10. Only student author

  • [C2] Shaowei Cai, Xindi Zhang. Pure MaxSAT and Its Applications to Combinatorial Optimization via Linear Local Search. In CP 2020: 90-106. 1st student author

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

*Sorted by the Last Name

System Documents

  • *Shaowei Cai, Bohan Li, Bohua Zhan, Xindi Zhang, Mengyu Zhao. Z3++ at SMT-COMP 2023. In SMT Competition 2023. (co-1st author)

  • Zhihan Chen, Xindi Zhang, Yuhang Qian, Shaowei Cai. PRS: A new parallel/distributed framework for SAT. In SAT Competition 2023.

  • *Shaowei Cai, Bohan Li, Jinkun Lin, Zhonghan Wang, Bohua Zhan, Xindi Zhang, Mengyu Zhao. Z3++ at SMT-COMP 2022. In SMT Competition 2022. (co-1st author)

  • Zhihan Chen, Xindi Zhang, Shaowei Cai, Pinyan Lu. CDCL Solvers with Improved Local Search Cooperation and Pre-processing. In SAT Competition 2022. (co-1st author)

  • Xindi Zhang, Zhihan Chen, Shaowei Cai. ParKissat: Random Shuffle Based and Pre-processing Extended Parallel Solvers with Clause Sharing. In SAT Competition 2022.

  • Xindi Zhang, Zhihan Chen, Shaowei Cai. Improving CDCL via Local Search. In SAT Competition 2021.

  • *Shaowei Cai, Bohan Li, Xindi Zhang. YicesLS on SMT COMP2021. In SMT Competition 2021.

  • Xindi Zhang, Shaowei Cai. Relaxed backtracking with rephasing. In SAT Competition 2020.

  • Shaowei Cai, Xindi Zhang. ReasonLS. In SAT Competition 2018.

*Sorted by the Last Name

Softwares

Some open-source softwares can be found in caisw-group or Homepage of Shaowei Cai.