Combining MaxSAT Reasoning and Incremental Upper Bound for the Maximum Clique Problem

Recently, MaxSAT reasoning has been shown to be powerful in computing upper bounds for the cardinality of a maximum clique of a graph. However, existing upper bounds based on MaxSAT reasoning have two drawbacks: (1)at every node of the search tree, MaxSAT reasoning has to be performed from scratch to compute an upper bound and is time-consuming, (2) due to the NP-hardness of the MaxSAT problem, MaxSAT reasoning generally cannot be complete at anode of a search tree, and may not give an upper bound tight enough for pruning search space. In this paper, we propose an incremental upper bound and combine it with MaxSAT reasoning to remedy the two drawbacks. The new approach is used to develop an efficient branch-and-bound algorithm for MaxClique, called IncMaxCLQ. We conduct experiments to show the complementarity of the incremental upper bound and MaxSAT reasoning and to compare IncMaxCLQ with several state-of-the-art algorithms for MaxClique.