IncMaxCLQ

MaxCLQ for MaxClique. Combining Incremental Upper Bound and MaxSAT reasoning for MaxClique. MaxSAT reasoning is 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 a node of a search tree, and may not give an upper bound tight enough for pruning search space. We thus 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, which is very efficient and closes an additional DIMACS instance (hamming10-4.clq) in less than 7 days on an INTEL XEON E5-2680 (2.7Ghz, 20M Cache and 16GB memory) under Linux.