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

Recently, MaxSAT reasoning has been shown tobe powerful in computing upper bounds for the cardinalityof a maximum clique of a graph. However, existing upperbounds based on MaxSAT reasoning have two drawbacks: (1)at every node of the search tree, MaxSAT reasoning has to beperformed from scratch to compute an upper bound and istime-consuming, (2) due to the NP-hardness of the MaxSATproblem, MaxSAT reasoning generally cannot be complete at anode of a search tree, and may not give an upper bound tightenough for pruning search space. In this paper, we proposean incremental upper bound and combine it with MaxSATreasoning to remedy the two drawbacks. The new approach isused to develop an efficient branch-and-bound algorithm forMaxClique, called IncMaxCLQ. We conduct experiments toshow the complementarity of the incremental upper bound andMaxSAT reasoning and to compare IncMaxCLQ with severalstate-of-the-art algorithms for MaxClique.