Shaowei Cai

Research Areas

• Constraint Solving
• Operations Research Optimization
• EDA (Electronic Design Automation) Verification

Major Academic Achievements

• Constraint Solving: Including Boolean Satisfiability Problem (SAT), Satisfiability Modulo Theories (SMT), Maximum Satisfiability Problem (MaxSAT), etc., which are core technologies in software and hardware verification, information security, and other domains. From independent development to leading a team, Prof. Cai has won multiple championships in SAT and SMT competitions over consecutive years, including the first SAT competition championship by a Chinese team (2012) and the first SMT competition championship by a Chinese team (2021). His team has consistently won championships in various tracks of MaxSAT competitions from 2013-2023, maintaining the title in the incomplete track for multiple years. He has received multiple Joint Logic Olympiad gold medals. For SAT problems, he proposed a hybrid solving method of CDCL + local search sampling, addressing the 7th challenge of the ten challenges in propositional logic reasoning and search, winning the Best Paper Award at SAT 2021 conference. For SMT problems, he designed the first local search algorithm supporting arithmetic theories, and developed the Z3++ solver in collaboration with Z3, winning the largest lead award and greatest contribution award in the model validation track of the SMT competition in 2022 and 2023. He achieved breakthroughs in distributed constraint solvers, leading the team to develop parallel and distributed SAT solvers, SMT solvers, and MaxSAT solvers, solving numerous previously unsolved instances. Related papers received the CAV 2024 Distinguished Paper Award.

• Operations Research and Optimization: He designed efficient local search algorithms and simplification algorithms for various renowned combinatorial optimization problems such as maximum clique, graph coloring, vertex cover, set covering, and other NP-hard problems, maintaining cutting-edge solving performance. He proposed the configuration checking strategy that effectively addresses a major deficiency in local search—cycling phenomenon—which has been widely applied to various NP-hard combinatorial optimization problems. He designed “search and reasoning” semi-exact algorithms that can solve graph optimization problems with tens of millions of vertices on sparse instances in seconds. He developed mixed-integer (linear and non-linear) programming solvers with fast-solving capabilities superior to the commercial solver Gurobi on standard test sets, breaking numerous records on challenging instances. These technologies have been applied to practical scenarios such as EDA layout and internet advertising. His papers have been published in top conferences such as KDD and CP, receiving the Best Paper Award at CP 2024.

• Formal Verification: He customized solvers for EDA and operating system verification, which have been applied in multiple enterprises. He led the team to independently develop hardware formal verification tools, including circuit equivalence verification tools, Model Checking tools, and ATPG tools, outperforming open-source tools on real circuit datasets. The team has also conducted cache protocol verification for open-source processors such as the Xiangshan Processor, identifying multiple deadlock errors and mutual exclusion errors, and proposing correction solutions. He developed efficient SMT solving algorithms, customized incremental SMT solving and lightweight SMT solving, enhancing the performance of operating system verification tools and applying them to automatic page layout in operating systems.

His research has been published in top journals and conferences including ACM Transactions on Computational Logic, Artificial Intelligence, IEEE Transactions on Computers, CAV, DAC, ICCAD, SAT, CP, AAAI, and other leading venues in relevant fields. The solvers and formal tools developed have enhanced chip verification and software verification capabilities and have been adopted by numerous companies. The related technologies have been applied across multiple industries, with projects in EDA, software verification, cloud computing, banking system optimization, operations scheduling, and smart campus management.