The Organizing Committee of the SAT Competition (2017) announced the results of the 20th International SAT Competition on its official website on September 15 (the results of the competition were also released in the International Conference on Theory and Applications of Satisfiability Testing (SAT 2017)). The competition organizers announced that the team from Professor Li Chu-Min from our School of Computer Science won the championship in the main track of the competition with a big advantage (the submitted four solvers got the first four places).
SAT problem, Satisfaction (SATisfiability) problem, is the first problem in the history that has been proven to be NP-complete. It is also the core-challenging problem in the field of artificial intelligence, and has very important significance and extensive applications in many industrial applications. For a long time, researchers have conducted extensive and in-depth research on it, and SAT competition has become a landmark academic event in this field. The SAT competition has been held every two years since 1992 and has been lasting for 20 years. The competition was intensively paid attention to by top researchers in both academia and industry. A total of 28 teams from 14 countries participated in the competition. The participating universities include New York University, University of Wisconsin, University of Waterloo in Canada, University of Linz in Belgium, University of Leuven, University of Technology in Sydney, and so on. There are also top Chinese universities and research institutes from Tsinghua University, Peking University, Chinese Academy of Sciences and other universities. This competition consists of six tracks: Main, Parallel, Incremental, Agile, Random, No-limits and so on. Among them, the Main track is focused on the solution to the challenging problems from various industrial applications. It is the most concerned and competitive track in the SAT competition.
The institute of theory in our school of computer science has a deep accumulation and in-depth research on various types of combinatorial optimization problems, such as SAT problem, and has a good reputation in this field. This is a new achievement obtained by our university following Professor Huang Wenqi who won the championship of the SAT competition in 1996. Our university’s team members include Professor Li Chu-Min, Professor Lu Zhipeng, Ph.D candidates Xiao Fan and Luo Mao and so on.
In addition, in the recent landmark conference in artificial intelligence, the 26th the International Joint Conference on Artificial Intelligence (IJCAI2017, August 19-25, Melbourne, Australia), the same team members reported the latest research outcomes on the SAT problem: An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers, (IJCAI2017, 703-711). Our school of computer science is the first affiliation with Ph.D candidate Luo Mao as the first author. The submitted solvers are based on this research work reported in IJCAI 2017.