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 of 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, the Satisfaction (SATisfiability) problem, is the first problem in history that has been proven to be NP-complete. It is also a 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, the University of Wisconsin, the University of Waterloo in Canada, the University of Linz in Belgium, the University of Leuven, the University of Technology in Sydney, and so on. There are also top Chinese universities and research institutes from Tsinghua University, Peking University, the 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 concerning 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 problems, 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 affiliated with Ph.D. candidate Luo Mao as the first author. The submitted solvers are based on this research work reported in IJCAI 2017.
