【08-31】SKLCS Seminar on”Integrating SAT Techniques in Hard Problem Solving”

Title: Integrating SAT Techniques in Hard Problem Solving
Speaker: Chu-Min Li（Professor，University of Picardie Jules Verne, France）
Time: 2023年8月31号（周四），10:00-11:30am
Venue: 中科院软件所5号楼三层334报告厅
Abstract: Propositional satisfiability (SAT) is the first problem shown to be NP-complete, due to its expressive power and its simplicity. Over the last few decades, SAT solvers have had a dramatic impact on many real-world applications, usually by encoding the real-world problems into SAT and then calling SAT solvers to solve the obtained SAT instances. In this talk, we argue that a probably more efficient approach to solve a problem is not to encode it into SAT, but to enhance a dedicated solver with SAT techniques. We present the works in this direction by distinguishing two cases: (1) the problem can naturally be encoded into SAT, (2) the problem cannot directly be encoded into SAT. Each case will be illustrated using one or two examples.
Bio: Chu-Min Li is a professor of computer science in University of Picardie Jules Verne in France, and he is also one of the 40 AI chairs in France. His research interests include fast propositional reasoning and its applications in efficient SAT and MaxSAT solver development and in solving other hard combinatorial problems such as graph coloring and MaxClique. As achievements, he won several gold medals in SAT competitions, including the gold medal of the 20th anniversary track of SAT competition 2022, and he refuted a prevailing opinion in MaxSAT community saying that branch-and-bound is not adequate for real-world applications, by developing the first branch-and-bound MaxSAT solver competitive for industrial MaxSAT instances. He is Program Chair of SAT’21 and associate editor of JAIR and IJAIT.