Tags:Core-guided, Hitting set problem, Linear Programming and MaxSAT
Abstract:
Most current complete MaxSAT algorithms fall into two categories: core-guided or implicit hitting set. The two kinds of algorithms seem to have complementary strengths in practice, so that each kind of solver is better able to handle different families of instances. This suggests that a hybrid might match and outperform either, but the techniques used seem incompatible. In this paper, we focus on PMRES, a core-guided algorithm based on max resolution. We show that PMRES implicitly discovers cores of the original formula, as has been previously shown for WPM1. Moreover, we show that in some cases, including unweighted instances, PMRES computes the optimum hitting set of these cores at each iteration. We also give a compact integer linear program which encodes this hitting set problem. Importantly, the continuous relaxation has an optimum that matches the bound computed by PMRES. This goes some way towards resolving the incompatibility of implicit hitting set and core-guided algorithms, since solvers based on the implicit hitting set algorithm typically solve the problem by encoding it as a linear program.
An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming