Optimal Correlation Clustering via MaxSAT

We introduce an extensible framework for correlation clustering by harnessing the Maximum satisfiability (MaxSAT) Boolean optimization paradigm. The approach is based on formulating the correlation clustering task in an exact fashion as MaxSAT, and then using a state-of-the-art MaxSAT solver for finding clusterings by solving the MaxSAT formulation. Our approach allows for finding optimal clusterings wrt the objective function of the problem, extends to constrained correlation clustering-by allowing for easy integration of user-defined domain knowledge in terms of hard constraints over the clusterings of interest-as well as overlapping correlation clustering. First experiments on the scalability of the approach are presented.