Abstract

The maximum clique problem has a history similar to that of SAT solving: following the introduction of a standard file format and a first set of benchmark instances in the second DIMACS implementation challenge in 1992, practitioners have produced a series of algorithm implementations that can solve more and more of these benchmark instances using less time. We have also seen new applications arise, particularly in computational biology and chemistry, where the maximum clique problem is used via an encoding to solve maximum common subgraph problems. I'll give an overview of one family of clique solving algorithms, with an emphasis on using empirical algorithmics techniques to understand what makes clique instances hard in practice, and why these solvers behave the way they do. I'll also go over some unfortunate mistakes that commonly occur when evaluating these solvers, in the hopes that we can learn from them. Finally, I'll discuss two pieces of recent work that have potential connections to the SAT community: bounds based upon MaxSAT reasoning, and proof logging.

Video Recording