报告人
Shuolin Li
Aix-Marseille University
时间
2025年12月2日 星期二
下午 14:00-15:00
地点
602会议室
Abstract
Boolean satisfiability (SAT) and Maximum Satisfiability (MaxSAT) have become central pillars of modern combinatorial reasoning. Beyond their theoretical significance—being canonical NP-complete and NP-hard problems—they now serve as general-purpose engines that drive progress in verification, artificial intelligence, planning, bioinformatics, and industrial optimization. State-of-the-art SAT and MaxSAT solvers operate by constructing a binary assignment tree, whose size is determined by both the number of variables and the depth of the search. In this talk, I present several techniques for reducing this search tree and accelerating the solving process. These techniques have been experimentally validated to be highly effective.
Biography
Shuolin Li is currently a post-doctoral researcher at Aix-Marseille University, working with Professors Chu-Min Li and Professors Djamal Habet. Her research focuses on exact solving techniques for SAT and MaxSAT and their industrial applications, with a particular interest in understanding the differences between various reasoning methods. Her work has been published in top-tier conferences such as AAAI and IJCAI. She has also developed SAT and MaxSAT solvers that have consistently ranked in the top three in international SAT or MaxSAT competitions over the past four years, including winning three first-place awards.
