Affiliated with the Key Laboratory of Basic Software and Systems of the Chinese Academy of Sciences (National Key Laboratory of Computer Science), the Constraint Solving Research Lab focuses on algorithm research and practical applications of constraint solvers and formal methods.
Constraint solvers are key technologies for ensuring the reliability of software and hardware, serve as the computational engine for formal methods, and have wide applications in information security, such as cryptanalysis and various intelligent decision-making scenarios. We pursue extreme performance improvements by exploring combinations of different methods and enhancing scalability to adapt to high-performance computing platforms.
Particularly, we focus on the following areas:
We develop efficient algorithms for Boolean satisfiability problems, including local search, hybrid approaches, and distributed solving techniques.
Our research extends SAT solving with additional theories, enabling solutions for more complex logical formulas through specialized algorithms and distributed computing.
We tackle mathematical programming challenges through various approaches including Pseudo-Boolean Optimization, Mixed Integer Programming, and Integer Linear Programming.
We also dedicate to the application of constraint solving in Electronic Design Automation (EDA), including:
Electronic Design Automation (EDA)
We develop formal verification and testing tools for hardware design, including Logic Equivalence Checking, Model Checking (BMC and PDR), and Automatic Test Pattern Generation.