Shaowei Cai

Professor

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China

Email: shaoweicai.cs@gmail.com; caisw@ios.ac.cn

My research focus on Constraint Solving (particularly SAT, SMT, and integer programming) and formal verification, as well as their applications in industries. 

中文主页

Publications

For published papers, please visit my DBLP and Google Scholar Citations

Talks

• A Tutorial on SAT Solving, 6th Indian Winter SAT+SMT School, Inviated talk
• Configuration Checking Based Local Search, 14th Annual Symposium on Combinatorial Search (SOCS 2021), Invited talk
  ( Configuration Checking is a generic idea for local search algorithms to address the cyclying issue.) 
• Local Search and Its Application in CDCL/CDCL(T) for SAT and SMT, 23th Formal Methods in Computer-Aided Design (FMCAD 2023), Invited tutorial
• Distributed SMT Solving Based on Variable-level Partitioning, 36th International Conference on Computer Aided Verification (CAV 2024), Distinguished Paper Award.  

A Graduate Course in Constraint Solving

• Beginning And Constraint Models
• SAT Solving: Basis And CDCL
• SMT Solving: DPLL(T) And Eager Encoding
• SMT Solving: Combined Theories

Research

The codes in our group can be found here: https://github.com/shaowei-cai-group

• Satisfiability Solving
• Combinatorial Optimization
  

Winning awards 

• Distinguished Paper Award, “Distributed SMT Solving Based on Dynamic Variable-level Partitioning”, CAV 2024
• Best Paper Award, “An Efficient Local Search Solver for Mixed Integer Programming”, CP 2024
• Best Paper Award, "Deep Cooperation of CDCL and Local Search for SAT", SAT 2021
• Our SAT solvers have won more than 10 Gold medals in Main tracks and parallel Main tracks in SAT Competitions; particularly, our parallel SAT solver named PRS won all parallel tracks and ranked 2nd in Cloud track in SAT Competition 2023. 
• Our SMT solver Z3++ have won "Biggest Lead" and "Largest Contribution" in Model Validation track over all theories in SMT Competition 2022 and 2023. Particularly, Z3++ won many tracks of LIA, NIA, NRA Divisions.