Clustering is a well-studied problem and several algorithms have been developed to find these clusterings under certain constraints. This work will show the applicability of propositional logic (MaxSAT) based approaches to a specific version of correlation clustering called cluster editing. This is the problem of finding the minimum number of edits to turn a given graph into a disjoint union of cliques. This work proposes a combination of modelling, preprocessing and solving techniques to solve the cluster editing problem via propositional logic. This approach's performance is experimentally evaluated and compared to another search algorithm based on merging vertices and adding/deleting edges. The results show that for certain instances propositional logic based approaches have a satisfactory performance while for other instances the theoretical approach provides a more guided search of the solution space.

Core-guided solvers and Implicit Hitting Set (IHS) solvers have become ubiquitous within the field of Maximum Satisfiability (MaxSAT). While both types of solvers iteratively increase the solution cost until a satisfiable solution is found, the manner in which this relaxation is performed leads to the belief that these techniques are wholly separate from one another. This work exhibits the difficulty of directly translating the cores found by an IHS-solver to cores utilizable by an OLL-solver due to an inherent disconnect between the manner in which both approaches explore the solution space. It will then be shown how this translation can be performed more easily given certain assumptions. Finally, several techniques are introduced for performing a translation from cores of the original formula to OLL-cores which avoids the aforementioned issue, resulting in a hybrid IHS-OLL algorithm. The comparison between the performance of the hybrid algorithm and RC2 shows that the hybrid algorithm achieves analogous performance in terms of the number of instances solved while indicating that utilising cores of the original formula as a starting point for an OLL solver can be beneficial for the performance of the solver in certain cases.