Towards the unification of the Core-Guided and Hitting Set Maximum Satisfiability approaches

Abstract

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.