Abstract
Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates.
In this work we analyze minimal cores and minimum correction sets of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate a deep connection between core-guided and hitting set based algorithms. We discuss theoretical and practical implications of our results. Finally, we discuss how we can leverage these results to build an efficient solver.