M. Zhiwen Fang soutiendra le vendredi 10 juin 2016 à 9h une thèse d’Informatique de l’Université de Picardie Jules Verne (Pôle Scientifique - Bâtiment Ecole des Minimes - salle des thèses - en visioconférence) ayant pour thème «Exact Algorithms for the Maximum Clique Problem».
Le jury sera composé de M. Jian Zhang (Institute of Software, Chinese Academy of Sciences - Beijing - Chine), M. Felip Manya (IIIA-CSIC Campus de la UAB, Barcelone - Espagne), M. Chu-Min Li (Université de Picardie Jules Verne), M. Gilles Dequen (Université de Picardie Jules Verne), M. Hai-Jun Zhou (Institute of Theoretical Physics, Chinese Academy of Sciences, Beijin - Chine), M. Xiaoming Sun (Institute of Computing Technology, Chinese Academy of Sciences, Beijing - Chine).
Abstract
The PhD thesis of M. Fang Zhiwen is on the exact resolution of the MaxClique problem based on MaxSAT reasoning. MaxClique is a typical NP-hard problem consisting in finding a maximum clique in a graph, in which every two vertices are connected. MaxClique is important in algorithm complexity theory and also has numerous practical applications, the interest in this problem is growing with more and more applications in domains such as social networks, scientific computation networks and wireless sensor networks.
There are two contributions in this thesis.
The first contribution is the combining of an incremental upper bound with MaxSAT reasoning in a branch-and-bound algorithm to solve MaxClique. MaxSAT reasoning consists in encoding MaxClique into propositional logic, in which each boolean variable represents a vertex and each clause specifies a relation among some vertices, and then identifying those vertices that cannot belong to a maximum clique by propositional deduction. MaxSAT reasoning allows to reduce the search space of the branch-and-bound algorithm effectively. However, it is time-consuming and connot be done completely. Fang Zhiwen proposes an incremental upper bound allowing to expoit the results of previous MaxSAT reasoning on subgraphs, which may allow to reduce more search space than MaxSAT reasoning from sketch on the current graph. The resulting MaxClique algorithm is substantially faster than state-of-the-art algorithms for MaxClique. In addition, Fang Zhiwen discovered a new vertex ordering allowing to solve a broad class of MaxClique instances several orders of magnitude faster.
The second contribution consists in finding a clique with the maximum total weight (MWC, short for Maximum Weight Clique) in a graph in which each vertex is associated a weight. In this work, Fang Zhiwen introduces a new weighted partial MaxSAT formalism called Literal Weighted MaxSAT (LW MaxSAT) to encode a MWC problem, in which not only the soft clauses are weighted as in existing weighted partial MaxSAT formalisms, the literals in soft clauses are also weighted. Then he extends MaxSAT reasoning by introducing two notions called Top-k literal failed clause and Top-k empty clause respectively, and by defining two transforming rules to split a clause on demand to handle both clause weights and literal weights. The extended MaxSAT reasoning allows to identify efficiently and effectively many vertices that cannot belong to a maximum weight clique, so that the search space can be greatly reduced. The resulting algorithm substantially outperforms the state-of-the-art algorithms on the vast majority instances in the litterature. It is especially effective in solving hard instances.
